Step |
Hyp |
Ref |
Expression |
1 |
|
simp3l |
|- ( ( A < C < |
2 |
|
simp3r |
|- ( ( A < { ( A |s B ) } < |
3 |
|
simp1 |
|- ( ( A < A < |
4 |
|
scutbday |
|- ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A < |
5 |
3 4
|
syl |
|- ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A < |
6 |
|
ssltex1 |
|- ( A < A e. _V ) |
7 |
3 6
|
syl |
|- ( ( A < A e. _V ) |
8 |
7
|
ad2antrr |
|- ( ( ( ( A < A e. _V ) |
9 |
|
ssltss1 |
|- ( A < A C_ No ) |
10 |
3 9
|
syl |
|- ( ( A < A C_ No ) |
11 |
10
|
ad2antrr |
|- ( ( ( ( A < A C_ No ) |
12 |
8 11
|
elpwd |
|- ( ( ( ( A < A e. ~P No ) |
13 |
|
simpl2l |
|- ( ( ( A < A. x e. A E. y e. C x <_s y ) |
14 |
13
|
adantr |
|- ( ( ( ( A < A. x e. A E. y e. C x <_s y ) |
15 |
|
simpr |
|- ( ( ( ( A < C < |
16 |
|
cofsslt |
|- ( ( A e. ~P No /\ A. x e. A E. y e. C x <_s y /\ C < A < |
17 |
12 14 15 16
|
syl3anc |
|- ( ( ( ( A < A < |
18 |
17
|
ex |
|- ( ( ( A < ( C < A < |
19 |
|
ssltex2 |
|- ( A < B e. _V ) |
20 |
3 19
|
syl |
|- ( ( A < B e. _V ) |
21 |
20
|
ad2antrr |
|- ( ( ( ( A < B e. _V ) |
22 |
|
ssltss2 |
|- ( A < B C_ No ) |
23 |
3 22
|
syl |
|- ( ( A < B C_ No ) |
24 |
23
|
ad2antrr |
|- ( ( ( ( A < B C_ No ) |
25 |
21 24
|
elpwd |
|- ( ( ( ( A < B e. ~P No ) |
26 |
|
simpl2r |
|- ( ( ( A < A. z e. B E. w e. D w <_s z ) |
27 |
26
|
adantr |
|- ( ( ( ( A < A. z e. B E. w e. D w <_s z ) |
28 |
|
simpr |
|- ( ( ( ( A < { t } < |
29 |
|
coinitsslt |
|- ( ( B e. ~P No /\ A. z e. B E. w e. D w <_s z /\ { t } < { t } < |
30 |
25 27 28 29
|
syl3anc |
|- ( ( ( ( A < { t } < |
31 |
30
|
ex |
|- ( ( ( A < ( { t } < { t } < |
32 |
18 31
|
anim12d |
|- ( ( ( A < ( ( C < ( A < |
33 |
32
|
ss2rabdv |
|- ( ( A < { t e. No | ( C < |
34 |
|
imass2 |
|- ( { t e. No | ( C < ( bday " { t e. No | ( C < |
35 |
|
intss |
|- ( ( bday " { t e. No | ( C < |^| ( bday " { t e. No | ( A < |
36 |
33 34 35
|
3syl |
|- ( ( A < |^| ( bday " { t e. No | ( A < |
37 |
5 36
|
eqsstrd |
|- ( ( A < ( bday ` ( A |s B ) ) C_ |^| ( bday " { t e. No | ( C < |
38 |
|
bdayfn |
|- bday Fn No |
39 |
|
ssrab2 |
|- { t e. No | ( C < |
40 |
|
sneq |
|- ( t = ( A |s B ) -> { t } = { ( A |s B ) } ) |
41 |
40
|
breq2d |
|- ( t = ( A |s B ) -> ( C < C < |
42 |
40
|
breq1d |
|- ( t = ( A |s B ) -> ( { t } < { ( A |s B ) } < |
43 |
41 42
|
anbi12d |
|- ( t = ( A |s B ) -> ( ( C < ( C < |
44 |
3
|
scutcld |
|- ( ( A < ( A |s B ) e. No ) |
45 |
|
simp3 |
|- ( ( A < ( C < |
46 |
43 44 45
|
elrabd |
|- ( ( A < ( A |s B ) e. { t e. No | ( C < |
47 |
|
fnfvima |
|- ( ( bday Fn No /\ { t e. No | ( C < ( bday ` ( A |s B ) ) e. ( bday " { t e. No | ( C < |
48 |
38 39 46 47
|
mp3an12i |
|- ( ( A < ( bday ` ( A |s B ) ) e. ( bday " { t e. No | ( C < |
49 |
|
intss1 |
|- ( ( bday ` ( A |s B ) ) e. ( bday " { t e. No | ( C < |^| ( bday " { t e. No | ( C < |
50 |
48 49
|
syl |
|- ( ( A < |^| ( bday " { t e. No | ( C < |
51 |
37 50
|
eqssd |
|- ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( C < |
52 |
|
ovex |
|- ( A |s B ) e. _V |
53 |
52
|
snnz |
|- { ( A |s B ) } =/= (/) |
54 |
|
sslttr |
|- ( ( C < C < |
55 |
53 54
|
mp3an3 |
|- ( ( C < C < |
56 |
55
|
3ad2ant3 |
|- ( ( A < C < |
57 |
|
eqscut |
|- ( ( C < ( ( C |s D ) = ( A |s B ) <-> ( C < |
58 |
56 44 57
|
syl2anc |
|- ( ( A < ( ( C |s D ) = ( A |s B ) <-> ( C < |
59 |
1 2 51 58
|
mpbir3and |
|- ( ( A < ( C |s D ) = ( A |s B ) ) |
60 |
59
|
eqcomd |
|- ( ( A < ( A |s B ) = ( C |s D ) ) |