| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fzfi |
⊢ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ∈ Fin |
| 2 |
|
ficardom |
⊢ ( ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ∈ Fin → ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ ω ) |
| 3 |
1 2
|
ax-mp |
⊢ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ ω |
| 4 |
|
eqid |
⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) |
| 5 |
4
|
hashgval |
⊢ ( 𝐴 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) ) |
| 6 |
5
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) ) |
| 7 |
4
|
hashgval |
⊢ ( ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) |
| 8 |
1 7
|
ax-mp |
⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) |
| 9 |
|
hashcl |
⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) |
| 10 |
9
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) |
| 11 |
|
hashcl |
⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) |
| 12 |
11
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) |
| 13 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) |
| 14 |
|
nn0sub2 |
⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ∈ ℕ0 ) |
| 15 |
10 12 13 14
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ∈ ℕ0 ) |
| 16 |
|
hashfz1 |
⊢ ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) = ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) |
| 17 |
15 16
|
syl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) = ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) |
| 18 |
8 17
|
syl5eq |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) |
| 19 |
6 18
|
oveq12d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) |
| 20 |
9
|
nn0cnd |
⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℂ ) |
| 21 |
11
|
nn0cnd |
⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℂ ) |
| 22 |
|
pncan3 |
⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℂ ∧ ( ♯ ‘ 𝐵 ) ∈ ℂ ) → ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐵 ) ) |
| 23 |
20 21 22
|
syl2an |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐵 ) ) |
| 24 |
23
|
adantr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐵 ) ) |
| 25 |
19 24
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ♯ ‘ 𝐵 ) ) |
| 26 |
|
ficardom |
⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω ) |
| 27 |
26
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( card ‘ 𝐴 ) ∈ ω ) |
| 28 |
4
|
hashgadd |
⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) |
| 29 |
27 3 28
|
sylancl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) |
| 30 |
4
|
hashgval |
⊢ ( 𝐵 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) = ( ♯ ‘ 𝐵 ) ) |
| 31 |
30
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) = ( ♯ ‘ 𝐵 ) ) |
| 32 |
25 29 31
|
3eqtr4d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) |
| 33 |
32
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) = ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) ) |
| 34 |
4
|
hashgf1o |
⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ0 |
| 35 |
|
nnacl |
⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ ω ) → ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ ω ) |
| 36 |
27 3 35
|
sylancl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ ω ) |
| 37 |
|
f1ocnvfv1 |
⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ0 ∧ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ ω ) → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) |
| 38 |
34 36 37
|
sylancr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) |
| 39 |
|
ficardom |
⊢ ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ∈ ω ) |
| 40 |
39
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( card ‘ 𝐵 ) ∈ ω ) |
| 41 |
|
f1ocnvfv1 |
⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ0 ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) = ( card ‘ 𝐵 ) ) |
| 42 |
34 40 41
|
sylancr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) = ( card ‘ 𝐵 ) ) |
| 43 |
33 38 42
|
3eqtr3d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( card ‘ 𝐵 ) ) |
| 44 |
|
oveq2 |
⊢ ( 𝑦 = ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) → ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) ) |
| 45 |
44
|
eqeq1d |
⊢ ( 𝑦 = ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) → ( ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ↔ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( card ‘ 𝐵 ) ) ) |
| 46 |
45
|
rspcev |
⊢ ( ( ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ ω ∧ ( ( card ‘ 𝐴 ) +o ( card ‘ ( 1 ... ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( card ‘ 𝐵 ) ) → ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) |
| 47 |
3 43 46
|
sylancr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) → ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) |
| 48 |
47
|
ex |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) → ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) ) |
| 49 |
|
cardnn |
⊢ ( 𝑦 ∈ ω → ( card ‘ 𝑦 ) = 𝑦 ) |
| 50 |
49
|
adantl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( card ‘ 𝑦 ) = 𝑦 ) |
| 51 |
50
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) = ( ( card ‘ 𝐴 ) +o 𝑦 ) ) |
| 52 |
51
|
eqeq1d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) = ( card ‘ 𝐵 ) ↔ ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) ) |
| 53 |
|
fveq2 |
⊢ ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) = ( card ‘ 𝐵 ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ) |
| 54 |
|
nnfi |
⊢ ( 𝑦 ∈ ω → 𝑦 ∈ Fin ) |
| 55 |
|
ficardom |
⊢ ( 𝑦 ∈ Fin → ( card ‘ 𝑦 ) ∈ ω ) |
| 56 |
4
|
hashgadd |
⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝑦 ) ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) ) ) |
| 57 |
26 55 56
|
syl2an |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) ) ) |
| 58 |
4
|
hashgval |
⊢ ( 𝑦 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) = ( ♯ ‘ 𝑦 ) ) |
| 59 |
5 58
|
oveqan12d |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) + ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ) |
| 60 |
57 59
|
eqtrd |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ) |
| 61 |
60
|
adantlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ) |
| 62 |
30
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) = ( ♯ ‘ 𝐵 ) ) |
| 63 |
61 62
|
eqeq12d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ↔ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) = ( ♯ ‘ 𝐵 ) ) ) |
| 64 |
|
hashcl |
⊢ ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℕ0 ) |
| 65 |
64
|
nn0ge0d |
⊢ ( 𝑦 ∈ Fin → 0 ≤ ( ♯ ‘ 𝑦 ) ) |
| 66 |
65
|
adantl |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → 0 ≤ ( ♯ ‘ 𝑦 ) ) |
| 67 |
9
|
nn0red |
⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℝ ) |
| 68 |
64
|
nn0red |
⊢ ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℝ ) |
| 69 |
|
addge01 |
⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ ( ♯ ‘ 𝑦 ) ∈ ℝ ) → ( 0 ≤ ( ♯ ‘ 𝑦 ) ↔ ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ) ) |
| 70 |
67 68 69
|
syl2an |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( 0 ≤ ( ♯ ‘ 𝑦 ) ↔ ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ) ) |
| 71 |
66 70
|
mpbid |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ) |
| 72 |
71
|
adantlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ) |
| 73 |
|
breq2 |
⊢ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) = ( ♯ ‘ 𝐵 ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) ↔ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) ) |
| 74 |
72 73
|
syl5ibcom |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑦 ) ) = ( ♯ ‘ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) ) |
| 75 |
63 74
|
sylbid |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ Fin ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) ) |
| 76 |
54 75
|
sylan2 |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) ) |
| 77 |
53 76
|
syl5 |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝑦 ) ) = ( card ‘ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) ) |
| 78 |
52 77
|
sylbird |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ 𝑦 ∈ ω ) → ( ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) ) |
| 79 |
78
|
rexlimdva |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) ) |
| 80 |
48 79
|
impbid |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) ) |
| 81 |
|
nnawordex |
⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) ) |
| 82 |
26 39 81
|
syl2an |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ ∃ 𝑦 ∈ ω ( ( card ‘ 𝐴 ) +o 𝑦 ) = ( card ‘ 𝐵 ) ) ) |
| 83 |
|
finnum |
⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card ) |
| 84 |
|
finnum |
⊢ ( 𝐵 ∈ Fin → 𝐵 ∈ dom card ) |
| 85 |
|
carddom2 |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) ) |
| 86 |
83 84 85
|
syl2an |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) ) |
| 87 |
80 82 86
|
3bitr2d |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) ) |
| 88 |
87
|
adantlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) ) |
| 89 |
|
hashxrcl |
⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℝ* ) |
| 90 |
89
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ∈ ℝ* ) |
| 91 |
|
pnfge |
⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℝ* → ( ♯ ‘ 𝐴 ) ≤ +∞ ) |
| 92 |
90 91
|
syl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ +∞ ) |
| 93 |
|
hashinf |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ ) |
| 94 |
93
|
adantll |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ ) |
| 95 |
92 94
|
breqtrrd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) |
| 96 |
|
isinffi |
⊢ ( ( ¬ 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) |
| 97 |
96
|
ancoms |
⊢ ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) |
| 98 |
97
|
adantlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) |
| 99 |
|
brdomg |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) ) |
| 100 |
99
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) ) |
| 101 |
98 100
|
mpbird |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → 𝐴 ≼ 𝐵 ) |
| 102 |
95 101
|
2thd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) ) |
| 103 |
88 102
|
pm2.61dan |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) ) |