Step |
Hyp |
Ref |
Expression |
1 |
|
ssonuni |
|- ( A e. V -> ( A C_ On -> U. A e. On ) ) |
2 |
|
fveq2 |
|- ( x = y -> ( card ` x ) = ( card ` y ) ) |
3 |
|
id |
|- ( x = y -> x = y ) |
4 |
2 3
|
eqeq12d |
|- ( x = y -> ( ( card ` x ) = x <-> ( card ` y ) = y ) ) |
5 |
4
|
rspcv |
|- ( y e. A -> ( A. x e. A ( card ` x ) = x -> ( card ` y ) = y ) ) |
6 |
|
cardon |
|- ( card ` y ) e. On |
7 |
|
eleq1 |
|- ( ( card ` y ) = y -> ( ( card ` y ) e. On <-> y e. On ) ) |
8 |
6 7
|
mpbii |
|- ( ( card ` y ) = y -> y e. On ) |
9 |
5 8
|
syl6com |
|- ( A. x e. A ( card ` x ) = x -> ( y e. A -> y e. On ) ) |
10 |
9
|
ssrdv |
|- ( A. x e. A ( card ` x ) = x -> A C_ On ) |
11 |
1 10
|
impel |
|- ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> U. A e. On ) |
12 |
|
cardonle |
|- ( U. A e. On -> ( card ` U. A ) C_ U. A ) |
13 |
11 12
|
syl |
|- ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> ( card ` U. A ) C_ U. A ) |
14 |
|
cardon |
|- ( card ` U. A ) e. On |
15 |
14
|
onirri |
|- -. ( card ` U. A ) e. ( card ` U. A ) |
16 |
|
eluni |
|- ( ( card ` U. A ) e. U. A <-> E. y ( ( card ` U. A ) e. y /\ y e. A ) ) |
17 |
|
elssuni |
|- ( y e. A -> y C_ U. A ) |
18 |
|
ssdomg |
|- ( U. A e. On -> ( y C_ U. A -> y ~<_ U. A ) ) |
19 |
18
|
adantl |
|- ( ( ( card ` y ) = y /\ U. A e. On ) -> ( y C_ U. A -> y ~<_ U. A ) ) |
20 |
17 19
|
syl5 |
|- ( ( ( card ` y ) = y /\ U. A e. On ) -> ( y e. A -> y ~<_ U. A ) ) |
21 |
|
id |
|- ( ( card ` y ) = y -> ( card ` y ) = y ) |
22 |
|
onenon |
|- ( ( card ` y ) e. On -> ( card ` y ) e. dom card ) |
23 |
6 22
|
ax-mp |
|- ( card ` y ) e. dom card |
24 |
21 23
|
eqeltrrdi |
|- ( ( card ` y ) = y -> y e. dom card ) |
25 |
|
onenon |
|- ( U. A e. On -> U. A e. dom card ) |
26 |
|
carddom2 |
|- ( ( y e. dom card /\ U. A e. dom card ) -> ( ( card ` y ) C_ ( card ` U. A ) <-> y ~<_ U. A ) ) |
27 |
24 25 26
|
syl2an |
|- ( ( ( card ` y ) = y /\ U. A e. On ) -> ( ( card ` y ) C_ ( card ` U. A ) <-> y ~<_ U. A ) ) |
28 |
20 27
|
sylibrd |
|- ( ( ( card ` y ) = y /\ U. A e. On ) -> ( y e. A -> ( card ` y ) C_ ( card ` U. A ) ) ) |
29 |
|
sseq1 |
|- ( ( card ` y ) = y -> ( ( card ` y ) C_ ( card ` U. A ) <-> y C_ ( card ` U. A ) ) ) |
30 |
29
|
adantr |
|- ( ( ( card ` y ) = y /\ U. A e. On ) -> ( ( card ` y ) C_ ( card ` U. A ) <-> y C_ ( card ` U. A ) ) ) |
31 |
28 30
|
sylibd |
|- ( ( ( card ` y ) = y /\ U. A e. On ) -> ( y e. A -> y C_ ( card ` U. A ) ) ) |
32 |
|
ssel |
|- ( y C_ ( card ` U. A ) -> ( ( card ` U. A ) e. y -> ( card ` U. A ) e. ( card ` U. A ) ) ) |
33 |
31 32
|
syl6 |
|- ( ( ( card ` y ) = y /\ U. A e. On ) -> ( y e. A -> ( ( card ` U. A ) e. y -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) |
34 |
33
|
ex |
|- ( ( card ` y ) = y -> ( U. A e. On -> ( y e. A -> ( ( card ` U. A ) e. y -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) ) |
35 |
34
|
com3r |
|- ( y e. A -> ( ( card ` y ) = y -> ( U. A e. On -> ( ( card ` U. A ) e. y -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) ) |
36 |
5 35
|
syld |
|- ( y e. A -> ( A. x e. A ( card ` x ) = x -> ( U. A e. On -> ( ( card ` U. A ) e. y -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) ) |
37 |
36
|
com4r |
|- ( ( card ` U. A ) e. y -> ( y e. A -> ( A. x e. A ( card ` x ) = x -> ( U. A e. On -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) ) |
38 |
37
|
imp |
|- ( ( ( card ` U. A ) e. y /\ y e. A ) -> ( A. x e. A ( card ` x ) = x -> ( U. A e. On -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) |
39 |
38
|
exlimiv |
|- ( E. y ( ( card ` U. A ) e. y /\ y e. A ) -> ( A. x e. A ( card ` x ) = x -> ( U. A e. On -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) |
40 |
16 39
|
sylbi |
|- ( ( card ` U. A ) e. U. A -> ( A. x e. A ( card ` x ) = x -> ( U. A e. On -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) |
41 |
40
|
com13 |
|- ( U. A e. On -> ( A. x e. A ( card ` x ) = x -> ( ( card ` U. A ) e. U. A -> ( card ` U. A ) e. ( card ` U. A ) ) ) ) |
42 |
41
|
imp |
|- ( ( U. A e. On /\ A. x e. A ( card ` x ) = x ) -> ( ( card ` U. A ) e. U. A -> ( card ` U. A ) e. ( card ` U. A ) ) ) |
43 |
11 42
|
sylancom |
|- ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> ( ( card ` U. A ) e. U. A -> ( card ` U. A ) e. ( card ` U. A ) ) ) |
44 |
15 43
|
mtoi |
|- ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> -. ( card ` U. A ) e. U. A ) |
45 |
14
|
onordi |
|- Ord ( card ` U. A ) |
46 |
|
eloni |
|- ( U. A e. On -> Ord U. A ) |
47 |
11 46
|
syl |
|- ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> Ord U. A ) |
48 |
|
ordtri4 |
|- ( ( Ord ( card ` U. A ) /\ Ord U. A ) -> ( ( card ` U. A ) = U. A <-> ( ( card ` U. A ) C_ U. A /\ -. ( card ` U. A ) e. U. A ) ) ) |
49 |
45 47 48
|
sylancr |
|- ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> ( ( card ` U. A ) = U. A <-> ( ( card ` U. A ) C_ U. A /\ -. ( card ` U. A ) e. U. A ) ) ) |
50 |
13 44 49
|
mpbir2and |
|- ( ( A e. V /\ A. x e. A ( card ` x ) = x ) -> ( card ` U. A ) = U. A ) |
51 |
50
|
ex |
|- ( A e. V -> ( A. x e. A ( card ` x ) = x -> ( card ` U. A ) = U. A ) ) |