Metamath Proof Explorer

Theorem cmpsublem

Description: Lemma for cmpsub . (Contributed by Jeff Hankins, 28-Jun-2009)

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 syl6ibr 
 |-  ( ( ( ( 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 syl5bi 
 |-  ( ( ( 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 ) ) )