Metamath Proof Explorer

Theorem neiptopuni

Description: Lemma for neiptopreu . (Contributed by Thierry Arnoux, 6-Jan-2018)

Ref Expression
Hypotheses neiptop.o ⊢ J = a ∈ 𝒫 X | ∀ p ∈ a a ∈ N ⁡ p
neiptop.0 ⊢ φ → N : X ⟶ 𝒫 𝒫 X
neiptop.1 ⊢ φ ∧ p ∈ X ∧ a ⊆ b ∧ b ⊆ X ∧ a ∈ N ⁡ p → b ∈ N ⁡ p
neiptop.2 ⊢ φ ∧ p ∈ X → fi ⁡ N ⁡ p ⊆ N ⁡ p
neiptop.3 ⊢ φ ∧ p ∈ X ∧ a ∈ N ⁡ p → p ∈ a
neiptop.4 ⊢ φ ∧ p ∈ X ∧ a ∈ N ⁡ p → ∃ b ∈ N ⁡ p ∀ q ∈ b a ∈ N ⁡ q
neiptop.5 ⊢ φ ∧ p ∈ X → X ∈ N ⁡ p
Assertion neiptopuni ⊢ φ → X = ⋃ J

Proof

Step Hyp Ref Expression
1 neiptop.o ⊢ J = a ∈ 𝒫 X | ∀ p ∈ a a ∈ N ⁡ p
2 neiptop.0 ⊢ φ → N : X ⟶ 𝒫 𝒫 X
3 neiptop.1 ⊢ φ ∧ p ∈ X ∧ a ⊆ b ∧ b ⊆ X ∧ a ∈ N ⁡ p → b ∈ N ⁡ p
4 neiptop.2 ⊢ φ ∧ p ∈ X → fi ⁡ N ⁡ p ⊆ N ⁡ p
5 neiptop.3 ⊢ φ ∧ p ∈ X ∧ a ∈ N ⁡ p → p ∈ a
6 neiptop.4 ⊢ φ ∧ p ∈ X ∧ a ∈ N ⁡ p → ∃ b ∈ N ⁡ p ∀ q ∈ b a ∈ N ⁡ q
7 neiptop.5 ⊢ φ ∧ p ∈ X → X ∈ N ⁡ p
8 elpwi ⊢ a ∈ 𝒫 X → a ⊆ X
9 8 ad2antlr ⊢ p ∈ ⋃ J ∧ a ∈ 𝒫 X ∧ p ∈ a → a ⊆ X
10 simpr ⊢ p ∈ ⋃ J ∧ a ∈ 𝒫 X ∧ p ∈ a → p ∈ a
11 9 10 sseldd ⊢ p ∈ ⋃ J ∧ a ∈ 𝒫 X ∧ p ∈ a → p ∈ X
12 1 unieqi ⊢ ⋃ J = ⋃ a ∈ 𝒫 X | ∀ p ∈ a a ∈ N ⁡ p
13 12 eleq2i ⊢ p ∈ ⋃ J ↔ p ∈ ⋃ a ∈ 𝒫 X | ∀ p ∈ a a ∈ N ⁡ p
14 elunirab ⊢ p ∈ ⋃ a ∈ 𝒫 X | ∀ p ∈ a a ∈ N ⁡ p ↔ ∃ a ∈ 𝒫 X p ∈ a ∧ ∀ p ∈ a a ∈ N ⁡ p
15 13 14 bitri ⊢ p ∈ ⋃ J ↔ ∃ a ∈ 𝒫 X p ∈ a ∧ ∀ p ∈ a a ∈ N ⁡ p
16 simpl ⊢ p ∈ a ∧ ∀ p ∈ a a ∈ N ⁡ p → p ∈ a
17 16 reximi ⊢ ∃ a ∈ 𝒫 X p ∈ a ∧ ∀ p ∈ a a ∈ N ⁡ p → ∃ a ∈ 𝒫 X p ∈ a
18 15 17 sylbi ⊢ p ∈ ⋃ J → ∃ a ∈ 𝒫 X p ∈ a
19 11 18 r19.29a ⊢ p ∈ ⋃ J → p ∈ X
20 19 a1i ⊢ φ → p ∈ ⋃ J → p ∈ X
21 20 ssrdv ⊢ φ → ⋃ J ⊆ X
22 ssidd ⊢ φ → X ⊆ X
23 7 ralrimiva ⊢ φ → ∀ p ∈ X X ∈ N ⁡ p
24 1 neipeltop ⊢ X ∈ J ↔ X ⊆ X ∧ ∀ p ∈ X X ∈ N ⁡ p
25 22 23 24 sylanbrc ⊢ φ → X ∈ J
26 unissel ⊢ ⋃ J ⊆ X ∧ X ∈ J → ⋃ J = X
27 21 25 26 syl2anc ⊢ φ → ⋃ J = X
28 27 eqcomd ⊢ φ → X = ⋃ J