Step |
Hyp |
Ref |
Expression |
1 |
|
alexsubALT.1 |
|- X = U. J |
2 |
|
dfrex2 |
|- ( E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n <-> -. A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) |
3 |
2
|
ralbii |
|- ( A. s e. t E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n <-> A. s e. t -. A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) |
4 |
|
ralnex |
|- ( A. s e. t -. A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n <-> -. E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) |
5 |
3 4
|
bitr2i |
|- ( -. E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n <-> A. s e. t E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n ) |
6 |
|
elin |
|- ( n e. ( ~P ( u u. { s } ) i^i Fin ) <-> ( n e. ~P ( u u. { s } ) /\ n e. Fin ) ) |
7 |
|
elpwi |
|- ( n e. ~P ( u u. { s } ) -> n C_ ( u u. { s } ) ) |
8 |
7
|
adantr |
|- ( ( n e. ~P ( u u. { s } ) /\ n e. Fin ) -> n C_ ( u u. { s } ) ) |
9 |
|
uncom |
|- ( u u. { s } ) = ( { s } u. u ) |
10 |
8 9
|
sseqtrdi |
|- ( ( n e. ~P ( u u. { s } ) /\ n e. Fin ) -> n C_ ( { s } u. u ) ) |
11 |
|
ssundif |
|- ( n C_ ( { s } u. u ) <-> ( n \ { s } ) C_ u ) |
12 |
10 11
|
sylib |
|- ( ( n e. ~P ( u u. { s } ) /\ n e. Fin ) -> ( n \ { s } ) C_ u ) |
13 |
|
diffi |
|- ( n e. Fin -> ( n \ { s } ) e. Fin ) |
14 |
13
|
adantl |
|- ( ( n e. ~P ( u u. { s } ) /\ n e. Fin ) -> ( n \ { s } ) e. Fin ) |
15 |
12 14
|
jca |
|- ( ( n e. ~P ( u u. { s } ) /\ n e. Fin ) -> ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) ) |
16 |
6 15
|
sylbi |
|- ( n e. ( ~P ( u u. { s } ) i^i Fin ) -> ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) ) |
17 |
16
|
adantr |
|- ( ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) -> ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) ) |
18 |
17
|
ad2antll |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) ) |
19 |
|
elin |
|- ( ( n \ { s } ) e. ( ~P u i^i Fin ) <-> ( ( n \ { s } ) e. ~P u /\ ( n \ { s } ) e. Fin ) ) |
20 |
|
vex |
|- u e. _V |
21 |
20
|
elpw2 |
|- ( ( n \ { s } ) e. ~P u <-> ( n \ { s } ) C_ u ) |
22 |
21
|
anbi1i |
|- ( ( ( n \ { s } ) e. ~P u /\ ( n \ { s } ) e. Fin ) <-> ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) ) |
23 |
19 22
|
bitr2i |
|- ( ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) <-> ( n \ { s } ) e. ( ~P u i^i Fin ) ) |
24 |
18 23
|
sylib |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> ( n \ { s } ) e. ( ~P u i^i Fin ) ) |
25 |
|
simprrr |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> X = U. n ) |
26 |
|
eldif |
|- ( x e. ( n \ { s } ) <-> ( x e. n /\ -. x e. { s } ) ) |
27 |
26
|
simplbi2 |
|- ( x e. n -> ( -. x e. { s } -> x e. ( n \ { s } ) ) ) |
28 |
|
elun |
|- ( x e. ( ( n \ { s } ) u. { s } ) <-> ( x e. ( n \ { s } ) \/ x e. { s } ) ) |
29 |
|
orcom |
|- ( ( x e. { s } \/ x e. ( n \ { s } ) ) <-> ( x e. ( n \ { s } ) \/ x e. { s } ) ) |
30 |
28 29
|
bitr4i |
|- ( x e. ( ( n \ { s } ) u. { s } ) <-> ( x e. { s } \/ x e. ( n \ { s } ) ) ) |
31 |
|
df-or |
|- ( ( x e. { s } \/ x e. ( n \ { s } ) ) <-> ( -. x e. { s } -> x e. ( n \ { s } ) ) ) |
32 |
30 31
|
bitr2i |
|- ( ( -. x e. { s } -> x e. ( n \ { s } ) ) <-> x e. ( ( n \ { s } ) u. { s } ) ) |
33 |
27 32
|
sylib |
|- ( x e. n -> x e. ( ( n \ { s } ) u. { s } ) ) |
34 |
33
|
ssriv |
|- n C_ ( ( n \ { s } ) u. { s } ) |
35 |
|
uniss |
|- ( n C_ ( ( n \ { s } ) u. { s } ) -> U. n C_ U. ( ( n \ { s } ) u. { s } ) ) |
36 |
34 35
|
mp1i |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. n C_ U. ( ( n \ { s } ) u. { s } ) ) |
37 |
|
uniun |
|- U. ( ( n \ { s } ) u. { s } ) = ( U. ( n \ { s } ) u. U. { s } ) |
38 |
|
unisnv |
|- U. { s } = s |
39 |
38
|
uneq2i |
|- ( U. ( n \ { s } ) u. U. { s } ) = ( U. ( n \ { s } ) u. s ) |
40 |
37 39
|
eqtri |
|- U. ( ( n \ { s } ) u. { s } ) = ( U. ( n \ { s } ) u. s ) |
41 |
36 40
|
sseqtrdi |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. n C_ ( U. ( n \ { s } ) u. s ) ) |
42 |
25 41
|
eqsstrd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> X C_ ( U. ( n \ { s } ) u. s ) ) |
43 |
|
difss |
|- ( n \ { s } ) C_ n |
44 |
43
|
unissi |
|- U. ( n \ { s } ) C_ U. n |
45 |
|
sseq2 |
|- ( X = U. n -> ( U. ( n \ { s } ) C_ X <-> U. ( n \ { s } ) C_ U. n ) ) |
46 |
44 45
|
mpbiri |
|- ( X = U. n -> U. ( n \ { s } ) C_ X ) |
47 |
46
|
adantl |
|- ( ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) -> U. ( n \ { s } ) C_ X ) |
48 |
47
|
ad2antll |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. ( n \ { s } ) C_ X ) |
49 |
|
elinel1 |
|- ( t e. ( ~P x i^i Fin ) -> t e. ~P x ) |
50 |
49
|
elpwid |
|- ( t e. ( ~P x i^i Fin ) -> t C_ x ) |
51 |
50
|
ad3antrrr |
|- ( ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) -> t C_ x ) |
52 |
51
|
ad2antlr |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> t C_ x ) |
53 |
|
simprl |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> s e. t ) |
54 |
52 53
|
sseldd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> s e. x ) |
55 |
|
elssuni |
|- ( s e. x -> s C_ U. x ) |
56 |
54 55
|
syl |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> s C_ U. x ) |
57 |
|
fibas |
|- ( fi ` x ) e. TopBases |
58 |
|
unitg |
|- ( ( fi ` x ) e. TopBases -> U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x ) ) |
59 |
57 58
|
mp1i |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x ) ) |
60 |
|
unieq |
|- ( J = ( topGen ` ( fi ` x ) ) -> U. J = U. ( topGen ` ( fi ` x ) ) ) |
61 |
60
|
3ad2ant1 |
|- ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> U. J = U. ( topGen ` ( fi ` x ) ) ) |
62 |
61
|
ad3antrrr |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. J = U. ( topGen ` ( fi ` x ) ) ) |
63 |
|
vex |
|- x e. _V |
64 |
|
fiuni |
|- ( x e. _V -> U. x = U. ( fi ` x ) ) |
65 |
63 64
|
mp1i |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. x = U. ( fi ` x ) ) |
66 |
59 62 65
|
3eqtr4rd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. x = U. J ) |
67 |
66 1
|
eqtr4di |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. x = X ) |
68 |
56 67
|
sseqtrd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> s C_ X ) |
69 |
48 68
|
unssd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> ( U. ( n \ { s } ) u. s ) C_ X ) |
70 |
42 69
|
eqssd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> X = ( U. ( n \ { s } ) u. s ) ) |
71 |
|
unieq |
|- ( m = ( n \ { s } ) -> U. m = U. ( n \ { s } ) ) |
72 |
71
|
uneq1d |
|- ( m = ( n \ { s } ) -> ( U. m u. s ) = ( U. ( n \ { s } ) u. s ) ) |
73 |
72
|
rspceeqv |
|- ( ( ( n \ { s } ) e. ( ~P u i^i Fin ) /\ X = ( U. ( n \ { s } ) u. s ) ) -> E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) |
74 |
24 70 73
|
syl2anc |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) |
75 |
74
|
expr |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ s e. t ) -> ( ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) -> E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) ) |
76 |
75
|
expd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ s e. t ) -> ( n e. ( ~P ( u u. { s } ) i^i Fin ) -> ( X = U. n -> E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) ) ) |
77 |
76
|
rexlimdv |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ s e. t ) -> ( E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n -> E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) ) |
78 |
77
|
ralimdva |
|- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( A. s e. t E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n -> A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) ) |
79 |
|
elinel2 |
|- ( t e. ( ~P x i^i Fin ) -> t e. Fin ) |
80 |
79
|
adantr |
|- ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) -> t e. Fin ) |
81 |
|
unieq |
|- ( m = ( f ` s ) -> U. m = U. ( f ` s ) ) |
82 |
81
|
uneq1d |
|- ( m = ( f ` s ) -> ( U. m u. s ) = ( U. ( f ` s ) u. s ) ) |
83 |
82
|
eqeq2d |
|- ( m = ( f ` s ) -> ( X = ( U. m u. s ) <-> X = ( U. ( f ` s ) u. s ) ) ) |
84 |
83
|
ac6sfi |
|- ( ( t e. Fin /\ A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) -> E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) |
85 |
84
|
ex |
|- ( t e. Fin -> ( A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) -> E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) ) |
86 |
80 85
|
syl |
|- ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) -> ( A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) -> E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) ) |
87 |
86
|
adantr |
|- ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) -> ( A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) -> E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) ) |
88 |
87
|
ad2antrl |
|- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) -> E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) ) |
89 |
|
ffvelcdm |
|- ( ( f : t --> ( ~P u i^i Fin ) /\ s e. t ) -> ( f ` s ) e. ( ~P u i^i Fin ) ) |
90 |
|
elin |
|- ( ( f ` s ) e. ( ~P u i^i Fin ) <-> ( ( f ` s ) e. ~P u /\ ( f ` s ) e. Fin ) ) |
91 |
|
elpwi |
|- ( ( f ` s ) e. ~P u -> ( f ` s ) C_ u ) |
92 |
91
|
adantr |
|- ( ( ( f ` s ) e. ~P u /\ ( f ` s ) e. Fin ) -> ( f ` s ) C_ u ) |
93 |
90 92
|
sylbi |
|- ( ( f ` s ) e. ( ~P u i^i Fin ) -> ( f ` s ) C_ u ) |
94 |
89 93
|
syl |
|- ( ( f : t --> ( ~P u i^i Fin ) /\ s e. t ) -> ( f ` s ) C_ u ) |
95 |
94
|
ralrimiva |
|- ( f : t --> ( ~P u i^i Fin ) -> A. s e. t ( f ` s ) C_ u ) |
96 |
|
iunss |
|- ( U_ s e. t ( f ` s ) C_ u <-> A. s e. t ( f ` s ) C_ u ) |
97 |
95 96
|
sylibr |
|- ( f : t --> ( ~P u i^i Fin ) -> U_ s e. t ( f ` s ) C_ u ) |
98 |
97
|
ad2antrl |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> U_ s e. t ( f ` s ) C_ u ) |
99 |
|
simplrr |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> w e. u ) |
100 |
99
|
snssd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> { w } C_ u ) |
101 |
98 100
|
unssd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( U_ s e. t ( f ` s ) u. { w } ) C_ u ) |
102 |
89
|
elin2d |
|- ( ( f : t --> ( ~P u i^i Fin ) /\ s e. t ) -> ( f ` s ) e. Fin ) |
103 |
102
|
ralrimiva |
|- ( f : t --> ( ~P u i^i Fin ) -> A. s e. t ( f ` s ) e. Fin ) |
104 |
|
iunfi |
|- ( ( t e. Fin /\ A. s e. t ( f ` s ) e. Fin ) -> U_ s e. t ( f ` s ) e. Fin ) |
105 |
80 103 104
|
syl2an |
|- ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ f : t --> ( ~P u i^i Fin ) ) -> U_ s e. t ( f ` s ) e. Fin ) |
106 |
105
|
ad4ant14 |
|- ( ( ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) /\ f : t --> ( ~P u i^i Fin ) ) -> U_ s e. t ( f ` s ) e. Fin ) |
107 |
106
|
ad2ant2lr |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> U_ s e. t ( f ` s ) e. Fin ) |
108 |
|
snfi |
|- { w } e. Fin |
109 |
|
unfi |
|- ( ( U_ s e. t ( f ` s ) e. Fin /\ { w } e. Fin ) -> ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) |
110 |
107 108 109
|
sylancl |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) |
111 |
101 110
|
jca |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( ( U_ s e. t ( f ` s ) u. { w } ) C_ u /\ ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) ) |
112 |
|
elin |
|- ( ( U_ s e. t ( f ` s ) u. { w } ) e. ( ~P u i^i Fin ) <-> ( ( U_ s e. t ( f ` s ) u. { w } ) e. ~P u /\ ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) ) |
113 |
20
|
elpw2 |
|- ( ( U_ s e. t ( f ` s ) u. { w } ) e. ~P u <-> ( U_ s e. t ( f ` s ) u. { w } ) C_ u ) |
114 |
113
|
anbi1i |
|- ( ( ( U_ s e. t ( f ` s ) u. { w } ) e. ~P u /\ ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) <-> ( ( U_ s e. t ( f ` s ) u. { w } ) C_ u /\ ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) ) |
115 |
112 114
|
bitr2i |
|- ( ( ( U_ s e. t ( f ` s ) u. { w } ) C_ u /\ ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) <-> ( U_ s e. t ( f ` s ) u. { w } ) e. ( ~P u i^i Fin ) ) |
116 |
111 115
|
sylib |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( U_ s e. t ( f ` s ) u. { w } ) e. ( ~P u i^i Fin ) ) |
117 |
|
ralnex |
|- ( A. s e. t -. y e. ( f ` s ) <-> -. E. s e. t y e. ( f ` s ) ) |
118 |
117
|
imbi2i |
|- ( ( v e. y -> A. s e. t -. y e. ( f ` s ) ) <-> ( v e. y -> -. E. s e. t y e. ( f ` s ) ) ) |
119 |
118
|
albii |
|- ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) <-> A. y ( v e. y -> -. E. s e. t y e. ( f ` s ) ) ) |
120 |
|
alinexa |
|- ( A. y ( v e. y -> -. E. s e. t y e. ( f ` s ) ) <-> -. E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) ) |
121 |
119 120
|
bitr2i |
|- ( -. E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) <-> A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) ) |
122 |
|
fveq2 |
|- ( s = z -> ( f ` s ) = ( f ` z ) ) |
123 |
122
|
unieqd |
|- ( s = z -> U. ( f ` s ) = U. ( f ` z ) ) |
124 |
|
id |
|- ( s = z -> s = z ) |
125 |
123 124
|
uneq12d |
|- ( s = z -> ( U. ( f ` s ) u. s ) = ( U. ( f ` z ) u. z ) ) |
126 |
125
|
eqeq2d |
|- ( s = z -> ( X = ( U. ( f ` s ) u. s ) <-> X = ( U. ( f ` z ) u. z ) ) ) |
127 |
126
|
rspcv |
|- ( z e. t -> ( A. s e. t X = ( U. ( f ` s ) u. s ) -> X = ( U. ( f ` z ) u. z ) ) ) |
128 |
|
eleq2 |
|- ( X = ( U. ( f ` z ) u. z ) -> ( v e. X <-> v e. ( U. ( f ` z ) u. z ) ) ) |
129 |
128
|
biimpd |
|- ( X = ( U. ( f ` z ) u. z ) -> ( v e. X -> v e. ( U. ( f ` z ) u. z ) ) ) |
130 |
|
elun |
|- ( v e. ( U. ( f ` z ) u. z ) <-> ( v e. U. ( f ` z ) \/ v e. z ) ) |
131 |
|
eluni |
|- ( v e. U. ( f ` z ) <-> E. w ( v e. w /\ w e. ( f ` z ) ) ) |
132 |
131
|
orbi1i |
|- ( ( v e. U. ( f ` z ) \/ v e. z ) <-> ( E. w ( v e. w /\ w e. ( f ` z ) ) \/ v e. z ) ) |
133 |
|
df-or |
|- ( ( E. w ( v e. w /\ w e. ( f ` z ) ) \/ v e. z ) <-> ( -. E. w ( v e. w /\ w e. ( f ` z ) ) -> v e. z ) ) |
134 |
|
alinexa |
|- ( A. w ( v e. w -> -. w e. ( f ` z ) ) <-> -. E. w ( v e. w /\ w e. ( f ` z ) ) ) |
135 |
134
|
imbi1i |
|- ( ( A. w ( v e. w -> -. w e. ( f ` z ) ) -> v e. z ) <-> ( -. E. w ( v e. w /\ w e. ( f ` z ) ) -> v e. z ) ) |
136 |
133 135
|
bitr4i |
|- ( ( E. w ( v e. w /\ w e. ( f ` z ) ) \/ v e. z ) <-> ( A. w ( v e. w -> -. w e. ( f ` z ) ) -> v e. z ) ) |
137 |
130 132 136
|
3bitri |
|- ( v e. ( U. ( f ` z ) u. z ) <-> ( A. w ( v e. w -> -. w e. ( f ` z ) ) -> v e. z ) ) |
138 |
|
eleq2 |
|- ( y = w -> ( v e. y <-> v e. w ) ) |
139 |
|
eleq1w |
|- ( y = w -> ( y e. ( f ` s ) <-> w e. ( f ` s ) ) ) |
140 |
139
|
notbid |
|- ( y = w -> ( -. y e. ( f ` s ) <-> -. w e. ( f ` s ) ) ) |
141 |
140
|
ralbidv |
|- ( y = w -> ( A. s e. t -. y e. ( f ` s ) <-> A. s e. t -. w e. ( f ` s ) ) ) |
142 |
138 141
|
imbi12d |
|- ( y = w -> ( ( v e. y -> A. s e. t -. y e. ( f ` s ) ) <-> ( v e. w -> A. s e. t -. w e. ( f ` s ) ) ) ) |
143 |
142
|
spvv |
|- ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> ( v e. w -> A. s e. t -. w e. ( f ` s ) ) ) |
144 |
122
|
eleq2d |
|- ( s = z -> ( w e. ( f ` s ) <-> w e. ( f ` z ) ) ) |
145 |
144
|
notbid |
|- ( s = z -> ( -. w e. ( f ` s ) <-> -. w e. ( f ` z ) ) ) |
146 |
145
|
rspcv |
|- ( z e. t -> ( A. s e. t -. w e. ( f ` s ) -> -. w e. ( f ` z ) ) ) |
147 |
143 146
|
syl9r |
|- ( z e. t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> ( v e. w -> -. w e. ( f ` z ) ) ) ) |
148 |
147
|
alrimdv |
|- ( z e. t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> A. w ( v e. w -> -. w e. ( f ` z ) ) ) ) |
149 |
148
|
imim1d |
|- ( z e. t -> ( ( A. w ( v e. w -> -. w e. ( f ` z ) ) -> v e. z ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) |
150 |
137 149
|
biimtrid |
|- ( z e. t -> ( v e. ( U. ( f ` z ) u. z ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) |
151 |
150
|
a1dd |
|- ( z e. t -> ( v e. ( U. ( f ` z ) u. z ) -> ( w = |^| t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) ) |
152 |
129 151
|
syl9r |
|- ( z e. t -> ( X = ( U. ( f ` z ) u. z ) -> ( v e. X -> ( w = |^| t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) ) ) |
153 |
127 152
|
syld |
|- ( z e. t -> ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( v e. X -> ( w = |^| t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) ) ) |
154 |
153
|
com14 |
|- ( w = |^| t -> ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( v e. X -> ( z e. t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) ) ) |
155 |
154
|
imp31 |
|- ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( z e. t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) |
156 |
155
|
com23 |
|- ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> ( z e. t -> v e. z ) ) ) |
157 |
156
|
ralrimdv |
|- ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> A. z e. t v e. z ) ) |
158 |
|
vex |
|- v e. _V |
159 |
158
|
elint2 |
|- ( v e. |^| t <-> A. z e. t v e. z ) |
160 |
157 159
|
syl6ibr |
|- ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. |^| t ) ) |
161 |
|
eleq2 |
|- ( w = |^| t -> ( v e. w <-> v e. |^| t ) ) |
162 |
161
|
ad2antrr |
|- ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( v e. w <-> v e. |^| t ) ) |
163 |
160 162
|
sylibrd |
|- ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. w ) ) |
164 |
121 163
|
biimtrid |
|- ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( -. E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) -> v e. w ) ) |
165 |
164
|
orrd |
|- ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) \/ v e. w ) ) |
166 |
165
|
ex |
|- ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) -> ( v e. X -> ( E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) \/ v e. w ) ) ) |
167 |
|
orc |
|- ( E. s e. t y e. ( f ` s ) -> ( E. s e. t y e. ( f ` s ) \/ y = w ) ) |
168 |
167
|
anim2i |
|- ( ( v e. y /\ E. s e. t y e. ( f ` s ) ) -> ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) ) |
169 |
168
|
eximi |
|- ( E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) -> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) ) |
170 |
|
equid |
|- w = w |
171 |
|
vex |
|- w e. _V |
172 |
|
equequ1 |
|- ( y = w -> ( y = w <-> w = w ) ) |
173 |
138 172
|
anbi12d |
|- ( y = w -> ( ( v e. y /\ y = w ) <-> ( v e. w /\ w = w ) ) ) |
174 |
171 173
|
spcev |
|- ( ( v e. w /\ w = w ) -> E. y ( v e. y /\ y = w ) ) |
175 |
170 174
|
mpan2 |
|- ( v e. w -> E. y ( v e. y /\ y = w ) ) |
176 |
|
olc |
|- ( y = w -> ( E. s e. t y e. ( f ` s ) \/ y = w ) ) |
177 |
176
|
anim2i |
|- ( ( v e. y /\ y = w ) -> ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) ) |
178 |
177
|
eximi |
|- ( E. y ( v e. y /\ y = w ) -> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) ) |
179 |
175 178
|
syl |
|- ( v e. w -> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) ) |
180 |
169 179
|
jaoi |
|- ( ( E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) \/ v e. w ) -> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) ) |
181 |
|
eluni |
|- ( v e. U. ( U_ s e. t ( f ` s ) u. { w } ) <-> E. y ( v e. y /\ y e. ( U_ s e. t ( f ` s ) u. { w } ) ) ) |
182 |
|
elun |
|- ( y e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( y e. U_ s e. t ( f ` s ) \/ y e. { w } ) ) |
183 |
|
eliun |
|- ( y e. U_ s e. t ( f ` s ) <-> E. s e. t y e. ( f ` s ) ) |
184 |
|
velsn |
|- ( y e. { w } <-> y = w ) |
185 |
183 184
|
orbi12i |
|- ( ( y e. U_ s e. t ( f ` s ) \/ y e. { w } ) <-> ( E. s e. t y e. ( f ` s ) \/ y = w ) ) |
186 |
182 185
|
bitri |
|- ( y e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( E. s e. t y e. ( f ` s ) \/ y = w ) ) |
187 |
186
|
anbi2i |
|- ( ( v e. y /\ y e. ( U_ s e. t ( f ` s ) u. { w } ) ) <-> ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) ) |
188 |
187
|
exbii |
|- ( E. y ( v e. y /\ y e. ( U_ s e. t ( f ` s ) u. { w } ) ) <-> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) ) |
189 |
181 188
|
bitr2i |
|- ( E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) <-> v e. U. ( U_ s e. t ( f ` s ) u. { w } ) ) |
190 |
180 189
|
sylib |
|- ( ( E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) \/ v e. w ) -> v e. U. ( U_ s e. t ( f ` s ) u. { w } ) ) |
191 |
166 190
|
syl6 |
|- ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) -> ( v e. X -> v e. U. ( U_ s e. t ( f ` s ) u. { w } ) ) ) |
192 |
191
|
ad5ant25 |
|- ( ( ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) -> ( v e. X -> v e. U. ( U_ s e. t ( f ` s ) u. { w } ) ) ) |
193 |
192
|
ad2ant2l |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( v e. X -> v e. U. ( U_ s e. t ( f ` s ) u. { w } ) ) ) |
194 |
193
|
ssrdv |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> X C_ U. ( U_ s e. t ( f ` s ) u. { w } ) ) |
195 |
|
elun |
|- ( v e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( v e. U_ s e. t ( f ` s ) \/ v e. { w } ) ) |
196 |
|
eliun |
|- ( v e. U_ s e. t ( f ` s ) <-> E. s e. t v e. ( f ` s ) ) |
197 |
|
velsn |
|- ( v e. { w } <-> v = w ) |
198 |
196 197
|
orbi12i |
|- ( ( v e. U_ s e. t ( f ` s ) \/ v e. { w } ) <-> ( E. s e. t v e. ( f ` s ) \/ v = w ) ) |
199 |
195 198
|
bitri |
|- ( v e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( E. s e. t v e. ( f ` s ) \/ v = w ) ) |
200 |
|
nfra1 |
|- F/ s A. s e. t X = ( U. ( f ` s ) u. s ) |
201 |
|
nfv |
|- F/ s v C_ X |
202 |
|
rsp |
|- ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( s e. t -> X = ( U. ( f ` s ) u. s ) ) ) |
203 |
|
eqimss2 |
|- ( X = ( U. ( f ` s ) u. s ) -> ( U. ( f ` s ) u. s ) C_ X ) |
204 |
|
elssuni |
|- ( v e. ( f ` s ) -> v C_ U. ( f ` s ) ) |
205 |
|
ssun3 |
|- ( v C_ U. ( f ` s ) -> v C_ ( U. ( f ` s ) u. s ) ) |
206 |
204 205
|
syl |
|- ( v e. ( f ` s ) -> v C_ ( U. ( f ` s ) u. s ) ) |
207 |
|
sstr |
|- ( ( v C_ ( U. ( f ` s ) u. s ) /\ ( U. ( f ` s ) u. s ) C_ X ) -> v C_ X ) |
208 |
207
|
expcom |
|- ( ( U. ( f ` s ) u. s ) C_ X -> ( v C_ ( U. ( f ` s ) u. s ) -> v C_ X ) ) |
209 |
203 206 208
|
syl2im |
|- ( X = ( U. ( f ` s ) u. s ) -> ( v e. ( f ` s ) -> v C_ X ) ) |
210 |
202 209
|
syl6 |
|- ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( s e. t -> ( v e. ( f ` s ) -> v C_ X ) ) ) |
211 |
200 201 210
|
rexlimd |
|- ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( E. s e. t v e. ( f ` s ) -> v C_ X ) ) |
212 |
211
|
ad2antll |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( E. s e. t v e. ( f ` s ) -> v C_ X ) ) |
213 |
|
elpwi |
|- ( u e. ~P ( fi ` x ) -> u C_ ( fi ` x ) ) |
214 |
213
|
ad2antrl |
|- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) -> u C_ ( fi ` x ) ) |
215 |
214
|
ad2antrr |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> u C_ ( fi ` x ) ) |
216 |
215 99
|
sseldd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> w e. ( fi ` x ) ) |
217 |
|
elssuni |
|- ( w e. ( fi ` x ) -> w C_ U. ( fi ` x ) ) |
218 |
216 217
|
syl |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> w C_ U. ( fi ` x ) ) |
219 |
57 58
|
ax-mp |
|- U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x ) |
220 |
60 219
|
eqtr2di |
|- ( J = ( topGen ` ( fi ` x ) ) -> U. ( fi ` x ) = U. J ) |
221 |
220 1
|
eqtr4di |
|- ( J = ( topGen ` ( fi ` x ) ) -> U. ( fi ` x ) = X ) |
222 |
221
|
3ad2ant1 |
|- ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> U. ( fi ` x ) = X ) |
223 |
222
|
ad3antrrr |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> U. ( fi ` x ) = X ) |
224 |
218 223
|
sseqtrd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> w C_ X ) |
225 |
|
sseq1 |
|- ( v = w -> ( v C_ X <-> w C_ X ) ) |
226 |
224 225
|
syl5ibrcom |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( v = w -> v C_ X ) ) |
227 |
212 226
|
jaod |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( ( E. s e. t v e. ( f ` s ) \/ v = w ) -> v C_ X ) ) |
228 |
199 227
|
biimtrid |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( v e. ( U_ s e. t ( f ` s ) u. { w } ) -> v C_ X ) ) |
229 |
228
|
ralrimiv |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> A. v e. ( U_ s e. t ( f ` s ) u. { w } ) v C_ X ) |
230 |
|
unissb |
|- ( U. ( U_ s e. t ( f ` s ) u. { w } ) C_ X <-> A. v e. ( U_ s e. t ( f ` s ) u. { w } ) v C_ X ) |
231 |
229 230
|
sylibr |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> U. ( U_ s e. t ( f ` s ) u. { w } ) C_ X ) |
232 |
194 231
|
eqssd |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> X = U. ( U_ s e. t ( f ` s ) u. { w } ) ) |
233 |
|
unieq |
|- ( b = ( U_ s e. t ( f ` s ) u. { w } ) -> U. b = U. ( U_ s e. t ( f ` s ) u. { w } ) ) |
234 |
233
|
rspceeqv |
|- ( ( ( U_ s e. t ( f ` s ) u. { w } ) e. ( ~P u i^i Fin ) /\ X = U. ( U_ s e. t ( f ` s ) u. { w } ) ) -> E. b e. ( ~P u i^i Fin ) X = U. b ) |
235 |
116 232 234
|
syl2anc |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> E. b e. ( ~P u i^i Fin ) X = U. b ) |
236 |
235
|
ex |
|- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) -> E. b e. ( ~P u i^i Fin ) X = U. b ) ) |
237 |
236
|
exlimdv |
|- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) -> E. b e. ( ~P u i^i Fin ) X = U. b ) ) |
238 |
78 88 237
|
3syld |
|- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( A. s e. t E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n -> E. b e. ( ~P u i^i Fin ) X = U. b ) ) |
239 |
5 238
|
biimtrid |
|- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( -. E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n -> E. b e. ( ~P u i^i Fin ) X = U. b ) ) |
240 |
|
dfrex2 |
|- ( E. b e. ( ~P u i^i Fin ) X = U. b <-> -. A. b e. ( ~P u i^i Fin ) -. X = U. b ) |
241 |
239 240
|
imbitrdi |
|- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( -. E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n -> -. A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) |
242 |
241
|
con4d |
|- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) |
243 |
242
|
exp32 |
|- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) -> ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) -> ( w e. u -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) ) |
244 |
243
|
com24 |
|- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> ( w e. u -> ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) ) |
245 |
244
|
exp32 |
|- ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> ( u e. ~P ( fi ` x ) -> ( a C_ u -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> ( w e. u -> ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) ) ) ) |
246 |
245
|
imp45 |
|- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( w e. u -> ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) |
247 |
246
|
imp31 |
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) |