| Step | Hyp | Ref
| Expression |
| 1 | | elfzoelz 13699 |
. . . . . 6
⊢ (𝑥 ∈ (0..^(𝑀 · 𝑁)) → 𝑥 ∈ ℤ) |
| 2 | | crth.1 |
. . . . . 6
⊢ 𝑆 = (0..^(𝑀 · 𝑁)) |
| 3 | 1, 2 | eleq2s 2859 |
. . . . 5
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ ℤ) |
| 4 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ) |
| 5 | | crth.4 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) |
| 6 | 5 | simp1d 1143 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑀 ∈ ℕ) |
| 8 | | zmodfzo 13934 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑥 mod 𝑀) ∈ (0..^𝑀)) |
| 9 | 4, 7, 8 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥 mod 𝑀) ∈ (0..^𝑀)) |
| 10 | 5 | simp2d 1144 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℕ) |
| 12 | | zmodfzo 13934 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑥 mod 𝑁) ∈ (0..^𝑁)) |
| 13 | 4, 11, 12 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥 mod 𝑁) ∈ (0..^𝑁)) |
| 14 | 9, 13 | opelxpd 5724 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 ∈ ((0..^𝑀) × (0..^𝑁))) |
| 15 | | crth.2 |
. . . . . 6
⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁)) |
| 16 | 14, 15 | eleqtrrdi 2852 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 ∈ 𝑇) |
| 17 | 3, 16 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 ∈ 𝑇) |
| 18 | | crth.3 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉) |
| 19 | 17, 18 | fmptd 7134 |
. . 3
⊢ (𝜑 → 𝐹:𝑆⟶𝑇) |
| 20 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 mod 𝑀) = (𝑦 mod 𝑀)) |
| 21 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 mod 𝑁) = (𝑦 mod 𝑁)) |
| 22 | 20, 21 | opeq12d 4881 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 = 〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉) |
| 23 | | opex 5469 |
. . . . . . . . 9
⊢
〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉 ∈ V |
| 24 | 22, 18, 23 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑆 → (𝐹‘𝑦) = 〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉) |
| 25 | 24 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹‘𝑦) = 〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉) |
| 26 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 mod 𝑀) = (𝑧 mod 𝑀)) |
| 27 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 mod 𝑁) = (𝑧 mod 𝑁)) |
| 28 | 26, 27 | opeq12d 4881 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 = 〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉) |
| 29 | | opex 5469 |
. . . . . . . . 9
⊢
〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉 ∈ V |
| 30 | 28, 18, 29 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 → (𝐹‘𝑧) = 〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉) |
| 31 | 30 | ad2antll 729 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹‘𝑧) = 〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉) |
| 32 | 25, 31 | eqeq12d 2753 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉 = 〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉)) |
| 33 | | ovex 7464 |
. . . . . . 7
⊢ (𝑦 mod 𝑀) ∈ V |
| 34 | | ovex 7464 |
. . . . . . 7
⊢ (𝑦 mod 𝑁) ∈ V |
| 35 | 33, 34 | opth 5481 |
. . . . . 6
⊢
(〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉 = 〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉 ↔ ((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ∧ (𝑦 mod 𝑁) = (𝑧 mod 𝑁))) |
| 36 | 32, 35 | bitrdi 287 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ ((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ∧ (𝑦 mod 𝑁) = (𝑧 mod 𝑁)))) |
| 37 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑀 ∈ ℕ) |
| 38 | 37 | nnzd 12640 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑀 ∈ ℤ) |
| 39 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑁 ∈ ℕ) |
| 40 | 39 | nnzd 12640 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑁 ∈ ℤ) |
| 41 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
| 42 | 41, 2 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 ∈ (0..^(𝑀 · 𝑁))) |
| 43 | | elfzoelz 13699 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 𝑦 ∈ ℤ) |
| 44 | 42, 43 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 ∈ ℤ) |
| 45 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ 𝑆) |
| 46 | 45, 2 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ (0..^(𝑀 · 𝑁))) |
| 47 | | elfzoelz 13699 |
. . . . . . . . 9
⊢ (𝑧 ∈ (0..^(𝑀 · 𝑁)) → 𝑧 ∈ ℤ) |
| 48 | 46, 47 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ ℤ) |
| 49 | 44, 48 | zsubcld 12727 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦 − 𝑧) ∈ ℤ) |
| 50 | 5 | simp3d 1145 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) |
| 51 | 50 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑀 gcd 𝑁) = 1) |
| 52 | | coprmdvds2 16691 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑦 − 𝑧) ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 ∥ (𝑦 − 𝑧) ∧ 𝑁 ∥ (𝑦 − 𝑧)) → (𝑀 · 𝑁) ∥ (𝑦 − 𝑧))) |
| 53 | 38, 40, 49, 51, 52 | syl31anc 1375 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑀 ∥ (𝑦 − 𝑧) ∧ 𝑁 ∥ (𝑦 − 𝑧)) → (𝑀 · 𝑁) ∥ (𝑦 − 𝑧))) |
| 54 | | moddvds 16301 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ↔ 𝑀 ∥ (𝑦 − 𝑧))) |
| 55 | 37, 44, 48, 54 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ↔ 𝑀 ∥ (𝑦 − 𝑧))) |
| 56 | | moddvds 16301 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑦 mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ (𝑦 − 𝑧))) |
| 57 | 39, 44, 48, 56 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦 mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ (𝑦 − 𝑧))) |
| 58 | 55, 57 | anbi12d 632 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ∧ (𝑦 mod 𝑁) = (𝑧 mod 𝑁)) ↔ (𝑀 ∥ (𝑦 − 𝑧) ∧ 𝑁 ∥ (𝑦 − 𝑧)))) |
| 59 | 44 | zred 12722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 ∈ ℝ) |
| 60 | 37, 39 | nnmulcld 12319 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑀 · 𝑁) ∈ ℕ) |
| 61 | 60 | nnrpd 13075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑀 · 𝑁) ∈
ℝ+) |
| 62 | | elfzole1 13707 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 0 ≤ 𝑦) |
| 63 | 42, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 0 ≤ 𝑦) |
| 64 | | elfzolt2 13708 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 𝑦 < (𝑀 · 𝑁)) |
| 65 | 42, 64 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 < (𝑀 · 𝑁)) |
| 66 | | modid 13936 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℝ ∧ (𝑀 · 𝑁) ∈ ℝ+) ∧ (0 ≤
𝑦 ∧ 𝑦 < (𝑀 · 𝑁))) → (𝑦 mod (𝑀 · 𝑁)) = 𝑦) |
| 67 | 59, 61, 63, 65, 66 | syl22anc 839 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦 mod (𝑀 · 𝑁)) = 𝑦) |
| 68 | 48 | zred 12722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ ℝ) |
| 69 | | elfzole1 13707 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0..^(𝑀 · 𝑁)) → 0 ≤ 𝑧) |
| 70 | 46, 69 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 0 ≤ 𝑧) |
| 71 | | elfzolt2 13708 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0..^(𝑀 · 𝑁)) → 𝑧 < (𝑀 · 𝑁)) |
| 72 | 46, 71 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 < (𝑀 · 𝑁)) |
| 73 | | modid 13936 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ℝ ∧ (𝑀 · 𝑁) ∈ ℝ+) ∧ (0 ≤
𝑧 ∧ 𝑧 < (𝑀 · 𝑁))) → (𝑧 mod (𝑀 · 𝑁)) = 𝑧) |
| 74 | 68, 61, 70, 72, 73 | syl22anc 839 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑧 mod (𝑀 · 𝑁)) = 𝑧) |
| 75 | 67, 74 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦 mod (𝑀 · 𝑁)) = (𝑧 mod (𝑀 · 𝑁)) ↔ 𝑦 = 𝑧)) |
| 76 | | moddvds 16301 |
. . . . . . . 8
⊢ (((𝑀 · 𝑁) ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑦 mod (𝑀 · 𝑁)) = (𝑧 mod (𝑀 · 𝑁)) ↔ (𝑀 · 𝑁) ∥ (𝑦 − 𝑧))) |
| 77 | 60, 44, 48, 76 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦 mod (𝑀 · 𝑁)) = (𝑧 mod (𝑀 · 𝑁)) ↔ (𝑀 · 𝑁) ∥ (𝑦 − 𝑧))) |
| 78 | 75, 77 | bitr3d 281 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦 = 𝑧 ↔ (𝑀 · 𝑁) ∥ (𝑦 − 𝑧))) |
| 79 | 53, 58, 78 | 3imtr4d 294 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ∧ (𝑦 mod 𝑁) = (𝑧 mod 𝑁)) → 𝑦 = 𝑧)) |
| 80 | 36, 79 | sylbid 240 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
| 81 | 80 | ralrimivva 3202 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
| 82 | | dff13 7275 |
. . 3
⊢ (𝐹:𝑆–1-1→𝑇 ↔ (𝐹:𝑆⟶𝑇 ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧))) |
| 83 | 19, 81, 82 | sylanbrc 583 |
. 2
⊢ (𝜑 → 𝐹:𝑆–1-1→𝑇) |
| 84 | | nnnn0 12533 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
| 85 | | nnnn0 12533 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 86 | | nn0mulcl 12562 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 · 𝑁) ∈
ℕ0) |
| 87 | | hashfzo0 14469 |
. . . . . . . . 9
⊢ ((𝑀 · 𝑁) ∈ ℕ0 →
(♯‘(0..^(𝑀
· 𝑁))) = (𝑀 · 𝑁)) |
| 88 | 86, 87 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (♯‘(0..^(𝑀 · 𝑁))) = (𝑀 · 𝑁)) |
| 89 | | fzofi 14015 |
. . . . . . . . . 10
⊢
(0..^𝑀) ∈
Fin |
| 90 | | fzofi 14015 |
. . . . . . . . . 10
⊢
(0..^𝑁) ∈
Fin |
| 91 | | hashxp 14473 |
. . . . . . . . . 10
⊢
(((0..^𝑀) ∈ Fin
∧ (0..^𝑁) ∈ Fin)
→ (♯‘((0..^𝑀) × (0..^𝑁))) = ((♯‘(0..^𝑀)) · (♯‘(0..^𝑁)))) |
| 92 | 89, 90, 91 | mp2an 692 |
. . . . . . . . 9
⊢
(♯‘((0..^𝑀) × (0..^𝑁))) = ((♯‘(0..^𝑀)) · (♯‘(0..^𝑁))) |
| 93 | | hashfzo0 14469 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (♯‘(0..^𝑀)) = 𝑀) |
| 94 | | hashfzo0 14469 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0..^𝑁)) = 𝑁) |
| 95 | 93, 94 | oveqan12d 7450 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((♯‘(0..^𝑀)) · (♯‘(0..^𝑁))) = (𝑀 · 𝑁)) |
| 96 | 92, 95 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (♯‘((0..^𝑀) × (0..^𝑁))) = (𝑀 · 𝑁)) |
| 97 | 88, 96 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (♯‘(0..^(𝑀 · 𝑁))) = (♯‘((0..^𝑀) × (0..^𝑁)))) |
| 98 | | fzofi 14015 |
. . . . . . . 8
⊢
(0..^(𝑀 ·
𝑁)) ∈
Fin |
| 99 | | xpfi 9358 |
. . . . . . . . 9
⊢
(((0..^𝑀) ∈ Fin
∧ (0..^𝑁) ∈ Fin)
→ ((0..^𝑀) ×
(0..^𝑁)) ∈
Fin) |
| 100 | 89, 90, 99 | mp2an 692 |
. . . . . . . 8
⊢
((0..^𝑀) ×
(0..^𝑁)) ∈
Fin |
| 101 | | hashen 14386 |
. . . . . . . 8
⊢
(((0..^(𝑀 ·
𝑁)) ∈ Fin ∧
((0..^𝑀) × (0..^𝑁)) ∈ Fin) →
((♯‘(0..^(𝑀
· 𝑁))) =
(♯‘((0..^𝑀)
× (0..^𝑁))) ↔
(0..^(𝑀 · 𝑁)) ≈ ((0..^𝑀) × (0..^𝑁)))) |
| 102 | 98, 100, 101 | mp2an 692 |
. . . . . . 7
⊢
((♯‘(0..^(𝑀 · 𝑁))) = (♯‘((0..^𝑀) × (0..^𝑁))) ↔ (0..^(𝑀 · 𝑁)) ≈ ((0..^𝑀) × (0..^𝑁))) |
| 103 | 97, 102 | sylib 218 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (0..^(𝑀 · 𝑁)) ≈ ((0..^𝑀) × (0..^𝑁))) |
| 104 | 84, 85, 103 | syl2an 596 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(0..^(𝑀 · 𝑁)) ≈ ((0..^𝑀) × (0..^𝑁))) |
| 105 | 6, 10, 104 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (0..^(𝑀 · 𝑁)) ≈ ((0..^𝑀) × (0..^𝑁))) |
| 106 | 105, 2, 15 | 3brtr4g 5177 |
. . 3
⊢ (𝜑 → 𝑆 ≈ 𝑇) |
| 107 | 15, 100 | eqeltri 2837 |
. . 3
⊢ 𝑇 ∈ Fin |
| 108 | | f1finf1o 9305 |
. . 3
⊢ ((𝑆 ≈ 𝑇 ∧ 𝑇 ∈ Fin) → (𝐹:𝑆–1-1→𝑇 ↔ 𝐹:𝑆–1-1-onto→𝑇)) |
| 109 | 106, 107,
108 | sylancl 586 |
. 2
⊢ (𝜑 → (𝐹:𝑆–1-1→𝑇 ↔ 𝐹:𝑆–1-1-onto→𝑇)) |
| 110 | 83, 109 | mpbid 232 |
1
⊢ (𝜑 → 𝐹:𝑆–1-1-onto→𝑇) |