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	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )