Theorem neiptopuni

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

	Ref	Expression
Hypotheses	neiptop.o	|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }
	neiptop.0	|- ( ph -> N : X --> ~P ~P X )
	neiptop.1	|- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
	neiptop.2	|- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
	neiptop.3	|- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )
	neiptop.4	|- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
	neiptop.5	|- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )
Assertion	neiptopuni	|- ( ph -> X = U. J )

Proof

Step	Hyp	Ref	Expression
1		neiptop.o	|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }
2		neiptop.0	|- ( ph -> N : X --> ~P ~P X )
3		neiptop.1	|- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
4		neiptop.2	|- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
5		neiptop.3	|- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )
6		neiptop.4	|- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
7		neiptop.5	|- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )
8		elpwi	|- ( a e. ~P X -> a C_ X )
9	8	ad2antlr	|- ( ( ( p e. U. J /\ a e. ~P X ) /\ p e. a ) -> a C_ X )
10		simpr	|- ( ( ( p e. U. J /\ a e. ~P X ) /\ p e. a ) -> p e. a )
11	9 10	sseldd	|- ( ( ( p e. U. J /\ a e. ~P X ) /\ p e. a ) -> p e. X )
12	1	unieqi	|- U. J = U. { a e. ~P X | A. p e. a a e. ( N ` p ) }
13	12	eleq2i	|- ( p e. U. J <-> p e. U. { a e. ~P X | A. p e. a a e. ( N ` p ) } )
14		elunirab	|- ( p e. U. { a e. ~P X | A. p e. a a e. ( N ` p ) } <-> E. a e. ~P X ( p e. a /\ A. p e. a a e. ( N ` p ) ) )
15	13 14	bitri	|- ( p e. U. J <-> E. a e. ~P X ( p e. a /\ A. p e. a a e. ( N ` p ) ) )
16		simpl	|- ( ( p e. a /\ A. p e. a a e. ( N ` p ) ) -> p e. a )
17	16	reximi	|- ( E. a e. ~P X ( p e. a /\ A. p e. a a e. ( N ` p ) ) -> E. a e. ~P X p e. a )
18	15 17	sylbi	|- ( p e. U. J -> E. a e. ~P X p e. a )
19	11 18	r19.29a	|- ( p e. U. J -> p e. X )
20	19	a1i	|- ( ph -> ( p e. U. J -> p e. X ) )
21	20	ssrdv	|- ( ph -> U. J C_ X )
22		ssidd	|- ( ph -> X C_ X )
23	7	ralrimiva	|- ( ph -> A. p e. X X e. ( N ` p ) )
24	1	neipeltop	|- ( X e. J <-> ( X C_ X /\ A. p e. X X e. ( N ` p ) ) )
25	22 23 24	sylanbrc	|- ( ph -> X e. J )
26		unissel	|- ( ( U. J C_ X /\ X e. J ) -> U. J = X )
27	21 25 26	syl2anc	|- ( ph -> U. J = X )
28	27	eqcomd	|- ( ph -> X = U. J )