Step |
Hyp |
Ref |
Expression |
1 |
|
2ndcsep.1 |
|- X = U. J |
2 |
|
is2ndc |
|- ( J e. 2ndc <-> E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = J ) ) |
3 |
|
vex |
|- b e. _V |
4 |
|
difss |
|- ( b \ { (/) } ) C_ b |
5 |
|
ssdomg |
|- ( b e. _V -> ( ( b \ { (/) } ) C_ b -> ( b \ { (/) } ) ~<_ b ) ) |
6 |
3 4 5
|
mp2 |
|- ( b \ { (/) } ) ~<_ b |
7 |
|
simpr |
|- ( ( b e. TopBases /\ b ~<_ _om ) -> b ~<_ _om ) |
8 |
|
domtr |
|- ( ( ( b \ { (/) } ) ~<_ b /\ b ~<_ _om ) -> ( b \ { (/) } ) ~<_ _om ) |
9 |
6 7 8
|
sylancr |
|- ( ( b e. TopBases /\ b ~<_ _om ) -> ( b \ { (/) } ) ~<_ _om ) |
10 |
|
eldifsn |
|- ( y e. ( b \ { (/) } ) <-> ( y e. b /\ y =/= (/) ) ) |
11 |
|
n0 |
|- ( y =/= (/) <-> E. z z e. y ) |
12 |
|
elunii |
|- ( ( z e. y /\ y e. b ) -> z e. U. b ) |
13 |
|
simpl |
|- ( ( z e. y /\ y e. b ) -> z e. y ) |
14 |
12 13
|
jca |
|- ( ( z e. y /\ y e. b ) -> ( z e. U. b /\ z e. y ) ) |
15 |
14
|
expcom |
|- ( y e. b -> ( z e. y -> ( z e. U. b /\ z e. y ) ) ) |
16 |
15
|
eximdv |
|- ( y e. b -> ( E. z z e. y -> E. z ( z e. U. b /\ z e. y ) ) ) |
17 |
16
|
imp |
|- ( ( y e. b /\ E. z z e. y ) -> E. z ( z e. U. b /\ z e. y ) ) |
18 |
|
df-rex |
|- ( E. z e. U. b z e. y <-> E. z ( z e. U. b /\ z e. y ) ) |
19 |
17 18
|
sylibr |
|- ( ( y e. b /\ E. z z e. y ) -> E. z e. U. b z e. y ) |
20 |
11 19
|
sylan2b |
|- ( ( y e. b /\ y =/= (/) ) -> E. z e. U. b z e. y ) |
21 |
10 20
|
sylbi |
|- ( y e. ( b \ { (/) } ) -> E. z e. U. b z e. y ) |
22 |
21
|
rgen |
|- A. y e. ( b \ { (/) } ) E. z e. U. b z e. y |
23 |
|
vuniex |
|- U. b e. _V |
24 |
|
eleq1 |
|- ( z = ( f ` y ) -> ( z e. y <-> ( f ` y ) e. y ) ) |
25 |
23 24
|
axcc4dom |
|- ( ( ( b \ { (/) } ) ~<_ _om /\ A. y e. ( b \ { (/) } ) E. z e. U. b z e. y ) -> E. f ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) |
26 |
9 22 25
|
sylancl |
|- ( ( b e. TopBases /\ b ~<_ _om ) -> E. f ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) |
27 |
|
frn |
|- ( f : ( b \ { (/) } ) --> U. b -> ran f C_ U. b ) |
28 |
27
|
ad2antrl |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ran f C_ U. b ) |
29 |
|
vex |
|- f e. _V |
30 |
29
|
rnex |
|- ran f e. _V |
31 |
30
|
elpw |
|- ( ran f e. ~P U. b <-> ran f C_ U. b ) |
32 |
28 31
|
sylibr |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ran f e. ~P U. b ) |
33 |
|
omelon |
|- _om e. On |
34 |
7
|
adantr |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> b ~<_ _om ) |
35 |
|
ondomen |
|- ( ( _om e. On /\ b ~<_ _om ) -> b e. dom card ) |
36 |
33 34 35
|
sylancr |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> b e. dom card ) |
37 |
|
ssnum |
|- ( ( b e. dom card /\ ( b \ { (/) } ) C_ b ) -> ( b \ { (/) } ) e. dom card ) |
38 |
36 4 37
|
sylancl |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ( b \ { (/) } ) e. dom card ) |
39 |
|
ffn |
|- ( f : ( b \ { (/) } ) --> U. b -> f Fn ( b \ { (/) } ) ) |
40 |
39
|
ad2antrl |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> f Fn ( b \ { (/) } ) ) |
41 |
|
dffn4 |
|- ( f Fn ( b \ { (/) } ) <-> f : ( b \ { (/) } ) -onto-> ran f ) |
42 |
40 41
|
sylib |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> f : ( b \ { (/) } ) -onto-> ran f ) |
43 |
|
fodomnum |
|- ( ( b \ { (/) } ) e. dom card -> ( f : ( b \ { (/) } ) -onto-> ran f -> ran f ~<_ ( b \ { (/) } ) ) ) |
44 |
38 42 43
|
sylc |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ran f ~<_ ( b \ { (/) } ) ) |
45 |
9
|
adantr |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ( b \ { (/) } ) ~<_ _om ) |
46 |
|
domtr |
|- ( ( ran f ~<_ ( b \ { (/) } ) /\ ( b \ { (/) } ) ~<_ _om ) -> ran f ~<_ _om ) |
47 |
44 45 46
|
syl2anc |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ran f ~<_ _om ) |
48 |
|
tgcl |
|- ( b e. TopBases -> ( topGen ` b ) e. Top ) |
49 |
48
|
ad2antrr |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ( topGen ` b ) e. Top ) |
50 |
|
unitg |
|- ( b e. _V -> U. ( topGen ` b ) = U. b ) |
51 |
50
|
elv |
|- U. ( topGen ` b ) = U. b |
52 |
51
|
eqcomi |
|- U. b = U. ( topGen ` b ) |
53 |
52
|
clsss3 |
|- ( ( ( topGen ` b ) e. Top /\ ran f C_ U. b ) -> ( ( cls ` ( topGen ` b ) ) ` ran f ) C_ U. b ) |
54 |
49 28 53
|
syl2anc |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ( ( cls ` ( topGen ` b ) ) ` ran f ) C_ U. b ) |
55 |
|
ne0i |
|- ( x e. y -> y =/= (/) ) |
56 |
55
|
anim2i |
|- ( ( y e. b /\ x e. y ) -> ( y e. b /\ y =/= (/) ) ) |
57 |
56 10
|
sylibr |
|- ( ( y e. b /\ x e. y ) -> y e. ( b \ { (/) } ) ) |
58 |
|
fnfvelrn |
|- ( ( f Fn ( b \ { (/) } ) /\ y e. ( b \ { (/) } ) ) -> ( f ` y ) e. ran f ) |
59 |
39 58
|
sylan |
|- ( ( f : ( b \ { (/) } ) --> U. b /\ y e. ( b \ { (/) } ) ) -> ( f ` y ) e. ran f ) |
60 |
|
inelcm |
|- ( ( ( f ` y ) e. y /\ ( f ` y ) e. ran f ) -> ( y i^i ran f ) =/= (/) ) |
61 |
60
|
expcom |
|- ( ( f ` y ) e. ran f -> ( ( f ` y ) e. y -> ( y i^i ran f ) =/= (/) ) ) |
62 |
59 61
|
syl |
|- ( ( f : ( b \ { (/) } ) --> U. b /\ y e. ( b \ { (/) } ) ) -> ( ( f ` y ) e. y -> ( y i^i ran f ) =/= (/) ) ) |
63 |
62
|
ex |
|- ( f : ( b \ { (/) } ) --> U. b -> ( y e. ( b \ { (/) } ) -> ( ( f ` y ) e. y -> ( y i^i ran f ) =/= (/) ) ) ) |
64 |
63
|
a2d |
|- ( f : ( b \ { (/) } ) --> U. b -> ( ( y e. ( b \ { (/) } ) -> ( f ` y ) e. y ) -> ( y e. ( b \ { (/) } ) -> ( y i^i ran f ) =/= (/) ) ) ) |
65 |
57 64
|
syl7 |
|- ( f : ( b \ { (/) } ) --> U. b -> ( ( y e. ( b \ { (/) } ) -> ( f ` y ) e. y ) -> ( ( y e. b /\ x e. y ) -> ( y i^i ran f ) =/= (/) ) ) ) |
66 |
65
|
exp4a |
|- ( f : ( b \ { (/) } ) --> U. b -> ( ( y e. ( b \ { (/) } ) -> ( f ` y ) e. y ) -> ( y e. b -> ( x e. y -> ( y i^i ran f ) =/= (/) ) ) ) ) |
67 |
66
|
ralimdv2 |
|- ( f : ( b \ { (/) } ) --> U. b -> ( A. y e. ( b \ { (/) } ) ( f ` y ) e. y -> A. y e. b ( x e. y -> ( y i^i ran f ) =/= (/) ) ) ) |
68 |
67
|
imp |
|- ( ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) -> A. y e. b ( x e. y -> ( y i^i ran f ) =/= (/) ) ) |
69 |
68
|
ad2antlr |
|- ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> A. y e. b ( x e. y -> ( y i^i ran f ) =/= (/) ) ) |
70 |
|
eqidd |
|- ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> ( topGen ` b ) = ( topGen ` b ) ) |
71 |
52
|
a1i |
|- ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> U. b = U. ( topGen ` b ) ) |
72 |
|
simplll |
|- ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> b e. TopBases ) |
73 |
28
|
adantr |
|- ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> ran f C_ U. b ) |
74 |
|
simpr |
|- ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> x e. U. b ) |
75 |
70 71 72 73 74
|
elcls3 |
|- ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> ( x e. ( ( cls ` ( topGen ` b ) ) ` ran f ) <-> A. y e. b ( x e. y -> ( y i^i ran f ) =/= (/) ) ) ) |
76 |
69 75
|
mpbird |
|- ( ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) /\ x e. U. b ) -> x e. ( ( cls ` ( topGen ` b ) ) ` ran f ) ) |
77 |
54 76
|
eqelssd |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> ( ( cls ` ( topGen ` b ) ) ` ran f ) = U. b ) |
78 |
|
breq1 |
|- ( x = ran f -> ( x ~<_ _om <-> ran f ~<_ _om ) ) |
79 |
|
fveqeq2 |
|- ( x = ran f -> ( ( ( cls ` ( topGen ` b ) ) ` x ) = U. b <-> ( ( cls ` ( topGen ` b ) ) ` ran f ) = U. b ) ) |
80 |
78 79
|
anbi12d |
|- ( x = ran f -> ( ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) <-> ( ran f ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` ran f ) = U. b ) ) ) |
81 |
80
|
rspcev |
|- ( ( ran f e. ~P U. b /\ ( ran f ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` ran f ) = U. b ) ) -> E. x e. ~P U. b ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) ) |
82 |
32 47 77 81
|
syl12anc |
|- ( ( ( b e. TopBases /\ b ~<_ _om ) /\ ( f : ( b \ { (/) } ) --> U. b /\ A. y e. ( b \ { (/) } ) ( f ` y ) e. y ) ) -> E. x e. ~P U. b ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) ) |
83 |
26 82
|
exlimddv |
|- ( ( b e. TopBases /\ b ~<_ _om ) -> E. x e. ~P U. b ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) ) |
84 |
|
unieq |
|- ( ( topGen ` b ) = J -> U. ( topGen ` b ) = U. J ) |
85 |
84 52 1
|
3eqtr4g |
|- ( ( topGen ` b ) = J -> U. b = X ) |
86 |
85
|
pweqd |
|- ( ( topGen ` b ) = J -> ~P U. b = ~P X ) |
87 |
|
fveq2 |
|- ( ( topGen ` b ) = J -> ( cls ` ( topGen ` b ) ) = ( cls ` J ) ) |
88 |
87
|
fveq1d |
|- ( ( topGen ` b ) = J -> ( ( cls ` ( topGen ` b ) ) ` x ) = ( ( cls ` J ) ` x ) ) |
89 |
88 85
|
eqeq12d |
|- ( ( topGen ` b ) = J -> ( ( ( cls ` ( topGen ` b ) ) ` x ) = U. b <-> ( ( cls ` J ) ` x ) = X ) ) |
90 |
89
|
anbi2d |
|- ( ( topGen ` b ) = J -> ( ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) <-> ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) ) |
91 |
86 90
|
rexeqbidv |
|- ( ( topGen ` b ) = J -> ( E. x e. ~P U. b ( x ~<_ _om /\ ( ( cls ` ( topGen ` b ) ) ` x ) = U. b ) <-> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) ) |
92 |
83 91
|
syl5ibcom |
|- ( ( b e. TopBases /\ b ~<_ _om ) -> ( ( topGen ` b ) = J -> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) ) |
93 |
92
|
impr |
|- ( ( b e. TopBases /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) |
94 |
93
|
rexlimiva |
|- ( E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = J ) -> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) |
95 |
2 94
|
sylbi |
|- ( J e. 2ndc -> E. x e. ~P X ( x ~<_ _om /\ ( ( cls ` J ) ` x ) = X ) ) |