case h
L : Language
T : Theory L
α : Type w
ι : Type u_1
S : ι → Theory (L[[α]])
x✝ : CompleteType T α
⊢ (x✝ ∈ ⋂ (i : ι), {p | S i ⊆ ↑p}) ↔ x✝ ∈ {p | (⋃ (i : ι), S i) ⊆ ↑p}
L : Language
T : Theory L
α : Type w
ι : Type u_1
S : ι → Theory (L[[α]])
⊢ (⋂ (i : ι), {p | S i ⊆ ↑p}) = {p | (⋃ (i : ι), S i) ⊆ ↑p}
ext
no goals
case h
L : Language
T : Theory L
α : Type w
ι : Type u_1
S : ι → Theory (L[[α]])
x✝ : CompleteType T α
⊢ (x✝ ∈ ⋂ (i : ι), {p | S i ⊆ ↑p}) ↔ x✝ ∈ {p | (⋃ (i : ι), S i) ⊆ ↑p}
simp only [mem_iInter, mem_setOf_eq, iUnion_subset_iff]