Step |
Hyp |
Ref |
Expression |
1 |
|
djueq2 |
|- ( x = B -> ( A |_| x ) = ( A |_| B ) ) |
2 |
|
oveq2 |
|- ( x = B -> ( A +o x ) = ( A +o B ) ) |
3 |
1 2
|
breq12d |
|- ( x = B -> ( ( A |_| x ) ~~ ( A +o x ) <-> ( A |_| B ) ~~ ( A +o B ) ) ) |
4 |
3
|
imbi2d |
|- ( x = B -> ( ( A e. _om -> ( A |_| x ) ~~ ( A +o x ) ) <-> ( A e. _om -> ( A |_| B ) ~~ ( A +o B ) ) ) ) |
5 |
|
djueq2 |
|- ( x = (/) -> ( A |_| x ) = ( A |_| (/) ) ) |
6 |
|
oveq2 |
|- ( x = (/) -> ( A +o x ) = ( A +o (/) ) ) |
7 |
5 6
|
breq12d |
|- ( x = (/) -> ( ( A |_| x ) ~~ ( A +o x ) <-> ( A |_| (/) ) ~~ ( A +o (/) ) ) ) |
8 |
|
djueq2 |
|- ( x = y -> ( A |_| x ) = ( A |_| y ) ) |
9 |
|
oveq2 |
|- ( x = y -> ( A +o x ) = ( A +o y ) ) |
10 |
8 9
|
breq12d |
|- ( x = y -> ( ( A |_| x ) ~~ ( A +o x ) <-> ( A |_| y ) ~~ ( A +o y ) ) ) |
11 |
|
djueq2 |
|- ( x = suc y -> ( A |_| x ) = ( A |_| suc y ) ) |
12 |
|
oveq2 |
|- ( x = suc y -> ( A +o x ) = ( A +o suc y ) ) |
13 |
11 12
|
breq12d |
|- ( x = suc y -> ( ( A |_| x ) ~~ ( A +o x ) <-> ( A |_| suc y ) ~~ ( A +o suc y ) ) ) |
14 |
|
dju0en |
|- ( A e. _om -> ( A |_| (/) ) ~~ A ) |
15 |
|
nna0 |
|- ( A e. _om -> ( A +o (/) ) = A ) |
16 |
14 15
|
breqtrrd |
|- ( A e. _om -> ( A |_| (/) ) ~~ ( A +o (/) ) ) |
17 |
|
1oex |
|- 1o e. _V |
18 |
|
djuassen |
|- ( ( A e. _om /\ y e. _om /\ 1o e. _V ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A |_| ( y |_| 1o ) ) ) |
19 |
17 18
|
mp3an3 |
|- ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A |_| ( y |_| 1o ) ) ) |
20 |
|
enrefg |
|- ( A e. _om -> A ~~ A ) |
21 |
|
nnord |
|- ( y e. _om -> Ord y ) |
22 |
|
ordirr |
|- ( Ord y -> -. y e. y ) |
23 |
21 22
|
syl |
|- ( y e. _om -> -. y e. y ) |
24 |
|
dju1en |
|- ( ( y e. _om /\ -. y e. y ) -> ( y |_| 1o ) ~~ suc y ) |
25 |
23 24
|
mpdan |
|- ( y e. _om -> ( y |_| 1o ) ~~ suc y ) |
26 |
|
djuen |
|- ( ( A ~~ A /\ ( y |_| 1o ) ~~ suc y ) -> ( A |_| ( y |_| 1o ) ) ~~ ( A |_| suc y ) ) |
27 |
20 25 26
|
syl2an |
|- ( ( A e. _om /\ y e. _om ) -> ( A |_| ( y |_| 1o ) ) ~~ ( A |_| suc y ) ) |
28 |
|
entr |
|- ( ( ( ( A |_| y ) |_| 1o ) ~~ ( A |_| ( y |_| 1o ) ) /\ ( A |_| ( y |_| 1o ) ) ~~ ( A |_| suc y ) ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A |_| suc y ) ) |
29 |
19 27 28
|
syl2anc |
|- ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A |_| suc y ) ) |
30 |
29
|
ensymd |
|- ( ( A e. _om /\ y e. _om ) -> ( A |_| suc y ) ~~ ( ( A |_| y ) |_| 1o ) ) |
31 |
17
|
enref |
|- 1o ~~ 1o |
32 |
|
djuen |
|- ( ( ( A |_| y ) ~~ ( A +o y ) /\ 1o ~~ 1o ) -> ( ( A |_| y ) |_| 1o ) ~~ ( ( A +o y ) |_| 1o ) ) |
33 |
31 32
|
mpan2 |
|- ( ( A |_| y ) ~~ ( A +o y ) -> ( ( A |_| y ) |_| 1o ) ~~ ( ( A +o y ) |_| 1o ) ) |
34 |
33
|
a1i |
|- ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) ~~ ( A +o y ) -> ( ( A |_| y ) |_| 1o ) ~~ ( ( A +o y ) |_| 1o ) ) ) |
35 |
|
nnacl |
|- ( ( A e. _om /\ y e. _om ) -> ( A +o y ) e. _om ) |
36 |
|
nnord |
|- ( ( A +o y ) e. _om -> Ord ( A +o y ) ) |
37 |
|
ordirr |
|- ( Ord ( A +o y ) -> -. ( A +o y ) e. ( A +o y ) ) |
38 |
35 36 37
|
3syl |
|- ( ( A e. _om /\ y e. _om ) -> -. ( A +o y ) e. ( A +o y ) ) |
39 |
|
dju1en |
|- ( ( ( A +o y ) e. _om /\ -. ( A +o y ) e. ( A +o y ) ) -> ( ( A +o y ) |_| 1o ) ~~ suc ( A +o y ) ) |
40 |
35 38 39
|
syl2anc |
|- ( ( A e. _om /\ y e. _om ) -> ( ( A +o y ) |_| 1o ) ~~ suc ( A +o y ) ) |
41 |
|
nnasuc |
|- ( ( A e. _om /\ y e. _om ) -> ( A +o suc y ) = suc ( A +o y ) ) |
42 |
40 41
|
breqtrrd |
|- ( ( A e. _om /\ y e. _om ) -> ( ( A +o y ) |_| 1o ) ~~ ( A +o suc y ) ) |
43 |
34 42
|
jctird |
|- ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) ~~ ( A +o y ) -> ( ( ( A |_| y ) |_| 1o ) ~~ ( ( A +o y ) |_| 1o ) /\ ( ( A +o y ) |_| 1o ) ~~ ( A +o suc y ) ) ) ) |
44 |
|
entr |
|- ( ( ( ( A |_| y ) |_| 1o ) ~~ ( ( A +o y ) |_| 1o ) /\ ( ( A +o y ) |_| 1o ) ~~ ( A +o suc y ) ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A +o suc y ) ) |
45 |
43 44
|
syl6 |
|- ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) ~~ ( A +o y ) -> ( ( A |_| y ) |_| 1o ) ~~ ( A +o suc y ) ) ) |
46 |
|
entr |
|- ( ( ( A |_| suc y ) ~~ ( ( A |_| y ) |_| 1o ) /\ ( ( A |_| y ) |_| 1o ) ~~ ( A +o suc y ) ) -> ( A |_| suc y ) ~~ ( A +o suc y ) ) |
47 |
30 45 46
|
syl6an |
|- ( ( A e. _om /\ y e. _om ) -> ( ( A |_| y ) ~~ ( A +o y ) -> ( A |_| suc y ) ~~ ( A +o suc y ) ) ) |
48 |
47
|
expcom |
|- ( y e. _om -> ( A e. _om -> ( ( A |_| y ) ~~ ( A +o y ) -> ( A |_| suc y ) ~~ ( A +o suc y ) ) ) ) |
49 |
7 10 13 16 48
|
finds2 |
|- ( x e. _om -> ( A e. _om -> ( A |_| x ) ~~ ( A +o x ) ) ) |
50 |
4 49
|
vtoclga |
|- ( B e. _om -> ( A e. _om -> ( A |_| B ) ~~ ( A +o B ) ) ) |
51 |
50
|
impcom |
|- ( ( A e. _om /\ B e. _om ) -> ( A |_| B ) ~~ ( A +o B ) ) |
52 |
|
carden2b |
|- ( ( A |_| B ) ~~ ( A +o B ) -> ( card ` ( A |_| B ) ) = ( card ` ( A +o B ) ) ) |
53 |
51 52
|
syl |
|- ( ( A e. _om /\ B e. _om ) -> ( card ` ( A |_| B ) ) = ( card ` ( A +o B ) ) ) |
54 |
|
nnacl |
|- ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om ) |
55 |
|
cardnn |
|- ( ( A +o B ) e. _om -> ( card ` ( A +o B ) ) = ( A +o B ) ) |
56 |
54 55
|
syl |
|- ( ( A e. _om /\ B e. _om ) -> ( card ` ( A +o B ) ) = ( A +o B ) ) |
57 |
53 56
|
eqtrd |
|- ( ( A e. _om /\ B e. _om ) -> ( card ` ( A |_| B ) ) = ( A +o B ) ) |