Step |
Hyp |
Ref |
Expression |
1 |
|
df-1s |
|- 1s = ( { 0s } |s (/) ) |
2 |
1
|
fveq2i |
|- ( bday ` 1s ) = ( bday ` ( { 0s } |s (/) ) ) |
3 |
|
0sno |
|- 0s e. No |
4 |
|
snelpwi |
|- ( 0s e. No -> { 0s } e. ~P No ) |
5 |
3 4
|
ax-mp |
|- { 0s } e. ~P No |
6 |
|
nulssgt |
|- ( { 0s } e. ~P No -> { 0s } < |
7 |
5 6
|
ax-mp |
|- { 0s } < |
8 |
|
scutbdaybnd2 |
|- ( { 0s } < ( bday ` ( { 0s } |s (/) ) ) C_ suc U. ( bday " ( { 0s } u. (/) ) ) ) |
9 |
7 8
|
ax-mp |
|- ( bday ` ( { 0s } |s (/) ) ) C_ suc U. ( bday " ( { 0s } u. (/) ) ) |
10 |
|
un0 |
|- ( { 0s } u. (/) ) = { 0s } |
11 |
10
|
imaeq2i |
|- ( bday " ( { 0s } u. (/) ) ) = ( bday " { 0s } ) |
12 |
|
bdayfn |
|- bday Fn No |
13 |
|
fnsnfv |
|- ( ( bday Fn No /\ 0s e. No ) -> { ( bday ` 0s ) } = ( bday " { 0s } ) ) |
14 |
12 3 13
|
mp2an |
|- { ( bday ` 0s ) } = ( bday " { 0s } ) |
15 |
|
bday0s |
|- ( bday ` 0s ) = (/) |
16 |
15
|
sneqi |
|- { ( bday ` 0s ) } = { (/) } |
17 |
11 14 16
|
3eqtr2i |
|- ( bday " ( { 0s } u. (/) ) ) = { (/) } |
18 |
17
|
unieqi |
|- U. ( bday " ( { 0s } u. (/) ) ) = U. { (/) } |
19 |
|
0ex |
|- (/) e. _V |
20 |
19
|
unisn |
|- U. { (/) } = (/) |
21 |
18 20
|
eqtri |
|- U. ( bday " ( { 0s } u. (/) ) ) = (/) |
22 |
|
suceq |
|- ( U. ( bday " ( { 0s } u. (/) ) ) = (/) -> suc U. ( bday " ( { 0s } u. (/) ) ) = suc (/) ) |
23 |
21 22
|
ax-mp |
|- suc U. ( bday " ( { 0s } u. (/) ) ) = suc (/) |
24 |
|
df-1o |
|- 1o = suc (/) |
25 |
23 24
|
eqtr4i |
|- suc U. ( bday " ( { 0s } u. (/) ) ) = 1o |
26 |
9 25
|
sseqtri |
|- ( bday ` ( { 0s } |s (/) ) ) C_ 1o |
27 |
|
ssrab2 |
|- { x e. No | ( { 0s } < |
28 |
|
fnssintima |
|- ( ( bday Fn No /\ { x e. No | ( { 0s } < ( 1o C_ |^| ( bday " { x e. No | ( { 0s } < A. y e. { x e. No | ( { 0s } < |
29 |
12 27 28
|
mp2an |
|- ( 1o C_ |^| ( bday " { x e. No | ( { 0s } < A. y e. { x e. No | ( { 0s } < |
30 |
|
sneq |
|- ( x = y -> { x } = { y } ) |
31 |
30
|
breq2d |
|- ( x = y -> ( { 0s } < { 0s } < |
32 |
30
|
breq1d |
|- ( x = y -> ( { x } < { y } < |
33 |
31 32
|
anbi12d |
|- ( x = y -> ( ( { 0s } < ( { 0s } < |
34 |
33
|
elrab |
|- ( y e. { x e. No | ( { 0s } < ( y e. No /\ ( { 0s } < |
35 |
|
sltirr |
|- ( 0s e. No -> -. 0s |
36 |
3 35
|
ax-mp |
|- -. 0s |
37 |
|
breq2 |
|- ( y = 0s -> ( 0s 0s |
38 |
36 37
|
mtbiri |
|- ( y = 0s -> -. 0s |
39 |
38
|
necon2ai |
|- ( 0s y =/= 0s ) |
40 |
|
bday0b |
|- ( y e. No -> ( ( bday ` y ) = (/) <-> y = 0s ) ) |
41 |
40
|
necon3bid |
|- ( y e. No -> ( ( bday ` y ) =/= (/) <-> y =/= 0s ) ) |
42 |
39 41
|
syl5ibr |
|- ( y e. No -> ( 0s ( bday ` y ) =/= (/) ) ) |
43 |
|
bdayelon |
|- ( bday ` y ) e. On |
44 |
43
|
onordi |
|- Ord ( bday ` y ) |
45 |
|
ordge1n0 |
|- ( Ord ( bday ` y ) -> ( 1o C_ ( bday ` y ) <-> ( bday ` y ) =/= (/) ) ) |
46 |
44 45
|
ax-mp |
|- ( 1o C_ ( bday ` y ) <-> ( bday ` y ) =/= (/) ) |
47 |
42 46
|
syl6ibr |
|- ( y e. No -> ( 0s 1o C_ ( bday ` y ) ) ) |
48 |
|
ssltsep |
|- ( { 0s } < A. x e. { 0s } A. z e. { y } x |
49 |
|
vex |
|- y e. _V |
50 |
|
breq2 |
|- ( z = y -> ( x x |
51 |
49 50
|
ralsn |
|- ( A. z e. { y } x x |
52 |
51
|
ralbii |
|- ( A. x e. { 0s } A. z e. { y } x A. x e. { 0s } x |
53 |
3
|
elexi |
|- 0s e. _V |
54 |
|
breq1 |
|- ( x = 0s -> ( x 0s |
55 |
53 54
|
ralsn |
|- ( A. x e. { 0s } x 0s |
56 |
52 55
|
bitri |
|- ( A. x e. { 0s } A. z e. { y } x 0s |
57 |
48 56
|
sylib |
|- ( { 0s } < 0s |
58 |
47 57
|
impel |
|- ( ( y e. No /\ { 0s } < 1o C_ ( bday ` y ) ) |
59 |
58
|
adantrr |
|- ( ( y e. No /\ ( { 0s } < 1o C_ ( bday ` y ) ) |
60 |
34 59
|
sylbi |
|- ( y e. { x e. No | ( { 0s } < 1o C_ ( bday ` y ) ) |
61 |
29 60
|
mprgbir |
|- 1o C_ |^| ( bday " { x e. No | ( { 0s } < |
62 |
|
scutbday |
|- ( { 0s } < ( bday ` ( { 0s } |s (/) ) ) = |^| ( bday " { x e. No | ( { 0s } < |
63 |
7 62
|
ax-mp |
|- ( bday ` ( { 0s } |s (/) ) ) = |^| ( bday " { x e. No | ( { 0s } < |
64 |
61 63
|
sseqtrri |
|- 1o C_ ( bday ` ( { 0s } |s (/) ) ) |
65 |
26 64
|
eqssi |
|- ( bday ` ( { 0s } |s (/) ) ) = 1o |
66 |
2 65
|
eqtri |
|- ( bday ` 1s ) = 1o |