Step |
Hyp |
Ref |
Expression |
1 |
|
cfval |
|- ( A e. On -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) |
2 |
1
|
eqeq1d |
|- ( A e. On -> ( ( cf ` A ) = (/) <-> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) ) ) |
3 |
|
vex |
|- v e. _V |
4 |
|
eqeq1 |
|- ( x = v -> ( x = ( card ` y ) <-> v = ( card ` y ) ) ) |
5 |
4
|
anbi1d |
|- ( x = v -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
6 |
5
|
exbidv |
|- ( x = v -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
7 |
3 6
|
elab |
|- ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } <-> E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) |
8 |
|
fveq2 |
|- ( v = ( card ` y ) -> ( card ` v ) = ( card ` ( card ` y ) ) ) |
9 |
|
cardidm |
|- ( card ` ( card ` y ) ) = ( card ` y ) |
10 |
8 9
|
eqtrdi |
|- ( v = ( card ` y ) -> ( card ` v ) = ( card ` y ) ) |
11 |
|
eqeq2 |
|- ( v = ( card ` y ) -> ( ( card ` v ) = v <-> ( card ` v ) = ( card ` y ) ) ) |
12 |
10 11
|
mpbird |
|- ( v = ( card ` y ) -> ( card ` v ) = v ) |
13 |
12
|
adantr |
|- ( ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( card ` v ) = v ) |
14 |
13
|
exlimiv |
|- ( E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( card ` v ) = v ) |
15 |
7 14
|
sylbi |
|- ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> ( card ` v ) = v ) |
16 |
|
cardon |
|- ( card ` v ) e. On |
17 |
15 16
|
eqeltrrdi |
|- ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> v e. On ) |
18 |
17
|
ssriv |
|- { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ On |
19 |
|
onint0 |
|- ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ On -> ( |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) <-> (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) ) |
20 |
18 19
|
ax-mp |
|- ( |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) <-> (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) |
21 |
|
0ex |
|- (/) e. _V |
22 |
|
eqeq1 |
|- ( x = (/) -> ( x = ( card ` y ) <-> (/) = ( card ` y ) ) ) |
23 |
22
|
anbi1d |
|- ( x = (/) -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
24 |
23
|
exbidv |
|- ( x = (/) -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> E. y ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
25 |
21 24
|
elab |
|- ( (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } <-> E. y ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) |
26 |
|
onss |
|- ( A e. On -> A C_ On ) |
27 |
|
sstr |
|- ( ( y C_ A /\ A C_ On ) -> y C_ On ) |
28 |
27
|
ancoms |
|- ( ( A C_ On /\ y C_ A ) -> y C_ On ) |
29 |
26 28
|
sylan |
|- ( ( A e. On /\ y C_ A ) -> y C_ On ) |
30 |
29
|
3adant2 |
|- ( ( A e. On /\ (/) = ( card ` y ) /\ y C_ A ) -> y C_ On ) |
31 |
30
|
3adant3r |
|- ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> y C_ On ) |
32 |
|
simp2 |
|- ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> (/) = ( card ` y ) ) |
33 |
|
simp3 |
|- ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) |
34 |
|
eqcom |
|- ( (/) = ( card ` y ) <-> ( card ` y ) = (/) ) |
35 |
|
vex |
|- y e. _V |
36 |
|
onssnum |
|- ( ( y e. _V /\ y C_ On ) -> y e. dom card ) |
37 |
35 36
|
mpan |
|- ( y C_ On -> y e. dom card ) |
38 |
|
cardnueq0 |
|- ( y e. dom card -> ( ( card ` y ) = (/) <-> y = (/) ) ) |
39 |
37 38
|
syl |
|- ( y C_ On -> ( ( card ` y ) = (/) <-> y = (/) ) ) |
40 |
34 39
|
syl5bb |
|- ( y C_ On -> ( (/) = ( card ` y ) <-> y = (/) ) ) |
41 |
40
|
biimpa |
|- ( ( y C_ On /\ (/) = ( card ` y ) ) -> y = (/) ) |
42 |
|
sseq1 |
|- ( y = (/) -> ( y C_ A <-> (/) C_ A ) ) |
43 |
|
rexeq |
|- ( y = (/) -> ( E. w e. y z C_ w <-> E. w e. (/) z C_ w ) ) |
44 |
43
|
ralbidv |
|- ( y = (/) -> ( A. z e. A E. w e. y z C_ w <-> A. z e. A E. w e. (/) z C_ w ) ) |
45 |
42 44
|
anbi12d |
|- ( y = (/) -> ( ( y C_ A /\ A. z e. A E. w e. y z C_ w ) <-> ( (/) C_ A /\ A. z e. A E. w e. (/) z C_ w ) ) ) |
46 |
45
|
biimpa |
|- ( ( y = (/) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( (/) C_ A /\ A. z e. A E. w e. (/) z C_ w ) ) |
47 |
41 46
|
sylan |
|- ( ( ( y C_ On /\ (/) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( (/) C_ A /\ A. z e. A E. w e. (/) z C_ w ) ) |
48 |
|
rex0 |
|- -. E. w e. (/) z C_ w |
49 |
48
|
rgenw |
|- A. z e. A -. E. w e. (/) z C_ w |
50 |
|
r19.2z |
|- ( ( A =/= (/) /\ A. z e. A -. E. w e. (/) z C_ w ) -> E. z e. A -. E. w e. (/) z C_ w ) |
51 |
49 50
|
mpan2 |
|- ( A =/= (/) -> E. z e. A -. E. w e. (/) z C_ w ) |
52 |
|
rexnal |
|- ( E. z e. A -. E. w e. (/) z C_ w <-> -. A. z e. A E. w e. (/) z C_ w ) |
53 |
51 52
|
sylib |
|- ( A =/= (/) -> -. A. z e. A E. w e. (/) z C_ w ) |
54 |
53
|
necon4ai |
|- ( A. z e. A E. w e. (/) z C_ w -> A = (/) ) |
55 |
47 54
|
simpl2im |
|- ( ( ( y C_ On /\ (/) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) ) |
56 |
31 32 33 55
|
syl21anc |
|- ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) ) |
57 |
56
|
3expib |
|- ( A e. On -> ( ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) ) ) |
58 |
57
|
exlimdv |
|- ( A e. On -> ( E. y ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) ) ) |
59 |
25 58
|
syl5bi |
|- ( A e. On -> ( (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> A = (/) ) ) |
60 |
20 59
|
syl5bi |
|- ( A e. On -> ( |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) -> A = (/) ) ) |
61 |
2 60
|
sylbid |
|- ( A e. On -> ( ( cf ` A ) = (/) -> A = (/) ) ) |
62 |
|
fveq2 |
|- ( A = (/) -> ( cf ` A ) = ( cf ` (/) ) ) |
63 |
|
cf0 |
|- ( cf ` (/) ) = (/) |
64 |
62 63
|
eqtrdi |
|- ( A = (/) -> ( cf ` A ) = (/) ) |
65 |
61 64
|
impbid1 |
|- ( A e. On -> ( ( cf ` A ) = (/) <-> A = (/) ) ) |