cmpsublem

		Ref	Expression
	Hypothesis	cmpsub.1	\|- X = U. J
	Assertion	cmpsublem	\|- ( ( J e. Top /\ S C_ X ) -> ( A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) -> A. s e. ~P ( J \|`t S ) ( U. ( J \|`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) ) )

Proof

Step	Hyp	Ref	Expression
1		cmpsub.1	\|- X = U. J
2		rabexg	\|- ( J e. Top -> { y e. J \| ( y i^i S ) e. s } e. _V )
3	2	ad2antrr	\|- ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) -> { y e. J \| ( y i^i S ) e. s } e. _V )
4		ssrab2	\|- { y e. J \| ( y i^i S ) e. s } C_ J
5		elpwg	\|- ( { y e. J \| ( y i^i S ) e. s } e. _V -> ( { y e. J \| ( y i^i S ) e. s } e. ~P J <-> { y e. J \| ( y i^i S ) e. s } C_ J ) )
6	4 5	mpbiri	\|- ( { y e. J \| ( y i^i S ) e. s } e. _V -> { y e. J \| ( y i^i S ) e. s } e. ~P J )
7	3 6	syl	\|- ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) -> { y e. J \| ( y i^i S ) e. s } e. ~P J )
8		unieq	\|- ( c = { y e. J \| ( y i^i S ) e. s } -> U. c = U. { y e. J \| ( y i^i S ) e. s } )
9	8	sseq2d	\|- ( c = { y e. J \| ( y i^i S ) e. s } -> ( S C_ U. c <-> S C_ U. { y e. J \| ( y i^i S ) e. s } ) )
10		pweq	\|- ( c = { y e. J \| ( y i^i S ) e. s } -> ~P c = ~P { y e. J \| ( y i^i S ) e. s } )
11	10	ineq1d	\|- ( c = { y e. J \| ( y i^i S ) e. s } -> ( ~P c i^i Fin ) = ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) )
12	11	rexeqdv	\|- ( c = { y e. J \| ( y i^i S ) e. s } -> ( E. d e. ( ~P c i^i Fin ) S C_ U. d <-> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) )
13	9 12	imbi12d	\|- ( c = { y e. J \| ( y i^i S ) e. s } -> ( ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) <-> ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) ) )
14	13	rspcva	\|- ( ( { y e. J \| ( y i^i S ) e. s } e. ~P J /\ A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) -> ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) )
15	7 14	sylan	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) -> ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) )
16	15	ex	\|- ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) -> ( A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) -> ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) ) )
17	1	restuni	\|- ( ( J e. Top /\ S C_ X ) -> S = U. ( J \|`t S ) )
18	17	adantr	\|- ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) -> S = U. ( J \|`t S ) )
19	18	eqeq1d	\|- ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) -> ( S = U. s <-> U. ( J \|`t S ) = U. s ) )
20		velpw	\|- ( s e. ~P ( J \|`t S ) <-> s C_ ( J \|`t S ) )
21		eleq2	\|- ( S = U. s -> ( t e. S <-> t e. U. s ) )
22		eluni	\|- ( t e. U. s <-> E. u ( t e. u /\ u e. s ) )
23	21 22	bitrdi	\|- ( S = U. s -> ( t e. S <-> E. u ( t e. u /\ u e. s ) ) )
24	23	adantl	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ s C_ ( J \|`t S ) ) /\ S = U. s ) -> ( t e. S <-> E. u ( t e. u /\ u e. s ) ) )
25		ssel	\|- ( s C_ ( J \|`t S ) -> ( u e. s -> u e. ( J \|`t S ) ) )
26	1	sseq2i	\|- ( S C_ X <-> S C_ U. J )
27		uniexg	\|- ( J e. Top -> U. J e. _V )
28		ssexg	\|- ( ( S C_ U. J /\ U. J e. _V ) -> S e. _V )
29	28	ancoms	\|- ( ( U. J e. _V /\ S C_ U. J ) -> S e. _V )
30	27 29	sylan	\|- ( ( J e. Top /\ S C_ U. J ) -> S e. _V )
31	26 30	sylan2b	\|- ( ( J e. Top /\ S C_ X ) -> S e. _V )
32		elrest	\|- ( ( J e. Top /\ S e. _V ) -> ( u e. ( J \|`t S ) <-> E. w e. J u = ( w i^i S ) ) )
33	31 32	syldan	\|- ( ( J e. Top /\ S C_ X ) -> ( u e. ( J \|`t S ) <-> E. w e. J u = ( w i^i S ) ) )
34		inss1	\|- ( w i^i S ) C_ w
35		sseq1	\|- ( u = ( w i^i S ) -> ( u C_ w <-> ( w i^i S ) C_ w ) )
36	34 35	mpbiri	\|- ( u = ( w i^i S ) -> u C_ w )
37	36	sselda	\|- ( ( u = ( w i^i S ) /\ t e. u ) -> t e. w )
38	37	3ad2antl3	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ w e. J /\ u = ( w i^i S ) ) /\ t e. u ) -> t e. w )
39	38	3adant2	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ w e. J /\ u = ( w i^i S ) ) /\ u e. s /\ t e. u ) -> t e. w )
40		ineq1	\|- ( y = w -> ( y i^i S ) = ( w i^i S ) )
41	40	eleq1d	\|- ( y = w -> ( ( y i^i S ) e. s <-> ( w i^i S ) e. s ) )
42		simp12	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ w e. J /\ u = ( w i^i S ) ) /\ u e. s /\ t e. u ) -> w e. J )
43		eleq1	\|- ( u = ( w i^i S ) -> ( u e. s <-> ( w i^i S ) e. s ) )
44	43	biimpa	\|- ( ( u = ( w i^i S ) /\ u e. s ) -> ( w i^i S ) e. s )
45	44	3ad2antl3	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ w e. J /\ u = ( w i^i S ) ) /\ u e. s ) -> ( w i^i S ) e. s )
46	45	3adant3	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ w e. J /\ u = ( w i^i S ) ) /\ u e. s /\ t e. u ) -> ( w i^i S ) e. s )
47	41 42 46	elrabd	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ w e. J /\ u = ( w i^i S ) ) /\ u e. s /\ t e. u ) -> w e. { y e. J \| ( y i^i S ) e. s } )
48		vex	\|- w e. _V
49		eleq2	\|- ( v = w -> ( t e. v <-> t e. w ) )
50		eleq1	\|- ( v = w -> ( v e. { y e. J \| ( y i^i S ) e. s } <-> w e. { y e. J \| ( y i^i S ) e. s } ) )
51	49 50	anbi12d	\|- ( v = w -> ( ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) <-> ( t e. w /\ w e. { y e. J \| ( y i^i S ) e. s } ) ) )
52	48 51	spcev	\|- ( ( t e. w /\ w e. { y e. J \| ( y i^i S ) e. s } ) -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) )
53	39 47 52	syl2anc	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ w e. J /\ u = ( w i^i S ) ) /\ u e. s /\ t e. u ) -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) )
54	53	3exp	\|- ( ( ( J e. Top /\ S C_ X ) /\ w e. J /\ u = ( w i^i S ) ) -> ( u e. s -> ( t e. u -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) ) )
55	54	rexlimdv3a	\|- ( ( J e. Top /\ S C_ X ) -> ( E. w e. J u = ( w i^i S ) -> ( u e. s -> ( t e. u -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) ) ) )
56	33 55	sylbid	\|- ( ( J e. Top /\ S C_ X ) -> ( u e. ( J \|`t S ) -> ( u e. s -> ( t e. u -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) ) ) )
57	56	com23	\|- ( ( J e. Top /\ S C_ X ) -> ( u e. s -> ( u e. ( J \|`t S ) -> ( t e. u -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) ) ) )
58	57	com4l	\|- ( u e. s -> ( u e. ( J \|`t S ) -> ( t e. u -> ( ( J e. Top /\ S C_ X ) -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) ) ) )
59	25 58	sylcom	\|- ( s C_ ( J \|`t S ) -> ( u e. s -> ( t e. u -> ( ( J e. Top /\ S C_ X ) -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) ) ) )
60	59	com24	\|- ( s C_ ( J \|`t S ) -> ( ( J e. Top /\ S C_ X ) -> ( t e. u -> ( u e. s -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) ) ) )
61	60	impcom	\|- ( ( ( J e. Top /\ S C_ X ) /\ s C_ ( J \|`t S ) ) -> ( t e. u -> ( u e. s -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) ) )
62	61	impd	\|- ( ( ( J e. Top /\ S C_ X ) /\ s C_ ( J \|`t S ) ) -> ( ( t e. u /\ u e. s ) -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) )
63	62	exlimdv	\|- ( ( ( J e. Top /\ S C_ X ) /\ s C_ ( J \|`t S ) ) -> ( E. u ( t e. u /\ u e. s ) -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) )
64	63	adantr	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ s C_ ( J \|`t S ) ) /\ S = U. s ) -> ( E. u ( t e. u /\ u e. s ) -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) )
65	24 64	sylbid	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ s C_ ( J \|`t S ) ) /\ S = U. s ) -> ( t e. S -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) )
66	65	ex	\|- ( ( ( J e. Top /\ S C_ X ) /\ s C_ ( J \|`t S ) ) -> ( S = U. s -> ( t e. S -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) ) )
67	20 66	sylan2b	\|- ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) -> ( S = U. s -> ( t e. S -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) ) )
68	67	imp	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> ( t e. S -> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) ) )
69		eluni	\|- ( t e. U. { y e. J \| ( y i^i S ) e. s } <-> E. v ( t e. v /\ v e. { y e. J \| ( y i^i S ) e. s } ) )
70	68 69	imbitrrdi	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> ( t e. S -> t e. U. { y e. J \| ( y i^i S ) e. s } ) )
71	70	ssrdv	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> S C_ U. { y e. J \| ( y i^i S ) e. s } )
72		pm2.27	\|- ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> ( ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) )
73		elin	\|- ( d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) <-> ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) )
74		vex	\|- t e. _V
75		eqeq1	\|- ( x = t -> ( x = ( z i^i S ) <-> t = ( z i^i S ) ) )
76	75	rexbidv	\|- ( x = t -> ( E. z e. d x = ( z i^i S ) <-> E. z e. d t = ( z i^i S ) ) )
77	74 76	elab	\|- ( t e. { x \| E. z e. d x = ( z i^i S ) } <-> E. z e. d t = ( z i^i S ) )
78		velpw	\|- ( d e. ~P { y e. J \| ( y i^i S ) e. s } <-> d C_ { y e. J \| ( y i^i S ) e. s } )
79		ssel	\|- ( d C_ { y e. J \| ( y i^i S ) e. s } -> ( z e. d -> z e. { y e. J \| ( y i^i S ) e. s } ) )
80		ineq1	\|- ( y = z -> ( y i^i S ) = ( z i^i S ) )
81	80	eleq1d	\|- ( y = z -> ( ( y i^i S ) e. s <-> ( z i^i S ) e. s ) )
82	81	elrab	\|- ( z e. { y e. J \| ( y i^i S ) e. s } <-> ( z e. J /\ ( z i^i S ) e. s ) )
83		eleq1a	\|- ( ( z i^i S ) e. s -> ( t = ( z i^i S ) -> t e. s ) )
84	82 83	simplbiim	\|- ( z e. { y e. J \| ( y i^i S ) e. s } -> ( t = ( z i^i S ) -> t e. s ) )
85	79 84	syl6	\|- ( d C_ { y e. J \| ( y i^i S ) e. s } -> ( z e. d -> ( t = ( z i^i S ) -> t e. s ) ) )
86	85	2a1d	\|- ( d C_ { y e. J \| ( y i^i S ) e. s } -> ( S C_ U. d -> ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> ( z e. d -> ( t = ( z i^i S ) -> t e. s ) ) ) ) )
87	86	adantr	\|- ( ( d C_ { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) -> ( S C_ U. d -> ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> ( z e. d -> ( t = ( z i^i S ) -> t e. s ) ) ) ) )
88	78 87	sylanb	\|- ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) -> ( S C_ U. d -> ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> ( z e. d -> ( t = ( z i^i S ) -> t e. s ) ) ) ) )
89	88	3imp	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> ( z e. d -> ( t = ( z i^i S ) -> t e. s ) ) )
90	89	rexlimdv	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> ( E. z e. d t = ( z i^i S ) -> t e. s ) )
91	77 90	biimtrid	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> ( t e. { x \| E. z e. d x = ( z i^i S ) } -> t e. s ) )
92	91	ssrdv	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> { x \| E. z e. d x = ( z i^i S ) } C_ s )
93		vex	\|- d e. _V
94	93	abrexex	\|- { x \| E. z e. d x = ( z i^i S ) } e. _V
95	94	elpw	\|- ( { x \| E. z e. d x = ( z i^i S ) } e. ~P s <-> { x \| E. z e. d x = ( z i^i S ) } C_ s )
96	92 95	sylibr	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> { x \| E. z e. d x = ( z i^i S ) } e. ~P s )
97		abrexfi	\|- ( d e. Fin -> { x \| E. z e. d x = ( z i^i S ) } e. Fin )
98	97	ad2antlr	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d ) -> { x \| E. z e. d x = ( z i^i S ) } e. Fin )
99	98	3adant3	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> { x \| E. z e. d x = ( z i^i S ) } e. Fin )
100	96 99	elind	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> { x \| E. z e. d x = ( z i^i S ) } e. ( ~P s i^i Fin ) )
101		dfss	\|- ( S C_ U. d <-> S = ( S i^i U. d ) )
102	101	biimpi	\|- ( S C_ U. d -> S = ( S i^i U. d ) )
103		uniiun	\|- U. d = U_ z e. d z
104	103	ineq2i	\|- ( S i^i U. d ) = ( S i^i U_ z e. d z )
105		iunin2	\|- U_ z e. d ( S i^i z ) = ( S i^i U_ z e. d z )
106		incom	\|- ( S i^i z ) = ( z i^i S )
107	106	a1i	\|- ( z e. d -> ( S i^i z ) = ( z i^i S ) )
108	107	iuneq2i	\|- U_ z e. d ( S i^i z ) = U_ z e. d ( z i^i S )
109	104 105 108	3eqtr2i	\|- ( S i^i U. d ) = U_ z e. d ( z i^i S )
110	102 109	eqtrdi	\|- ( S C_ U. d -> S = U_ z e. d ( z i^i S ) )
111	110	3ad2ant2	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> S = U_ z e. d ( z i^i S ) )
112	18	ad2antrl	\|- ( ( S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> S = U. ( J \|`t S ) )
113	112	3adant1	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> S = U. ( J \|`t S ) )
114		vex	\|- z e. _V
115	114	inex1	\|- ( z i^i S ) e. _V
116	115	dfiun2	\|- U_ z e. d ( z i^i S ) = U. { x \| E. z e. d x = ( z i^i S ) }
117	116	a1i	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> U_ z e. d ( z i^i S ) = U. { x \| E. z e. d x = ( z i^i S ) } )
118	111 113 117	3eqtr3d	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> U. ( J \|`t S ) = U. { x \| E. z e. d x = ( z i^i S ) } )
119		unieq	\|- ( t = { x \| E. z e. d x = ( z i^i S ) } -> U. t = U. { x \| E. z e. d x = ( z i^i S ) } )
120	119	rspceeqv	\|- ( ( { x \| E. z e. d x = ( z i^i S ) } e. ( ~P s i^i Fin ) /\ U. ( J \|`t S ) = U. { x \| E. z e. d x = ( z i^i S ) } ) -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t )
121	100 118 120	syl2anc	\|- ( ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) /\ S C_ U. d /\ ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) ) -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t )
122	121	3exp	\|- ( ( d e. ~P { y e. J \| ( y i^i S ) e. s } /\ d e. Fin ) -> ( S C_ U. d -> ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) ) )
123	73 122	sylbi	\|- ( d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) -> ( S C_ U. d -> ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) ) )
124	123	rexlimiv	\|- ( E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d -> ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) )
125	72 124	syl6	\|- ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> ( ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) -> ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) ) )
126	125	com3r	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> ( ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) ) )
127	71 126	mpd	\|- ( ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) /\ S = U. s ) -> ( ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) )
128	127	ex	\|- ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) -> ( S = U. s -> ( ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) ) )
129	19 128	sylbird	\|- ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) -> ( U. ( J \|`t S ) = U. s -> ( ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) ) )
130	129	com23	\|- ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) -> ( ( S C_ U. { y e. J \| ( y i^i S ) e. s } -> E. d e. ( ~P { y e. J \| ( y i^i S ) e. s } i^i Fin ) S C_ U. d ) -> ( U. ( J \|`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) ) )
131	16 130	syld	\|- ( ( ( J e. Top /\ S C_ X ) /\ s e. ~P ( J \|`t S ) ) -> ( A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) -> ( U. ( J \|`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) ) )
132	131	ralrimdva	\|- ( ( J e. Top /\ S C_ X ) -> ( A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) -> A. s e. ~P ( J \|`t S ) ( U. ( J \|`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J \|`t S ) = U. t ) ) )

Metamath Proof Explorer

Theorem cmpsublem

Proof