Step | Hyp | Ref
| Expression |
1 | | fzfi 12633 |
. . . . . . . 8
⊢
(1...((#‘𝐵)
− (#‘𝐴)))
∈ Fin |
2 | | ficardom 8670 |
. . . . . . . 8
⊢
((1...((#‘𝐵)
− (#‘𝐴)))
∈ Fin → (card‘(1...((#‘𝐵) − (#‘𝐴)))) ∈ ω) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
⊢
(card‘(1...((#‘𝐵) − (#‘𝐴)))) ∈ ω |
4 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) = (rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) |
5 | 4 | hashgval 12982 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (#‘𝐴)) |
6 | 5 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (#‘𝐴)) |
7 | 4 | hashgval 12982 |
. . . . . . . . . . . . . 14
⊢
((1...((#‘𝐵)
− (#‘𝐴)))
∈ Fin → ((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘(card‘(1...((#‘𝐵) − (#‘𝐴))))) = (#‘(1...((#‘𝐵) − (#‘𝐴))))) |
8 | 1, 7 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω)‘(card‘(1...((#‘𝐵) − (#‘𝐴))))) = (#‘(1...((#‘𝐵) − (#‘𝐴)))) |
9 | | hashcl 13009 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℕ0) |
10 | 9 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(#‘𝐴) ∈
ℕ0) |
11 | | hashcl 13009 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ Fin →
(#‘𝐵) ∈
ℕ0) |
12 | 11 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(#‘𝐵) ∈
ℕ0) |
13 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(#‘𝐴) ≤
(#‘𝐵)) |
14 | | nn0sub2 11315 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) →
((#‘𝐵) −
(#‘𝐴)) ∈
ℕ0) |
15 | 10, 12, 13, 14 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
((#‘𝐵) −
(#‘𝐴)) ∈
ℕ0) |
16 | | hashfz1 12996 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐵)
− (#‘𝐴)) ∈
ℕ0 → (#‘(1...((#‘𝐵) − (#‘𝐴)))) = ((#‘𝐵) − (#‘𝐴))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(#‘(1...((#‘𝐵)
− (#‘𝐴)))) =
((#‘𝐵) −
(#‘𝐴))) |
18 | 8, 17 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((#‘𝐵) − (#‘𝐴))))) = ((#‘𝐵) − (#‘𝐴))) |
19 | 6, 18 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((#‘𝐵) − (#‘𝐴)))))) = ((#‘𝐴) + ((#‘𝐵) − (#‘𝐴)))) |
20 | 9 | nn0cnd 11230 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℂ) |
21 | 11 | nn0cnd 11230 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ Fin →
(#‘𝐵) ∈
ℂ) |
22 | | pncan3 10168 |
. . . . . . . . . . . . 13
⊢
(((#‘𝐴) ∈
ℂ ∧ (#‘𝐵)
∈ ℂ) → ((#‘𝐴) + ((#‘𝐵) − (#‘𝐴))) = (#‘𝐵)) |
23 | 20, 21, 22 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((#‘𝐴) +
((#‘𝐵) −
(#‘𝐴))) =
(#‘𝐵)) |
24 | 23 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
((#‘𝐴) +
((#‘𝐵) −
(#‘𝐴))) =
(#‘𝐵)) |
25 | 19, 24 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((#‘𝐵) − (#‘𝐴)))))) = (#‘𝐵)) |
26 | | ficardom 8670 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ∈
ω) |
27 | 26 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(card‘𝐴) ∈
ω) |
28 | 4 | hashgadd 13027 |
. . . . . . . . . . 11
⊢
(((card‘𝐴)
∈ ω ∧ (card‘(1...((#‘𝐵) − (#‘𝐴)))) ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴)))))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((#‘𝐵) − (#‘𝐴))))))) |
29 | 27, 3, 28 | sylancl 693 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴)))))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((#‘𝐵) − (#‘𝐴))))))) |
30 | 4 | hashgval 12982 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) = (#‘𝐵)) |
31 | 30 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) = (#‘𝐵)) |
32 | 25, 29, 31 | 3eqtr4d 2654 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴)))))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵))) |
33 | 32 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴))))))) = (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘(card‘𝐵)))) |
34 | 4 | hashgf1o 12632 |
. . . . . . . . 9
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω):ω–1-1-onto→ℕ0 |
35 | | nnacl 7578 |
. . . . . . . . . 10
⊢
(((card‘𝐴)
∈ ω ∧ (card‘(1...((#‘𝐵) − (#‘𝐴)))) ∈ ω) →
((card‘𝐴)
+𝑜 (card‘(1...((#‘𝐵) − (#‘𝐴))))) ∈ ω) |
36 | 27, 3, 35 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
((card‘𝐴)
+𝑜 (card‘(1...((#‘𝐵) − (#‘𝐴))))) ∈ ω) |
37 | | f1ocnvfv1 6432 |
. . . . . . . . 9
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω):ω–1-1-onto→ℕ0 ∧
((card‘𝐴)
+𝑜 (card‘(1...((#‘𝐵) − (#‘𝐴))))) ∈ ω) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴))))))) = ((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴)))))) |
38 | 34, 36, 37 | sylancr 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴))))))) = ((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴)))))) |
39 | | ficardom 8670 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Fin →
(card‘𝐵) ∈
ω) |
40 | 39 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(card‘𝐵) ∈
ω) |
41 | | f1ocnvfv1 6432 |
. . . . . . . . 9
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω):ω–1-1-onto→ℕ0 ∧
(card‘𝐵) ∈
ω) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵)) |
42 | 34, 40, 41 | sylancr 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵)) |
43 | 33, 38, 42 | 3eqtr3d 2652 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
((card‘𝐴)
+𝑜 (card‘(1...((#‘𝐵) − (#‘𝐴))))) = (card‘𝐵)) |
44 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑦 =
(card‘(1...((#‘𝐵) − (#‘𝐴)))) → ((card‘𝐴) +𝑜 𝑦) = ((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴)))))) |
45 | 44 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑦 =
(card‘(1...((#‘𝐵) − (#‘𝐴)))) → (((card‘𝐴) +𝑜 𝑦) = (card‘𝐵) ↔ ((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴))))) = (card‘𝐵))) |
46 | 45 | rspcev 3282 |
. . . . . . 7
⊢
(((card‘(1...((#‘𝐵) − (#‘𝐴)))) ∈ ω ∧ ((card‘𝐴) +𝑜
(card‘(1...((#‘𝐵) − (#‘𝐴))))) = (card‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +𝑜 𝑦) = (card‘𝐵)) |
47 | 3, 43, 46 | sylancr 694 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(#‘𝐴) ≤
(#‘𝐵)) →
∃𝑦 ∈ ω
((card‘𝐴)
+𝑜 𝑦) =
(card‘𝐵)) |
48 | 47 | ex 449 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((#‘𝐴) ≤
(#‘𝐵) →
∃𝑦 ∈ ω
((card‘𝐴)
+𝑜 𝑦) =
(card‘𝐵))) |
49 | | cardnn 8672 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ω →
(card‘𝑦) = 𝑦) |
50 | 49 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(card‘𝑦) = 𝑦) |
51 | 50 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
((card‘𝐴)
+𝑜 (card‘𝑦)) = ((card‘𝐴) +𝑜 𝑦)) |
52 | 51 | eqeq1d 2612 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(((card‘𝐴)
+𝑜 (card‘𝑦)) = (card‘𝐵) ↔ ((card‘𝐴) +𝑜 𝑦) = (card‘𝐵))) |
53 | | fveq2 6103 |
. . . . . . . 8
⊢
(((card‘𝐴)
+𝑜 (card‘𝑦)) = (card‘𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜 (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵))) |
54 | | nnfi 8038 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → 𝑦 ∈ Fin) |
55 | | ficardom 8670 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin →
(card‘𝑦) ∈
ω) |
56 | 4 | hashgadd 13027 |
. . . . . . . . . . . . . 14
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝑦) ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜 (card‘𝑦))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦)))) |
57 | 26, 55, 56 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜 (card‘𝑦))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦)))) |
58 | 4 | hashgval 12982 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦)) = (#‘𝑦)) |
59 | 5, 58 | oveqan12d 6568 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦))) = ((#‘𝐴) + (#‘𝑦))) |
60 | 57, 59 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜 (card‘𝑦))) = ((#‘𝐴) + (#‘𝑦))) |
61 | 60 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜 (card‘𝑦))) = ((#‘𝐴) + (#‘𝑦))) |
62 | 30 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) = (#‘𝐵)) |
63 | 61, 62 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜 (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) ↔ ((#‘𝐴) + (#‘𝑦)) = (#‘𝐵))) |
64 | | hashcl 13009 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ Fin →
(#‘𝑦) ∈
ℕ0) |
65 | 64 | nn0ge0d 11231 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin → 0 ≤
(#‘𝑦)) |
66 | 65 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → 0 ≤
(#‘𝑦)) |
67 | 9 | nn0red 11229 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℝ) |
68 | 64 | nn0red 11229 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin →
(#‘𝑦) ∈
ℝ) |
69 | | addge01 10417 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐴) ∈
ℝ ∧ (#‘𝑦)
∈ ℝ) → (0 ≤ (#‘𝑦) ↔ (#‘𝐴) ≤ ((#‘𝐴) + (#‘𝑦)))) |
70 | 67, 68, 69 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (0 ≤
(#‘𝑦) ↔
(#‘𝐴) ≤
((#‘𝐴) +
(#‘𝑦)))) |
71 | 66, 70 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) →
(#‘𝐴) ≤
((#‘𝐴) +
(#‘𝑦))) |
72 | 71 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(#‘𝐴) ≤
((#‘𝐴) +
(#‘𝑦))) |
73 | | breq2 4587 |
. . . . . . . . . . 11
⊢
(((#‘𝐴) +
(#‘𝑦)) =
(#‘𝐵) →
((#‘𝐴) ≤
((#‘𝐴) +
(#‘𝑦)) ↔
(#‘𝐴) ≤
(#‘𝐵))) |
74 | 72, 73 | syl5ibcom 234 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(((#‘𝐴) +
(#‘𝑦)) =
(#‘𝐵) →
(#‘𝐴) ≤
(#‘𝐵))) |
75 | 63, 74 | sylbid 229 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜 (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) → (#‘𝐴) ≤ (#‘𝐵))) |
76 | 54, 75 | sylan2 490 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +𝑜 (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) → (#‘𝐴) ≤ (#‘𝐵))) |
77 | 53, 76 | syl5 33 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(((card‘𝐴)
+𝑜 (card‘𝑦)) = (card‘𝐵) → (#‘𝐴) ≤ (#‘𝐵))) |
78 | 52, 77 | sylbird 249 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(((card‘𝐴)
+𝑜 𝑦) =
(card‘𝐵) →
(#‘𝐴) ≤
(#‘𝐵))) |
79 | 78 | rexlimdva 3013 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(∃𝑦 ∈ ω
((card‘𝐴)
+𝑜 𝑦) =
(card‘𝐵) →
(#‘𝐴) ≤
(#‘𝐵))) |
80 | 48, 79 | impbid 201 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((#‘𝐴) ≤
(#‘𝐵) ↔
∃𝑦 ∈ ω
((card‘𝐴)
+𝑜 𝑦) =
(card‘𝐵))) |
81 | | nnawordex 7604 |
. . . . 5
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω
((card‘𝐴)
+𝑜 𝑦) =
(card‘𝐵))) |
82 | 26, 39, 81 | syl2an 493 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴) ⊆
(card‘𝐵) ↔
∃𝑦 ∈ ω
((card‘𝐴)
+𝑜 𝑦) =
(card‘𝐵))) |
83 | | finnum 8657 |
. . . . 5
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom
card) |
84 | | finnum 8657 |
. . . . 5
⊢ (𝐵 ∈ Fin → 𝐵 ∈ dom
card) |
85 | | carddom2 8686 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) →
((card‘𝐴) ⊆
(card‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
86 | 83, 84, 85 | syl2an 493 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴) ⊆
(card‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
87 | 80, 82, 86 | 3bitr2d 295 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((#‘𝐴) ≤
(#‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
88 | 87 | adantlr 747 |
. 2
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ 𝐵 ∈ Fin) → ((#‘𝐴) ≤ (#‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
89 | | hashxrcl 13010 |
. . . . . 6
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℝ*) |
90 | 89 | ad2antrr 758 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐴) ∈
ℝ*) |
91 | | pnfge 11840 |
. . . . 5
⊢
((#‘𝐴) ∈
ℝ* → (#‘𝐴) ≤ +∞) |
92 | 90, 91 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐴) ≤
+∞) |
93 | | hashinf 12984 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐵) = +∞) |
94 | 93 | adantll 746 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐵) = +∞) |
95 | 92, 94 | breqtrrd 4611 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐴) ≤ (#‘𝐵)) |
96 | | isinffi 8701 |
. . . . . 6
⊢ ((¬
𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
97 | 96 | ancoms 468 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
98 | 97 | adantlr 747 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
99 | | brdomg 7851 |
. . . . 5
⊢ (𝐵 ∈ 𝑉 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
100 | 99 | ad2antlr 759 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
101 | 98, 100 | mpbird 246 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → 𝐴 ≼ 𝐵) |
102 | 95, 101 | 2thd 254 |
. 2
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ((#‘𝐴) ≤ (#‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
103 | 88, 102 | pm2.61dan 828 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((#‘𝐴) ≤ (#‘𝐵) ↔ 𝐴 ≼ 𝐵)) |