Step | Hyp | Ref
| Expression |
1 | | fzfi 13692 |
. . . . . . . 8
⊢
(1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin |
2 | | ficardom 9719 |
. . . . . . . 8
⊢
((1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin →
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
⊢
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω |
4 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) = (rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) |
5 | 4 | hashgval 14047 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (♯‘𝐴)) |
6 | 5 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (♯‘𝐴)) |
7 | 4 | hashgval 14047 |
. . . . . . . . . . . . . 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 14071 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
10 | 9 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(♯‘𝐴) ∈
ℕ0) |
11 | | hashcl 14071 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
12 | 11 | ad2antlr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(♯‘𝐵) ∈
ℕ0) |
13 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(♯‘𝐴) ≤
(♯‘𝐵)) |
14 | | nn0sub2 12381 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((♯‘𝐵) −
(♯‘𝐴)) ∈
ℕ0) |
15 | 10, 12, 13, 14 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((♯‘𝐵) −
(♯‘𝐴)) ∈
ℕ0) |
16 | | hashfz1 14060 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐵)
− (♯‘𝐴))
∈ ℕ0 → (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴))) |
18 | 8, 17 | eqtrid 2790 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = ((♯‘𝐵) − (♯‘𝐴))) |
19 | 6, 18 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴)))) |
20 | 9 | nn0cnd 12295 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℂ) |
21 | 11 | nn0cnd 12295 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℂ) |
22 | | pncan3 11229 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝐴)
∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) →
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘𝐴))) =
(♯‘𝐵)) |
23 | 20, 21, 22 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘𝐴))) =
(♯‘𝐵)) |
24 | 23 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘𝐴))) =
(♯‘𝐵)) |
25 | 19, 24 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = (♯‘𝐵)) |
26 | | ficardom 9719 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ∈
ω) |
27 | 26 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(card‘𝐴) ∈
ω) |
28 | 4 | hashgadd 14092 |
. . . . . . . . . . 11
⊢
(((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 586 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴))))))) |
30 | 4 | hashgval 14047 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) = (♯‘𝐵)) |
31 | 30 | ad2antlr 724 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) = (♯‘𝐵)) |
32 | 25, 29, 31 | 3eqtr4d 2788 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵))) |
33 | 32 | fveq2d 6778 |
. . . . . . . 8
⊢ (((𝐴 ∈ 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 13691 |
. . . . . . . . 9
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω):ω–1-1-onto→ℕ0 |
35 | | nnacl 8442 |
. . . . . . . . . 10
⊢
(((card‘𝐴)
∈ ω ∧ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω) →
((card‘𝐴)
+o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω) |
36 | 27, 3, 35 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((card‘𝐴)
+o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω) |
37 | | f1ocnvfv1 7148 |
. . . . . . . . 9
⊢
(((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 587 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴))))))) = ((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) |
39 | | ficardom 9719 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Fin →
(card‘𝐵) ∈
ω) |
40 | 39 | ad2antlr 724 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(card‘𝐵) ∈
ω) |
41 | | f1ocnvfv1 7148 |
. . . . . . . . 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 587 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵)) |
43 | 33, 38, 42 | 3eqtr3d 2786 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((card‘𝐴)
+o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)) |
44 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑦 =
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → ((card‘𝐴) +o 𝑦) = ((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) |
45 | 44 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑦 =
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → (((card‘𝐴) +o 𝑦) = (card‘𝐵) ↔ ((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵))) |
46 | 45 | rspcev 3561 |
. . . . . . 7
⊢
(((card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω ∧ ((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +o 𝑦) = (card‘𝐵)) |
47 | 3, 43, 46 | sylancr 587 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵)) |
48 | 47 | ex 413 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) ≤
(♯‘𝐵) →
∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵))) |
49 | | cardnn 9721 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ω →
(card‘𝑦) = 𝑦) |
50 | 49 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(card‘𝑦) = 𝑦) |
51 | 50 | oveq2d 7291 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
((card‘𝐴)
+o (card‘𝑦)) = ((card‘𝐴) +o 𝑦)) |
52 | 51 | eqeq1d 2740 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(((card‘𝐴)
+o (card‘𝑦)) = (card‘𝐵) ↔ ((card‘𝐴) +o 𝑦) = (card‘𝐵))) |
53 | | fveq2 6774 |
. . . . . . . 8
⊢
(((card‘𝐴)
+o (card‘𝑦)) = (card‘𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵))) |
54 | | nnfi 8950 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → 𝑦 ∈ Fin) |
55 | | ficardom 9719 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin →
(card‘𝑦) ∈
ω) |
56 | 4 | hashgadd 14092 |
. . . . . . . . . . . . . 14
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝑦) ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦)))) |
57 | 26, 55, 56 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦)))) |
58 | 4 | hashgval 14047 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦)) = (♯‘𝑦)) |
59 | 5, 58 | oveqan12d 7294 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦))) |
60 | 57, 59 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦))) |
61 | 60 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦))) |
62 | 30 | ad2antlr 724 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) = (♯‘𝐵)) |
63 | 61, 62 | eqeq12d 2754 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) ↔ ((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵))) |
64 | | hashcl 14071 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℕ0) |
65 | 64 | nn0ge0d 12296 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin → 0 ≤
(♯‘𝑦)) |
66 | 65 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → 0 ≤
(♯‘𝑦)) |
67 | 9 | nn0red 12294 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℝ) |
68 | 64 | nn0red 12294 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℝ) |
69 | | addge01 11485 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐴)
∈ ℝ ∧ (♯‘𝑦) ∈ ℝ) → (0 ≤
(♯‘𝑦) ↔
(♯‘𝐴) ≤
((♯‘𝐴) +
(♯‘𝑦)))) |
70 | 67, 68, 69 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (0 ≤
(♯‘𝑦) ↔
(♯‘𝐴) ≤
((♯‘𝐴) +
(♯‘𝑦)))) |
71 | 66, 70 | mpbid 231 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) →
(♯‘𝐴) ≤
((♯‘𝐴) +
(♯‘𝑦))) |
72 | 71 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(♯‘𝐴) ≤
((♯‘𝐴) +
(♯‘𝑦))) |
73 | | breq2 5078 |
. . . . . . . . . . 11
⊢
(((♯‘𝐴)
+ (♯‘𝑦)) =
(♯‘𝐵) →
((♯‘𝐴) ≤
((♯‘𝐴) +
(♯‘𝑦)) ↔
(♯‘𝐴) ≤
(♯‘𝐵))) |
74 | 72, 73 | syl5ibcom 244 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(((♯‘𝐴) +
(♯‘𝑦)) =
(♯‘𝐵) →
(♯‘𝐴) ≤
(♯‘𝐵))) |
75 | 63, 74 | sylbid 239 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))) |
76 | 54, 75 | sylan2 593 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))) |
77 | 53, 76 | syl5 34 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(((card‘𝐴)
+o (card‘𝑦)) = (card‘𝐵) → (♯‘𝐴) ≤ (♯‘𝐵))) |
78 | 52, 77 | sylbird 259 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(((card‘𝐴)
+o 𝑦) =
(card‘𝐵) →
(♯‘𝐴) ≤
(♯‘𝐵))) |
79 | 78 | rexlimdva 3213 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵) →
(♯‘𝐴) ≤
(♯‘𝐵))) |
80 | 48, 79 | impbid 211 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) ≤
(♯‘𝐵) ↔
∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵))) |
81 | | nnawordex 8468 |
. . . . 5
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵))) |
82 | 26, 39, 81 | syl2an 596 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴) ⊆
(card‘𝐵) ↔
∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵))) |
83 | | finnum 9706 |
. . . . 5
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom
card) |
84 | | finnum 9706 |
. . . . 5
⊢ (𝐵 ∈ Fin → 𝐵 ∈ dom
card) |
85 | | carddom2 9735 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) →
((card‘𝐴) ⊆
(card‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
86 | 83, 84, 85 | syl2an 596 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴) ⊆
(card‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
87 | 80, 82, 86 | 3bitr2d 307 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) ≤
(♯‘𝐵) ↔
𝐴 ≼ 𝐵)) |
88 | 87 | adantlr 712 |
. 2
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
89 | | hashxrcl 14072 |
. . . . . 6
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℝ*) |
90 | 89 | ad2antrr 723 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ∈
ℝ*) |
91 | | pnfge 12866 |
. . . . 5
⊢
((♯‘𝐴)
∈ ℝ* → (♯‘𝐴) ≤ +∞) |
92 | 90, 91 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤
+∞) |
93 | | hashinf 14049 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞) |
94 | 93 | adantll 711 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞) |
95 | 92, 94 | breqtrrd 5102 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ (♯‘𝐵)) |
96 | | isinffi 9750 |
. . . . . 6
⊢ ((¬
𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
97 | 96 | ancoms 459 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
98 | 97 | adantlr 712 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
99 | | brdomg 8746 |
. . . . 5
⊢ (𝐵 ∈ 𝑉 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
100 | 99 | ad2antlr 724 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
101 | 98, 100 | mpbird 256 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → 𝐴 ≼ 𝐵) |
102 | 95, 101 | 2thd 264 |
. 2
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
103 | 88, 102 | pm2.61dan 810 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵)) |