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∈aa∈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∈ba∈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∈aa∈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∈ba∈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∈aa∈N⁡p
13 12 eleq2i ⊢p∈⋃J↔p∈⋃a∈𝒫X|∀p∈aa∈N⁡p
14 elunirab ⊢p∈⋃a∈𝒫X|∀p∈aa∈N⁡p↔∃a∈𝒫Xp∈a∧∀p∈aa∈N⁡p
15 13 14 bitri ⊢p∈⋃J↔∃a∈𝒫Xp∈a∧∀p∈aa∈N⁡p
16 simpl ⊢p∈a∧∀p∈aa∈N⁡p→p∈a
17 16 reximi ⊢∃a∈𝒫Xp∈a∧∀p∈aa∈N⁡p→∃a∈𝒫Xp∈a
18 15 17 sylbi ⊢p∈⋃J→∃a∈𝒫Xp∈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∈XX∈N⁡p
24 1 neipeltop ⊢X∈J↔X⊆X∧∀p∈XX∈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