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
|
eqtrid |
⊢ ( ( ( 𝐴 ∈ 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 ∧ 𝐵 ∈ 𝑉 ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) ) |