Step | Hyp | Ref
| Expression |
1 | | fzfi 13443 |
. . . . . . . 8
⊢
(1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin |
2 | | ficardom 9475 |
. . . . . . . 8
⊢
((1...((♯‘𝐵) − (♯‘𝐴))) ∈ Fin →
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
⊢
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω |
4 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) = (rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) |
5 | 4 | hashgval 13797 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (♯‘𝐴)) |
6 | 5 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (♯‘𝐴)) |
7 | 4 | hashgval 13797 |
. . . . . . . . . . . . . 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 13821 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
10 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(♯‘𝐴) ∈
ℕ0) |
11 | | hashcl 13821 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
12 | 11 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(♯‘𝐵) ∈
ℕ0) |
13 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(♯‘𝐴) ≤
(♯‘𝐵)) |
14 | | nn0sub2 12136 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((♯‘𝐵) −
(♯‘𝐴)) ∈
ℕ0) |
15 | 10, 12, 13, 14 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((♯‘𝐵) −
(♯‘𝐴)) ∈
ℕ0) |
16 | | hashfz1 13810 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐵)
− (♯‘𝐴))
∈ ℕ0 → (♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(♯‘(1...((♯‘𝐵) − (♯‘𝐴)))) = ((♯‘𝐵) − (♯‘𝐴))) |
18 | 8, 17 | syl5eq 2786 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = ((♯‘𝐵) − (♯‘𝐴))) |
19 | 6, 18 | oveq12d 7200 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((♯‘𝐴) + ((♯‘𝐵) − (♯‘𝐴)))) |
20 | 9 | nn0cnd 12050 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℂ) |
21 | 11 | nn0cnd 12050 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℂ) |
22 | | pncan3 10984 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝐴)
∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) →
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘𝐴))) =
(♯‘𝐵)) |
23 | 20, 21, 22 | syl2an 599 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘𝐴))) =
(♯‘𝐵)) |
24 | 23 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘𝐴))) =
(♯‘𝐵)) |
25 | 19, 24 | eqtrd 2774 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = (♯‘𝐵)) |
26 | | ficardom 9475 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ∈
ω) |
27 | 26 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(card‘𝐴) ∈
ω) |
28 | 4 | hashgadd 13842 |
. . . . . . . . . . 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 589 |
. . . . . . . . . 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 13797 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) = (♯‘𝐵)) |
31 | 30 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) = (♯‘𝐵)) |
32 | 25, 29, 31 | 3eqtr4d 2784 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵))) |
33 | 32 | fveq2d 6690 |
. . . . . . . 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 13442 |
. . . . . . . . 9
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω):ω–1-1-onto→ℕ0 |
35 | | nnacl 8280 |
. . . . . . . . . 10
⊢
(((card‘𝐴)
∈ ω ∧ (card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω) →
((card‘𝐴)
+o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω) |
36 | 27, 3, 35 | sylancl 589 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((card‘𝐴)
+o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) ∈ ω) |
37 | | f1ocnvfv1 7056 |
. . . . . . . . 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 590 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴))))))) = ((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) |
39 | | ficardom 9475 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Fin →
(card‘𝐵) ∈
ω) |
40 | 39 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(card‘𝐵) ∈
ω) |
41 | | f1ocnvfv1 7056 |
. . . . . . . . 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 590 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω)‘(card‘𝐵))) = (card‘𝐵)) |
43 | 33, 38, 42 | 3eqtr3d 2782 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
((card‘𝐴)
+o (card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)) |
44 | | oveq2 7190 |
. . . . . . . . 9
⊢ (𝑦 =
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → ((card‘𝐴) +o 𝑦) = ((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))))) |
45 | 44 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑦 =
(card‘(1...((♯‘𝐵) − (♯‘𝐴)))) → (((card‘𝐴) +o 𝑦) = (card‘𝐵) ↔ ((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵))) |
46 | 45 | rspcev 3529 |
. . . . . . 7
⊢
(((card‘(1...((♯‘𝐵) − (♯‘𝐴)))) ∈ ω ∧ ((card‘𝐴) +o
(card‘(1...((♯‘𝐵) − (♯‘𝐴))))) = (card‘𝐵)) → ∃𝑦 ∈ ω ((card‘𝐴) +o 𝑦) = (card‘𝐵)) |
47 | 3, 43, 46 | sylancr 590 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵)) |
48 | 47 | ex 416 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) ≤
(♯‘𝐵) →
∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵))) |
49 | | cardnn 9477 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ω →
(card‘𝑦) = 𝑦) |
50 | 49 | adantl 485 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(card‘𝑦) = 𝑦) |
51 | 50 | oveq2d 7198 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
((card‘𝐴)
+o (card‘𝑦)) = ((card‘𝐴) +o 𝑦)) |
52 | 51 | eqeq1d 2741 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(((card‘𝐴)
+o (card‘𝑦)) = (card‘𝐵) ↔ ((card‘𝐴) +o 𝑦) = (card‘𝐵))) |
53 | | fveq2 6686 |
. . . . . . . 8
⊢
(((card‘𝐴)
+o (card‘𝑦)) = (card‘𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵))) |
54 | | nnfi 8778 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → 𝑦 ∈ Fin) |
55 | | ficardom 9475 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin →
(card‘𝑦) ∈
ω) |
56 | 4 | hashgadd 13842 |
. . . . . . . . . . . . . 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 599 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦)))) |
58 | 4 | hashgval 13797 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦)) = (♯‘𝑦)) |
59 | 5, 58 | oveqan12d 7201 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) + ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦))) |
60 | 57, 59 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦))) |
61 | 60 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((♯‘𝐴) + (♯‘𝑦))) |
62 | 30 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) = (♯‘𝐵)) |
63 | 61, 62 | eqeq12d 2755 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) ↔ ((♯‘𝐴) + (♯‘𝑦)) = (♯‘𝐵))) |
64 | | hashcl 13821 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℕ0) |
65 | 64 | nn0ge0d 12051 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin → 0 ≤
(♯‘𝑦)) |
66 | 65 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → 0 ≤
(♯‘𝑦)) |
67 | 9 | nn0red 12049 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℝ) |
68 | 64 | nn0red 12049 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℝ) |
69 | | addge01 11240 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐴)
∈ ℝ ∧ (♯‘𝑦) ∈ ℝ) → (0 ≤
(♯‘𝑦) ↔
(♯‘𝐴) ≤
((♯‘𝐴) +
(♯‘𝑦)))) |
70 | 67, 68, 69 | syl2an 599 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) → (0 ≤
(♯‘𝑦) ↔
(♯‘𝐴) ≤
((♯‘𝐴) +
(♯‘𝑦)))) |
71 | 66, 70 | mpbid 235 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑦 ∈ Fin) →
(♯‘𝐴) ≤
((♯‘𝐴) +
(♯‘𝑦))) |
72 | 71 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(♯‘𝐴) ≤
((♯‘𝐴) +
(♯‘𝑦))) |
73 | | breq2 5044 |
. . . . . . . . . . 11
⊢
(((♯‘𝐴)
+ (♯‘𝑦)) =
(♯‘𝐵) →
((♯‘𝐴) ≤
((♯‘𝐴) +
(♯‘𝑦)) ↔
(♯‘𝐴) ≤
(♯‘𝐵))) |
74 | 72, 73 | syl5ibcom 248 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(((♯‘𝐴) +
(♯‘𝑦)) =
(♯‘𝐵) →
(♯‘𝐴) ≤
(♯‘𝐵))) |
75 | 63, 74 | sylbid 243 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) →
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω)‘((card‘𝐴) +o (card‘𝑦))) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))) |
76 | 54, 75 | sylan2 596 |
. . . . . . . 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 263 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ ω) →
(((card‘𝐴)
+o 𝑦) =
(card‘𝐵) →
(♯‘𝐴) ≤
(♯‘𝐵))) |
79 | 78 | rexlimdva 3195 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵) →
(♯‘𝐴) ≤
(♯‘𝐵))) |
80 | 48, 79 | impbid 215 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) ≤
(♯‘𝐵) ↔
∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵))) |
81 | | nnawordex 8306 |
. . . . 5
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ ∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵))) |
82 | 26, 39, 81 | syl2an 599 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴) ⊆
(card‘𝐵) ↔
∃𝑦 ∈ ω
((card‘𝐴)
+o 𝑦) =
(card‘𝐵))) |
83 | | finnum 9462 |
. . . . 5
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom
card) |
84 | | finnum 9462 |
. . . . 5
⊢ (𝐵 ∈ Fin → 𝐵 ∈ dom
card) |
85 | | carddom2 9491 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) →
((card‘𝐴) ⊆
(card‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
86 | 83, 84, 85 | syl2an 599 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴) ⊆
(card‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
87 | 80, 82, 86 | 3bitr2d 310 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) ≤
(♯‘𝐵) ↔
𝐴 ≼ 𝐵)) |
88 | 87 | adantlr 715 |
. 2
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
89 | | hashxrcl 13822 |
. . . . . 6
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℝ*) |
90 | 89 | ad2antrr 726 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ∈
ℝ*) |
91 | | pnfge 12620 |
. . . . 5
⊢
((♯‘𝐴)
∈ ℝ* → (♯‘𝐴) ≤ +∞) |
92 | 90, 91 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤
+∞) |
93 | | hashinf 13799 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞) |
94 | 93 | adantll 714 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞) |
95 | 92, 94 | breqtrrd 5068 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ (♯‘𝐵)) |
96 | | isinffi 9506 |
. . . . . 6
⊢ ((¬
𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
97 | 96 | ancoms 462 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
98 | 97 | adantlr 715 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
99 | | brdomg 8577 |
. . . . 5
⊢ (𝐵 ∈ 𝑉 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
100 | 99 | ad2antlr 727 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
101 | 98, 100 | mpbird 260 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → 𝐴 ≼ 𝐵) |
102 | 95, 101 | 2thd 268 |
. 2
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
103 | 88, 102 | pm2.61dan 813 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵)) |