no goals
α : Type u_1
β : Type ?u.144485
γ : Type ?u.144488
ι : Sort ?u.144491
ι' : Sort ?u.144494
ι₂ : Sort ?u.144497
κ : ι → Sort ?u.144502
κ₁ : ι → Sort ?u.144507
κ₂ : ι → Sort ?u.144512
κ' : ι' → Sort ?u.144517
S : Set (Set α)
x : α
⊢ x ∈ (⋃₀ S)ᶜ ↔ x ∈ ⋂₀ (compl '' S)
simp