Step | Hyp | Ref
| Expression |
1 | | elfzoelz 12339 |
. . . . . 6
⊢ (𝑥 ∈ (0..^(𝑀 · 𝑁)) → 𝑥 ∈ ℤ) |
2 | | crth.1 |
. . . . . 6
⊢ 𝑆 = (0..^(𝑀 · 𝑁)) |
3 | 1, 2 | eleq2s 2706 |
. . . . 5
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ ℤ) |
4 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ) |
5 | | crth.4 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) |
6 | 5 | simp1d 1066 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑀 ∈ ℕ) |
8 | | zmodfzo 12555 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑥 mod 𝑀) ∈ (0..^𝑀)) |
9 | 4, 7, 8 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥 mod 𝑀) ∈ (0..^𝑀)) |
10 | 5 | simp2d 1067 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℕ) |
12 | | zmodfzo 12555 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑥 mod 𝑁) ∈ (0..^𝑁)) |
13 | 4, 11, 12 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥 mod 𝑁) ∈ (0..^𝑁)) |
14 | | opelxpi 5072 |
. . . . . . 7
⊢ (((𝑥 mod 𝑀) ∈ (0..^𝑀) ∧ (𝑥 mod 𝑁) ∈ (0..^𝑁)) → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 ∈ ((0..^𝑀) × (0..^𝑁))) |
15 | 9, 13, 14 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 ∈ ((0..^𝑀) × (0..^𝑁))) |
16 | | crth.2 |
. . . . . 6
⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁)) |
17 | 15, 16 | syl6eleqr 2699 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 ∈ 𝑇) |
18 | 3, 17 | sylan2 490 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 ∈ 𝑇) |
19 | | crth.3 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉) |
20 | 18, 19 | fmptd 6292 |
. . 3
⊢ (𝜑 → 𝐹:𝑆⟶𝑇) |
21 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 mod 𝑀) = (𝑦 mod 𝑀)) |
22 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 mod 𝑁) = (𝑦 mod 𝑁)) |
23 | 21, 22 | opeq12d 4348 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 = 〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉) |
24 | | opex 4859 |
. . . . . . . . 9
⊢
〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉 ∈ V |
25 | 23, 19, 24 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑆 → (𝐹‘𝑦) = 〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉) |
26 | 25 | ad2antrl 760 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹‘𝑦) = 〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉) |
27 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 mod 𝑀) = (𝑧 mod 𝑀)) |
28 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 mod 𝑁) = (𝑧 mod 𝑁)) |
29 | 27, 28 | opeq12d 4348 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉 = 〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉) |
30 | | opex 4859 |
. . . . . . . . 9
⊢
〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉 ∈ V |
31 | 29, 19, 30 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 → (𝐹‘𝑧) = 〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉) |
32 | 31 | ad2antll 761 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹‘𝑧) = 〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉) |
33 | 26, 32 | eqeq12d 2625 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ 〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉 = 〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉)) |
34 | | ovex 6577 |
. . . . . . 7
⊢ (𝑦 mod 𝑀) ∈ V |
35 | | ovex 6577 |
. . . . . . 7
⊢ (𝑦 mod 𝑁) ∈ V |
36 | 34, 35 | opth 4871 |
. . . . . 6
⊢
(〈(𝑦 mod 𝑀), (𝑦 mod 𝑁)〉 = 〈(𝑧 mod 𝑀), (𝑧 mod 𝑁)〉 ↔ ((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ∧ (𝑦 mod 𝑁) = (𝑧 mod 𝑁))) |
37 | 33, 36 | syl6bb 275 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ ((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ∧ (𝑦 mod 𝑁) = (𝑧 mod 𝑁)))) |
38 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑀 ∈ ℕ) |
39 | 38 | nnzd 11357 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑀 ∈ ℤ) |
40 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑁 ∈ ℕ) |
41 | 40 | nnzd 11357 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑁 ∈ ℤ) |
42 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
43 | 42, 2 | syl6eleq 2698 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 ∈ (0..^(𝑀 · 𝑁))) |
44 | | elfzoelz 12339 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 𝑦 ∈ ℤ) |
45 | 43, 44 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 ∈ ℤ) |
46 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ 𝑆) |
47 | 46, 2 | syl6eleq 2698 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ (0..^(𝑀 · 𝑁))) |
48 | | elfzoelz 12339 |
. . . . . . . . 9
⊢ (𝑧 ∈ (0..^(𝑀 · 𝑁)) → 𝑧 ∈ ℤ) |
49 | 47, 48 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ ℤ) |
50 | 45, 49 | zsubcld 11363 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦 − 𝑧) ∈ ℤ) |
51 | 5 | simp3d 1068 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) |
52 | 51 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑀 gcd 𝑁) = 1) |
53 | | coprmdvds2 15206 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑦 − 𝑧) ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 ∥ (𝑦 − 𝑧) ∧ 𝑁 ∥ (𝑦 − 𝑧)) → (𝑀 · 𝑁) ∥ (𝑦 − 𝑧))) |
54 | 39, 41, 50, 52, 53 | syl31anc 1321 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑀 ∥ (𝑦 − 𝑧) ∧ 𝑁 ∥ (𝑦 − 𝑧)) → (𝑀 · 𝑁) ∥ (𝑦 − 𝑧))) |
55 | | moddvds 14829 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ↔ 𝑀 ∥ (𝑦 − 𝑧))) |
56 | 38, 45, 49, 55 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ↔ 𝑀 ∥ (𝑦 − 𝑧))) |
57 | | moddvds 14829 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑦 mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ (𝑦 − 𝑧))) |
58 | 40, 45, 49, 57 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦 mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ (𝑦 − 𝑧))) |
59 | 56, 58 | anbi12d 743 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ∧ (𝑦 mod 𝑁) = (𝑧 mod 𝑁)) ↔ (𝑀 ∥ (𝑦 − 𝑧) ∧ 𝑁 ∥ (𝑦 − 𝑧)))) |
60 | 45 | zred 11358 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 ∈ ℝ) |
61 | 38, 40 | nnmulcld 10945 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑀 · 𝑁) ∈ ℕ) |
62 | 61 | nnrpd 11746 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑀 · 𝑁) ∈
ℝ+) |
63 | | elfzole1 12347 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 0 ≤ 𝑦) |
64 | 43, 63 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 0 ≤ 𝑦) |
65 | | elfzolt2 12348 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 𝑦 < (𝑀 · 𝑁)) |
66 | 43, 65 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 < (𝑀 · 𝑁)) |
67 | | modid 12557 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℝ ∧ (𝑀 · 𝑁) ∈ ℝ+) ∧ (0 ≤
𝑦 ∧ 𝑦 < (𝑀 · 𝑁))) → (𝑦 mod (𝑀 · 𝑁)) = 𝑦) |
68 | 60, 62, 64, 66, 67 | syl22anc 1319 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦 mod (𝑀 · 𝑁)) = 𝑦) |
69 | 49 | zred 11358 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ ℝ) |
70 | | elfzole1 12347 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0..^(𝑀 · 𝑁)) → 0 ≤ 𝑧) |
71 | 47, 70 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 0 ≤ 𝑧) |
72 | | elfzolt2 12348 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0..^(𝑀 · 𝑁)) → 𝑧 < (𝑀 · 𝑁)) |
73 | 47, 72 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 < (𝑀 · 𝑁)) |
74 | | modid 12557 |
. . . . . . . . 9
⊢ (((𝑧 ∈ ℝ ∧ (𝑀 · 𝑁) ∈ ℝ+) ∧ (0 ≤
𝑧 ∧ 𝑧 < (𝑀 · 𝑁))) → (𝑧 mod (𝑀 · 𝑁)) = 𝑧) |
75 | 69, 62, 71, 73, 74 | syl22anc 1319 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑧 mod (𝑀 · 𝑁)) = 𝑧) |
76 | 68, 75 | eqeq12d 2625 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦 mod (𝑀 · 𝑁)) = (𝑧 mod (𝑀 · 𝑁)) ↔ 𝑦 = 𝑧)) |
77 | | moddvds 14829 |
. . . . . . . 8
⊢ (((𝑀 · 𝑁) ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑦 mod (𝑀 · 𝑁)) = (𝑧 mod (𝑀 · 𝑁)) ↔ (𝑀 · 𝑁) ∥ (𝑦 − 𝑧))) |
78 | 61, 45, 49, 77 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦 mod (𝑀 · 𝑁)) = (𝑧 mod (𝑀 · 𝑁)) ↔ (𝑀 · 𝑁) ∥ (𝑦 − 𝑧))) |
79 | 76, 78 | bitr3d 269 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦 = 𝑧 ↔ (𝑀 · 𝑁) ∥ (𝑦 − 𝑧))) |
80 | 54, 59, 79 | 3imtr4d 282 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (((𝑦 mod 𝑀) = (𝑧 mod 𝑀) ∧ (𝑦 mod 𝑁) = (𝑧 mod 𝑁)) → 𝑦 = 𝑧)) |
81 | 37, 80 | sylbid 229 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
82 | 81 | ralrimivva 2954 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
83 | | dff13 6416 |
. . 3
⊢ (𝐹:𝑆–1-1→𝑇 ↔ (𝐹:𝑆⟶𝑇 ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧))) |
84 | 20, 82, 83 | sylanbrc 695 |
. 2
⊢ (𝜑 → 𝐹:𝑆–1-1→𝑇) |
85 | | nnnn0 11176 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
86 | | nnnn0 11176 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
87 | | nn0mulcl 11206 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 · 𝑁) ∈
ℕ0) |
88 | | hashfzo0 13077 |
. . . . . . . . 9
⊢ ((𝑀 · 𝑁) ∈ ℕ0 →
(#‘(0..^(𝑀 ·
𝑁))) = (𝑀 · 𝑁)) |
89 | 87, 88 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (#‘(0..^(𝑀 · 𝑁))) = (𝑀 · 𝑁)) |
90 | | fzofi 12635 |
. . . . . . . . . 10
⊢
(0..^𝑀) ∈
Fin |
91 | | fzofi 12635 |
. . . . . . . . . 10
⊢
(0..^𝑁) ∈
Fin |
92 | | hashxp 13081 |
. . . . . . . . . 10
⊢
(((0..^𝑀) ∈ Fin
∧ (0..^𝑁) ∈ Fin)
→ (#‘((0..^𝑀)
× (0..^𝑁))) =
((#‘(0..^𝑀)) ·
(#‘(0..^𝑁)))) |
93 | 90, 91, 92 | mp2an 704 |
. . . . . . . . 9
⊢
(#‘((0..^𝑀)
× (0..^𝑁))) =
((#‘(0..^𝑀)) ·
(#‘(0..^𝑁))) |
94 | | hashfzo0 13077 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (#‘(0..^𝑀)) =
𝑀) |
95 | | hashfzo0 13077 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (#‘(0..^𝑁)) =
𝑁) |
96 | 94, 95 | oveqan12d 6568 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((#‘(0..^𝑀)) · (#‘(0..^𝑁))) = (𝑀 · 𝑁)) |
97 | 93, 96 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (#‘((0..^𝑀) × (0..^𝑁))) = (𝑀 · 𝑁)) |
98 | 89, 97 | eqtr4d 2647 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (#‘(0..^(𝑀 · 𝑁))) = (#‘((0..^𝑀) × (0..^𝑁)))) |
99 | | fzofi 12635 |
. . . . . . . 8
⊢
(0..^(𝑀 ·
𝑁)) ∈
Fin |
100 | | xpfi 8116 |
. . . . . . . . 9
⊢
(((0..^𝑀) ∈ Fin
∧ (0..^𝑁) ∈ Fin)
→ ((0..^𝑀) ×
(0..^𝑁)) ∈
Fin) |
101 | 90, 91, 100 | mp2an 704 |
. . . . . . . 8
⊢
((0..^𝑀) ×
(0..^𝑁)) ∈
Fin |
102 | | hashen 12997 |
. . . . . . . 8
⊢
(((0..^(𝑀 ·
𝑁)) ∈ Fin ∧
((0..^𝑀) × (0..^𝑁)) ∈ Fin) →
((#‘(0..^(𝑀 ·
𝑁))) = (#‘((0..^𝑀) × (0..^𝑁))) ↔ (0..^(𝑀 · 𝑁)) ≈ ((0..^𝑀) × (0..^𝑁)))) |
103 | 99, 101, 102 | mp2an 704 |
. . . . . . 7
⊢
((#‘(0..^(𝑀
· 𝑁))) =
(#‘((0..^𝑀) ×
(0..^𝑁))) ↔
(0..^(𝑀 · 𝑁)) ≈ ((0..^𝑀) × (0..^𝑁))) |
104 | 98, 103 | sylib 207 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (0..^(𝑀 · 𝑁)) ≈ ((0..^𝑀) × (0..^𝑁))) |
105 | 85, 86, 104 | syl2an 493 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(0..^(𝑀 · 𝑁)) ≈ ((0..^𝑀) × (0..^𝑁))) |
106 | 6, 10, 105 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (0..^(𝑀 · 𝑁)) ≈ ((0..^𝑀) × (0..^𝑁))) |
107 | 106, 2, 16 | 3brtr4g 4617 |
. . 3
⊢ (𝜑 → 𝑆 ≈ 𝑇) |
108 | 16, 101 | eqeltri 2684 |
. . 3
⊢ 𝑇 ∈ Fin |
109 | | f1finf1o 8072 |
. . 3
⊢ ((𝑆 ≈ 𝑇 ∧ 𝑇 ∈ Fin) → (𝐹:𝑆–1-1→𝑇 ↔ 𝐹:𝑆–1-1-onto→𝑇)) |
110 | 107, 108,
109 | sylancl 693 |
. 2
⊢ (𝜑 → (𝐹:𝑆–1-1→𝑇 ↔ 𝐹:𝑆–1-1-onto→𝑇)) |
111 | 84, 110 | mpbid 221 |
1
⊢ (𝜑 → 𝐹:𝑆–1-1-onto→𝑇) |