Step |
Hyp |
Ref |
Expression |
1 |
|
cfslb.1 |
|- A e. _V |
2 |
|
limord |
|- ( Lim A -> Ord A ) |
3 |
|
ordsson |
|- ( Ord A -> A C_ On ) |
4 |
|
sstr |
|- ( ( x C_ A /\ A C_ On ) -> x C_ On ) |
5 |
4
|
expcom |
|- ( A C_ On -> ( x C_ A -> x C_ On ) ) |
6 |
2 3 5
|
3syl |
|- ( Lim A -> ( x C_ A -> x C_ On ) ) |
7 |
|
onsucuni |
|- ( x C_ On -> x C_ suc U. x ) |
8 |
6 7
|
syl6 |
|- ( Lim A -> ( x C_ A -> x C_ suc U. x ) ) |
9 |
8
|
adantrd |
|- ( Lim A -> ( ( x C_ A /\ x ~< ( cf ` A ) ) -> x C_ suc U. x ) ) |
10 |
9
|
ralimdv |
|- ( Lim A -> ( A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) -> A. x e. B x C_ suc U. x ) ) |
11 |
|
uniiun |
|- U. B = U_ x e. B x |
12 |
|
ss2iun |
|- ( A. x e. B x C_ suc U. x -> U_ x e. B x C_ U_ x e. B suc U. x ) |
13 |
11 12
|
eqsstrid |
|- ( A. x e. B x C_ suc U. x -> U. B C_ U_ x e. B suc U. x ) |
14 |
10 13
|
syl6 |
|- ( Lim A -> ( A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) -> U. B C_ U_ x e. B suc U. x ) ) |
15 |
14
|
imp |
|- ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> U. B C_ U_ x e. B suc U. x ) |
16 |
1
|
cfslbn |
|- ( ( Lim A /\ x C_ A /\ x ~< ( cf ` A ) ) -> U. x e. A ) |
17 |
16
|
3expib |
|- ( Lim A -> ( ( x C_ A /\ x ~< ( cf ` A ) ) -> U. x e. A ) ) |
18 |
|
ordsucss |
|- ( Ord A -> ( U. x e. A -> suc U. x C_ A ) ) |
19 |
2 17 18
|
sylsyld |
|- ( Lim A -> ( ( x C_ A /\ x ~< ( cf ` A ) ) -> suc U. x C_ A ) ) |
20 |
19
|
ralimdv |
|- ( Lim A -> ( A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) -> A. x e. B suc U. x C_ A ) ) |
21 |
|
iunss |
|- ( U_ x e. B suc U. x C_ A <-> A. x e. B suc U. x C_ A ) |
22 |
20 21
|
syl6ibr |
|- ( Lim A -> ( A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) -> U_ x e. B suc U. x C_ A ) ) |
23 |
22
|
imp |
|- ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> U_ x e. B suc U. x C_ A ) |
24 |
|
sseq1 |
|- ( U. B = A -> ( U. B C_ U_ x e. B suc U. x <-> A C_ U_ x e. B suc U. x ) ) |
25 |
|
eqss |
|- ( U_ x e. B suc U. x = A <-> ( U_ x e. B suc U. x C_ A /\ A C_ U_ x e. B suc U. x ) ) |
26 |
25
|
simplbi2com |
|- ( A C_ U_ x e. B suc U. x -> ( U_ x e. B suc U. x C_ A -> U_ x e. B suc U. x = A ) ) |
27 |
24 26
|
syl6bi |
|- ( U. B = A -> ( U. B C_ U_ x e. B suc U. x -> ( U_ x e. B suc U. x C_ A -> U_ x e. B suc U. x = A ) ) ) |
28 |
27
|
com3l |
|- ( U. B C_ U_ x e. B suc U. x -> ( U_ x e. B suc U. x C_ A -> ( U. B = A -> U_ x e. B suc U. x = A ) ) ) |
29 |
15 23 28
|
sylc |
|- ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( U. B = A -> U_ x e. B suc U. x = A ) ) |
30 |
|
limsuc |
|- ( Lim A -> ( U. x e. A <-> suc U. x e. A ) ) |
31 |
17 30
|
sylibd |
|- ( Lim A -> ( ( x C_ A /\ x ~< ( cf ` A ) ) -> suc U. x e. A ) ) |
32 |
31
|
ralimdv |
|- ( Lim A -> ( A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) -> A. x e. B suc U. x e. A ) ) |
33 |
32
|
imp |
|- ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> A. x e. B suc U. x e. A ) |
34 |
|
r19.29 |
|- ( ( A. x e. B suc U. x e. A /\ E. x e. B y = suc U. x ) -> E. x e. B ( suc U. x e. A /\ y = suc U. x ) ) |
35 |
|
eleq1 |
|- ( y = suc U. x -> ( y e. A <-> suc U. x e. A ) ) |
36 |
35
|
biimparc |
|- ( ( suc U. x e. A /\ y = suc U. x ) -> y e. A ) |
37 |
36
|
rexlimivw |
|- ( E. x e. B ( suc U. x e. A /\ y = suc U. x ) -> y e. A ) |
38 |
34 37
|
syl |
|- ( ( A. x e. B suc U. x e. A /\ E. x e. B y = suc U. x ) -> y e. A ) |
39 |
38
|
ex |
|- ( A. x e. B suc U. x e. A -> ( E. x e. B y = suc U. x -> y e. A ) ) |
40 |
33 39
|
syl |
|- ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( E. x e. B y = suc U. x -> y e. A ) ) |
41 |
40
|
abssdv |
|- ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> { y | E. x e. B y = suc U. x } C_ A ) |
42 |
|
vuniex |
|- U. x e. _V |
43 |
42
|
sucex |
|- suc U. x e. _V |
44 |
43
|
dfiun2 |
|- U_ x e. B suc U. x = U. { y | E. x e. B y = suc U. x } |
45 |
44
|
eqeq1i |
|- ( U_ x e. B suc U. x = A <-> U. { y | E. x e. B y = suc U. x } = A ) |
46 |
1
|
cfslb |
|- ( ( Lim A /\ { y | E. x e. B y = suc U. x } C_ A /\ U. { y | E. x e. B y = suc U. x } = A ) -> ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } ) |
47 |
46
|
3expia |
|- ( ( Lim A /\ { y | E. x e. B y = suc U. x } C_ A ) -> ( U. { y | E. x e. B y = suc U. x } = A -> ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } ) ) |
48 |
45 47
|
syl5bi |
|- ( ( Lim A /\ { y | E. x e. B y = suc U. x } C_ A ) -> ( U_ x e. B suc U. x = A -> ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } ) ) |
49 |
41 48
|
syldan |
|- ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( U_ x e. B suc U. x = A -> ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } ) ) |
50 |
|
eqid |
|- ( x e. B |-> suc U. x ) = ( x e. B |-> suc U. x ) |
51 |
50
|
rnmpt |
|- ran ( x e. B |-> suc U. x ) = { y | E. x e. B y = suc U. x } |
52 |
43 50
|
fnmpti |
|- ( x e. B |-> suc U. x ) Fn B |
53 |
|
dffn4 |
|- ( ( x e. B |-> suc U. x ) Fn B <-> ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) ) |
54 |
52 53
|
mpbi |
|- ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) |
55 |
|
relsdom |
|- Rel ~< |
56 |
55
|
brrelex1i |
|- ( B ~< ( cf ` A ) -> B e. _V ) |
57 |
|
breq1 |
|- ( y = B -> ( y ~< ( cf ` A ) <-> B ~< ( cf ` A ) ) ) |
58 |
|
foeq2 |
|- ( y = B -> ( ( x e. B |-> suc U. x ) : y -onto-> ran ( x e. B |-> suc U. x ) <-> ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) ) ) |
59 |
|
breq2 |
|- ( y = B -> ( ran ( x e. B |-> suc U. x ) ~<_ y <-> ran ( x e. B |-> suc U. x ) ~<_ B ) ) |
60 |
58 59
|
imbi12d |
|- ( y = B -> ( ( ( x e. B |-> suc U. x ) : y -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ y ) <-> ( ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ B ) ) ) |
61 |
57 60
|
imbi12d |
|- ( y = B -> ( ( y ~< ( cf ` A ) -> ( ( x e. B |-> suc U. x ) : y -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ y ) ) <-> ( B ~< ( cf ` A ) -> ( ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ B ) ) ) ) |
62 |
|
cfon |
|- ( cf ` A ) e. On |
63 |
|
sdomdom |
|- ( y ~< ( cf ` A ) -> y ~<_ ( cf ` A ) ) |
64 |
|
ondomen |
|- ( ( ( cf ` A ) e. On /\ y ~<_ ( cf ` A ) ) -> y e. dom card ) |
65 |
62 63 64
|
sylancr |
|- ( y ~< ( cf ` A ) -> y e. dom card ) |
66 |
|
fodomnum |
|- ( y e. dom card -> ( ( x e. B |-> suc U. x ) : y -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ y ) ) |
67 |
65 66
|
syl |
|- ( y ~< ( cf ` A ) -> ( ( x e. B |-> suc U. x ) : y -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ y ) ) |
68 |
61 67
|
vtoclg |
|- ( B e. _V -> ( B ~< ( cf ` A ) -> ( ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ B ) ) ) |
69 |
56 68
|
mpcom |
|- ( B ~< ( cf ` A ) -> ( ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ B ) ) |
70 |
54 69
|
mpi |
|- ( B ~< ( cf ` A ) -> ran ( x e. B |-> suc U. x ) ~<_ B ) |
71 |
51 70
|
eqbrtrrid |
|- ( B ~< ( cf ` A ) -> { y | E. x e. B y = suc U. x } ~<_ B ) |
72 |
|
domtr |
|- ( ( ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } /\ { y | E. x e. B y = suc U. x } ~<_ B ) -> ( cf ` A ) ~<_ B ) |
73 |
71 72
|
sylan2 |
|- ( ( ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } /\ B ~< ( cf ` A ) ) -> ( cf ` A ) ~<_ B ) |
74 |
|
domnsym |
|- ( ( cf ` A ) ~<_ B -> -. B ~< ( cf ` A ) ) |
75 |
73 74
|
syl |
|- ( ( ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } /\ B ~< ( cf ` A ) ) -> -. B ~< ( cf ` A ) ) |
76 |
75
|
pm2.01da |
|- ( ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } -> -. B ~< ( cf ` A ) ) |
77 |
76
|
a1i |
|- ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } -> -. B ~< ( cf ` A ) ) ) |
78 |
29 49 77
|
3syld |
|- ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( U. B = A -> -. B ~< ( cf ` A ) ) ) |
79 |
78
|
necon2ad |
|- ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( B ~< ( cf ` A ) -> U. B =/= A ) ) |