This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem neiptopuni

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

Ref Expression
Hypotheses neiptop.o ⊢ 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
neiptop.0 ⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )
neiptop.1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) )
neiptop.2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )
neiptop.3 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 )
neiptop.4 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) )
neiptop.5 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )
Assertion neiptopuni ( 𝜑 → 𝑋 = ∪ 𝐽 )

Proof

Step Hyp Ref Expression
1 neiptop.o ⊢ 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
2 neiptop.0 ⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )
3 neiptop.1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) )
4 neiptop.2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )
5 neiptop.3 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 )
6 neiptop.4 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) )
7 neiptop.5 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )
8 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋 )
9 8 ad2antlr ⊢ ( ( ( 𝑝 ∈ ∪ 𝐽 ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝 ∈ 𝑎 ) → 𝑎 ⊆ 𝑋 )
10 simpr ⊢ ( ( ( 𝑝 ∈ ∪ 𝐽 ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝 ∈ 𝑎 ) → 𝑝 ∈ 𝑎 )
11 9 10 sseldd ⊢ ( ( ( 𝑝 ∈ ∪ 𝐽 ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑝 ∈ 𝑎 ) → 𝑝 ∈ 𝑋 )
12 1 unieqi ⊢ ∪ 𝐽 = ∪ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
13 12 eleq2i ⊢ ( 𝑝 ∈ ∪ 𝐽 ↔ 𝑝 ∈ ∪ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) } )
14 elunirab ⊢ ( 𝑝 ∈ ∪ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) } ↔ ∃ 𝑎 ∈ 𝒫 𝑋 ( 𝑝 ∈ 𝑎 ∧ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) )
15 13 14 bitri ⊢ ( 𝑝 ∈ ∪ 𝐽 ↔ ∃ 𝑎 ∈ 𝒫 𝑋 ( 𝑝 ∈ 𝑎 ∧ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) )
16 simpl ⊢ ( ( 𝑝 ∈ 𝑎 ∧ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 )
17 16 reximi ⊢ ( ∃ 𝑎 ∈ 𝒫 𝑋 ( 𝑝 ∈ 𝑎 ∧ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑎 ∈ 𝒫 𝑋 𝑝 ∈ 𝑎 )
18 15 17 sylbi ⊢ ( 𝑝 ∈ ∪ 𝐽 → ∃ 𝑎 ∈ 𝒫 𝑋 𝑝 ∈ 𝑎 )
19 11 18 r19.29a ⊢ ( 𝑝 ∈ ∪ 𝐽 → 𝑝 ∈ 𝑋 )
20 19 a1i ⊢ ( 𝜑 → ( 𝑝 ∈ ∪ 𝐽 → 𝑝 ∈ 𝑋 ) )
21 20 ssrdv ⊢ ( 𝜑 → ∪ 𝐽 ⊆ 𝑋 )
22 ssidd ⊢ ( 𝜑 → 𝑋 ⊆ 𝑋 )
23 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑋 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )
24 1 neipeltop ⊢ ( 𝑋 ∈ 𝐽 ↔ ( 𝑋 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑋 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) ) )
25 22 23 24 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
26 unissel ⊢ ( ( ∪ 𝐽 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽 ) → ∪ 𝐽 = 𝑋 )
27 21 25 26 syl2anc ⊢ ( 𝜑 → ∪ 𝐽 = 𝑋 )
28 27 eqcomd ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )