Step |
Hyp |
Ref |
Expression |
1 |
|
djueq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝐴 ⊔ 𝑥 ) = ( 𝐴 ⊔ 𝐵 ) ) |
2 |
|
oveq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝐵 ) ) |
3 |
1 2
|
breq12d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ⊔ 𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ↔ ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 +o 𝐵 ) ) ) |
4 |
3
|
imbi2d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ ω → ( 𝐴 ⊔ 𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 +o 𝐵 ) ) ) ) |
5 |
|
djueq2 |
⊢ ( 𝑥 = ∅ → ( 𝐴 ⊔ 𝑥 ) = ( 𝐴 ⊔ ∅ ) ) |
6 |
|
oveq2 |
⊢ ( 𝑥 = ∅ → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o ∅ ) ) |
7 |
5 6
|
breq12d |
⊢ ( 𝑥 = ∅ → ( ( 𝐴 ⊔ 𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ↔ ( 𝐴 ⊔ ∅ ) ≈ ( 𝐴 +o ∅ ) ) ) |
8 |
|
djueq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐴 ⊔ 𝑥 ) = ( 𝐴 ⊔ 𝑦 ) ) |
9 |
|
oveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) ) |
10 |
8 9
|
breq12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ⊔ 𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ↔ ( 𝐴 ⊔ 𝑦 ) ≈ ( 𝐴 +o 𝑦 ) ) ) |
11 |
|
djueq2 |
⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ⊔ 𝑥 ) = ( 𝐴 ⊔ suc 𝑦 ) ) |
12 |
|
oveq2 |
⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o suc 𝑦 ) ) |
13 |
11 12
|
breq12d |
⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ⊔ 𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ↔ ( 𝐴 ⊔ suc 𝑦 ) ≈ ( 𝐴 +o suc 𝑦 ) ) ) |
14 |
|
dju0en |
⊢ ( 𝐴 ∈ ω → ( 𝐴 ⊔ ∅ ) ≈ 𝐴 ) |
15 |
|
nna0 |
⊢ ( 𝐴 ∈ ω → ( 𝐴 +o ∅ ) = 𝐴 ) |
16 |
14 15
|
breqtrrd |
⊢ ( 𝐴 ∈ ω → ( 𝐴 ⊔ ∅ ) ≈ ( 𝐴 +o ∅ ) ) |
17 |
|
1oex |
⊢ 1o ∈ V |
18 |
|
djuassen |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ∧ 1o ∈ V ) → ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) ) |
19 |
17 18
|
mp3an3 |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) ) |
20 |
|
enrefg |
⊢ ( 𝐴 ∈ ω → 𝐴 ≈ 𝐴 ) |
21 |
|
nnord |
⊢ ( 𝑦 ∈ ω → Ord 𝑦 ) |
22 |
|
ordirr |
⊢ ( Ord 𝑦 → ¬ 𝑦 ∈ 𝑦 ) |
23 |
21 22
|
syl |
⊢ ( 𝑦 ∈ ω → ¬ 𝑦 ∈ 𝑦 ) |
24 |
|
dju1en |
⊢ ( ( 𝑦 ∈ ω ∧ ¬ 𝑦 ∈ 𝑦 ) → ( 𝑦 ⊔ 1o ) ≈ suc 𝑦 ) |
25 |
23 24
|
mpdan |
⊢ ( 𝑦 ∈ ω → ( 𝑦 ⊔ 1o ) ≈ suc 𝑦 ) |
26 |
|
djuen |
⊢ ( ( 𝐴 ≈ 𝐴 ∧ ( 𝑦 ⊔ 1o ) ≈ suc 𝑦 ) → ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) ≈ ( 𝐴 ⊔ suc 𝑦 ) ) |
27 |
20 25 26
|
syl2an |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) ≈ ( 𝐴 ⊔ suc 𝑦 ) ) |
28 |
|
entr |
⊢ ( ( ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) ∧ ( 𝐴 ⊔ ( 𝑦 ⊔ 1o ) ) ≈ ( 𝐴 ⊔ suc 𝑦 ) ) → ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 ⊔ suc 𝑦 ) ) |
29 |
19 27 28
|
syl2anc |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 ⊔ suc 𝑦 ) ) |
30 |
29
|
ensymd |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ⊔ suc 𝑦 ) ≈ ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ) |
31 |
17
|
enref |
⊢ 1o ≈ 1o |
32 |
|
djuen |
⊢ ( ( ( 𝐴 ⊔ 𝑦 ) ≈ ( 𝐴 +o 𝑦 ) ∧ 1o ≈ 1o ) → ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ) |
33 |
31 32
|
mpan2 |
⊢ ( ( 𝐴 ⊔ 𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ) |
34 |
33
|
a1i |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ⊔ 𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ) ) |
35 |
|
nnacl |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 +o 𝑦 ) ∈ ω ) |
36 |
|
nnord |
⊢ ( ( 𝐴 +o 𝑦 ) ∈ ω → Ord ( 𝐴 +o 𝑦 ) ) |
37 |
|
ordirr |
⊢ ( Ord ( 𝐴 +o 𝑦 ) → ¬ ( 𝐴 +o 𝑦 ) ∈ ( 𝐴 +o 𝑦 ) ) |
38 |
35 36 37
|
3syl |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ¬ ( 𝐴 +o 𝑦 ) ∈ ( 𝐴 +o 𝑦 ) ) |
39 |
|
dju1en |
⊢ ( ( ( 𝐴 +o 𝑦 ) ∈ ω ∧ ¬ ( 𝐴 +o 𝑦 ) ∈ ( 𝐴 +o 𝑦 ) ) → ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ≈ suc ( 𝐴 +o 𝑦 ) ) |
40 |
35 38 39
|
syl2anc |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ≈ suc ( 𝐴 +o 𝑦 ) ) |
41 |
|
nnasuc |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) ) |
42 |
40 41
|
breqtrrd |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) ) |
43 |
34 42
|
jctird |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ⊔ 𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ∧ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) ) ) ) |
44 |
|
entr |
⊢ ( ( ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ∧ ( ( 𝐴 +o 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) ) → ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) ) |
45 |
43 44
|
syl6 |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ⊔ 𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) ) ) |
46 |
|
entr |
⊢ ( ( ( 𝐴 ⊔ suc 𝑦 ) ≈ ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ∧ ( ( 𝐴 ⊔ 𝑦 ) ⊔ 1o ) ≈ ( 𝐴 +o suc 𝑦 ) ) → ( 𝐴 ⊔ suc 𝑦 ) ≈ ( 𝐴 +o suc 𝑦 ) ) |
47 |
30 45 46
|
syl6an |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ⊔ 𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( 𝐴 ⊔ suc 𝑦 ) ≈ ( 𝐴 +o suc 𝑦 ) ) ) |
48 |
47
|
expcom |
⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( ( 𝐴 ⊔ 𝑦 ) ≈ ( 𝐴 +o 𝑦 ) → ( 𝐴 ⊔ suc 𝑦 ) ≈ ( 𝐴 +o suc 𝑦 ) ) ) ) |
49 |
7 10 13 16 48
|
finds2 |
⊢ ( 𝑥 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴 ⊔ 𝑥 ) ≈ ( 𝐴 +o 𝑥 ) ) ) |
50 |
4 49
|
vtoclga |
⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 +o 𝐵 ) ) ) |
51 |
50
|
impcom |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 +o 𝐵 ) ) |
52 |
|
carden2b |
⊢ ( ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 +o 𝐵 ) → ( card ‘ ( 𝐴 ⊔ 𝐵 ) ) = ( card ‘ ( 𝐴 +o 𝐵 ) ) ) |
53 |
51 52
|
syl |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴 ⊔ 𝐵 ) ) = ( card ‘ ( 𝐴 +o 𝐵 ) ) ) |
54 |
|
nnacl |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) ∈ ω ) |
55 |
|
cardnn |
⊢ ( ( 𝐴 +o 𝐵 ) ∈ ω → ( card ‘ ( 𝐴 +o 𝐵 ) ) = ( 𝐴 +o 𝐵 ) ) |
56 |
54 55
|
syl |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴 +o 𝐵 ) ) = ( 𝐴 +o 𝐵 ) ) |
57 |
53 56
|
eqtrd |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴 ⊔ 𝐵 ) ) = ( 𝐴 +o 𝐵 ) ) |