This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem crth

Description: The Chinese Remainder Theorem: the function that maps x to its remainder classes mod M and mod N is 1-1 and onto when M and N are coprime. (Contributed by Mario Carneiro, 24-Feb-2014) (Proof shortened by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses crth.1 ⊢ 𝑆 = ( 0 ..^ ( 𝑀 · 𝑁 ) )
crth.2 ⊢ 𝑇 = ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) )
crth.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ )
crth.4 ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) )
Assertion crth ( 𝜑 → 𝐹 : 𝑆 –1-1-onto→ 𝑇 )

Proof

Step Hyp Ref Expression
1 crth.1 ⊢ 𝑆 = ( 0 ..^ ( 𝑀 · 𝑁 ) )
2 crth.2 ⊢ 𝑇 = ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) )
3 crth.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ )
4 crth.4 ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) )
5 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) → 𝑥 ∈ ℤ )
6 5 1 eleq2s ⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ℤ )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
8 4 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝑀 ∈ ℕ )
10 zmodfzo ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝑥 mod 𝑀 ) ∈ ( 0 ..^ 𝑀 ) )
11 7 9 10 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑥 mod 𝑀 ) ∈ ( 0 ..^ 𝑀 ) )
12 4 simp2d ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝑁 ∈ ℕ )
14 zmodfzo ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑥 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
15 7 13 14 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑥 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
16 11 15 opelxpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ ∈ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) )
17 16 2 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ ∈ 𝑇 )
18 6 17 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ ∈ 𝑇 )
19 18 3 fmptd ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ 𝑇 )
20 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 mod 𝑀 ) = ( 𝑦 mod 𝑀 ) )
21 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 mod 𝑁 ) = ( 𝑦 mod 𝑁 ) )
22 20 21 opeq12d ⊢ ( 𝑥 = 𝑦 → ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ = ⟨ ( 𝑦 mod 𝑀 ) , ( 𝑦 mod 𝑁 ) ⟩ )
23 opex ⊢ ⟨ ( 𝑦 mod 𝑀 ) , ( 𝑦 mod 𝑁 ) ⟩ ∈ V
24 22 3 23 fvmpt ⊢ ( 𝑦 ∈ 𝑆 → ( 𝐹 ‘ 𝑦 ) = ⟨ ( 𝑦 mod 𝑀 ) , ( 𝑦 mod 𝑁 ) ⟩ )
25 24 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝐹 ‘ 𝑦 ) = ⟨ ( 𝑦 mod 𝑀 ) , ( 𝑦 mod 𝑁 ) ⟩ )
26 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 mod 𝑀 ) = ( 𝑧 mod 𝑀 ) )
27 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 mod 𝑁 ) = ( 𝑧 mod 𝑁 ) )
28 26 27 opeq12d ⊢ ( 𝑥 = 𝑧 → ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ = ⟨ ( 𝑧 mod 𝑀 ) , ( 𝑧 mod 𝑁 ) ⟩ )
29 opex ⊢ ⟨ ( 𝑧 mod 𝑀 ) , ( 𝑧 mod 𝑁 ) ⟩ ∈ V
30 28 3 29 fvmpt ⊢ ( 𝑧 ∈ 𝑆 → ( 𝐹 ‘ 𝑧 ) = ⟨ ( 𝑧 mod 𝑀 ) , ( 𝑧 mod 𝑁 ) ⟩ )
31 30 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝐹 ‘ 𝑧 ) = ⟨ ( 𝑧 mod 𝑀 ) , ( 𝑧 mod 𝑁 ) ⟩ )
32 25 31 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ⟨ ( 𝑦 mod 𝑀 ) , ( 𝑦 mod 𝑁 ) ⟩ = ⟨ ( 𝑧 mod 𝑀 ) , ( 𝑧 mod 𝑁 ) ⟩ ) )
33 ovex ⊢ ( 𝑦 mod 𝑀 ) ∈ V
34 ovex ⊢ ( 𝑦 mod 𝑁 ) ∈ V
35 33 34 opth ⊢ ( ⟨ ( 𝑦 mod 𝑀 ) , ( 𝑦 mod 𝑁 ) ⟩ = ⟨ ( 𝑧 mod 𝑀 ) , ( 𝑧 mod 𝑁 ) ⟩ ↔ ( ( 𝑦 mod 𝑀 ) = ( 𝑧 mod 𝑀 ) ∧ ( 𝑦 mod 𝑁 ) = ( 𝑧 mod 𝑁 ) ) )
36 32 35 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( ( 𝑦 mod 𝑀 ) = ( 𝑧 mod 𝑀 ) ∧ ( 𝑦 mod 𝑁 ) = ( 𝑧 mod 𝑁 ) ) ) )
37 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑀 ∈ ℕ )
38 37 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑀 ∈ ℤ )
39 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑁 ∈ ℕ )
40 39 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑁 ∈ ℤ )
41 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑦 ∈ 𝑆 )
42 41 1 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑦 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) )
43 elfzoelz ⊢ ( 𝑦 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) → 𝑦 ∈ ℤ )
44 42 43 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑦 ∈ ℤ )
45 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ 𝑆 )
46 45 1 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) )
47 elfzoelz ⊢ ( 𝑧 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) → 𝑧 ∈ ℤ )
48 46 47 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ ℤ )
49 44 48 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑦 − 𝑧 ) ∈ ℤ )
50 4 simp3d ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑀 gcd 𝑁 ) = 1 )
52 coprmdvds2 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑦 − 𝑧 ) ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑀 ∥ ( 𝑦 − 𝑧 ) ∧ 𝑁 ∥ ( 𝑦 − 𝑧 ) ) → ( 𝑀 · 𝑁 ) ∥ ( 𝑦 − 𝑧 ) ) )
53 38 40 49 51 52 syl31anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑀 ∥ ( 𝑦 − 𝑧 ) ∧ 𝑁 ∥ ( 𝑦 − 𝑧 ) ) → ( 𝑀 · 𝑁 ) ∥ ( 𝑦 − 𝑧 ) ) )
54 moddvds ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( 𝑦 mod 𝑀 ) = ( 𝑧 mod 𝑀 ) ↔ 𝑀 ∥ ( 𝑦 − 𝑧 ) ) )
55 37 44 48 54 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑦 mod 𝑀 ) = ( 𝑧 mod 𝑀 ) ↔ 𝑀 ∥ ( 𝑦 − 𝑧 ) ) )
56 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( 𝑦 mod 𝑁 ) = ( 𝑧 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝑦 − 𝑧 ) ) )
57 39 44 48 56 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑦 mod 𝑁 ) = ( 𝑧 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝑦 − 𝑧 ) ) )
58 55 57 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( ( 𝑦 mod 𝑀 ) = ( 𝑧 mod 𝑀 ) ∧ ( 𝑦 mod 𝑁 ) = ( 𝑧 mod 𝑁 ) ) ↔ ( 𝑀 ∥ ( 𝑦 − 𝑧 ) ∧ 𝑁 ∥ ( 𝑦 − 𝑧 ) ) ) )
59 44 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑦 ∈ ℝ )
60 37 39 nnmulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑀 · 𝑁 ) ∈ ℕ )
61 60 nnrpd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑀 · 𝑁 ) ∈ ℝ+ )
62 elfzole1 ⊢ ( 𝑦 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) → 0 ≤ 𝑦 )
63 42 62 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 0 ≤ 𝑦 )
64 elfzolt2 ⊢ ( 𝑦 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) → 𝑦 < ( 𝑀 · 𝑁 ) )
65 42 64 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑦 < ( 𝑀 · 𝑁 ) )
66 modid ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( 𝑀 · 𝑁 ) ∈ ℝ+ ) ∧ ( 0 ≤ 𝑦 ∧ 𝑦 < ( 𝑀 · 𝑁 ) ) ) → ( 𝑦 mod ( 𝑀 · 𝑁 ) ) = 𝑦 )
67 59 61 63 65 66 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑦 mod ( 𝑀 · 𝑁 ) ) = 𝑦 )
68 48 zred ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ ℝ )
69 elfzole1 ⊢ ( 𝑧 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) → 0 ≤ 𝑧 )
70 46 69 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 0 ≤ 𝑧 )
71 elfzolt2 ⊢ ( 𝑧 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) → 𝑧 < ( 𝑀 · 𝑁 ) )
72 46 71 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 < ( 𝑀 · 𝑁 ) )
73 modid ⊢ ( ( ( 𝑧 ∈ ℝ ∧ ( 𝑀 · 𝑁 ) ∈ ℝ+ ) ∧ ( 0 ≤ 𝑧 ∧ 𝑧 < ( 𝑀 · 𝑁 ) ) ) → ( 𝑧 mod ( 𝑀 · 𝑁 ) ) = 𝑧 )
74 68 61 70 72 73 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑧 mod ( 𝑀 · 𝑁 ) ) = 𝑧 )
75 67 74 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑦 mod ( 𝑀 · 𝑁 ) ) = ( 𝑧 mod ( 𝑀 · 𝑁 ) ) ↔ 𝑦 = 𝑧 ) )
76 moddvds ⊢ ( ( ( 𝑀 · 𝑁 ) ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( 𝑦 mod ( 𝑀 · 𝑁 ) ) = ( 𝑧 mod ( 𝑀 · 𝑁 ) ) ↔ ( 𝑀 · 𝑁 ) ∥ ( 𝑦 − 𝑧 ) ) )
77 60 44 48 76 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑦 mod ( 𝑀 · 𝑁 ) ) = ( 𝑧 mod ( 𝑀 · 𝑁 ) ) ↔ ( 𝑀 · 𝑁 ) ∥ ( 𝑦 − 𝑧 ) ) )
78 75 77 bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑦 = 𝑧 ↔ ( 𝑀 · 𝑁 ) ∥ ( 𝑦 − 𝑧 ) ) )
79 53 58 78 3imtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( ( 𝑦 mod 𝑀 ) = ( 𝑧 mod 𝑀 ) ∧ ( 𝑦 mod 𝑁 ) = ( 𝑧 mod 𝑁 ) ) → 𝑦 = 𝑧 ) )
80 36 79 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
81 80 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
82 dff13 ⊢ ( 𝐹 : 𝑆 –1-1→ 𝑇 ↔ ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
83 19 81 82 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝑆 –1-1→ 𝑇 )
84 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
85 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
86 nn0mulcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 · 𝑁 ) ∈ ℕ0 )
87 hashfzo0 ⊢ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ) = ( 𝑀 · 𝑁 ) )
88 86 87 syl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ) = ( 𝑀 · 𝑁 ) )
89 fzofi ⊢ ( 0 ..^ 𝑀 ) ∈ Fin
90 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
91 hashxp ⊢ ( ( ( 0 ..^ 𝑀 ) ∈ Fin ∧ ( 0 ..^ 𝑁 ) ∈ Fin ) → ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ) )
92 89 90 91 mp2an ⊢ ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
93 hashfzo0 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑀 ) ) = 𝑀 )
94 hashfzo0 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
95 93 94 oveqan12d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ) = ( 𝑀 · 𝑁 ) )
96 92 95 eqtrid ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) ) = ( 𝑀 · 𝑁 ) )
97 88 96 eqtr4d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ) = ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) ) )
98 fzofi ⊢ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ∈ Fin
99 xpfi ⊢ ( ( ( 0 ..^ 𝑀 ) ∈ Fin ∧ ( 0 ..^ 𝑁 ) ∈ Fin ) → ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) ∈ Fin )
100 89 90 99 mp2an ⊢ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) ∈ Fin
101 hashen ⊢ ( ( ( 0 ..^ ( 𝑀 · 𝑁 ) ) ∈ Fin ∧ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) ∈ Fin ) → ( ( ♯ ‘ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ) = ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) ) ↔ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ≈ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) ) )
102 98 100 101 mp2an ⊢ ( ( ♯ ‘ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ) = ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) ) ↔ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ≈ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) )
103 97 102 sylib ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 0 ..^ ( 𝑀 · 𝑁 ) ) ≈ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) )
104 84 85 103 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 0 ..^ ( 𝑀 · 𝑁 ) ) ≈ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) )
105 8 12 104 syl2anc ⊢ ( 𝜑 → ( 0 ..^ ( 𝑀 · 𝑁 ) ) ≈ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) )
106 105 1 2 3brtr4g ⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )
107 2 100 eqeltri ⊢ 𝑇 ∈ Fin
108 f1finf1o ⊢ ( ( 𝑆 ≈ 𝑇 ∧ 𝑇 ∈ Fin ) → ( 𝐹 : 𝑆 –1-1→ 𝑇 ↔ 𝐹 : 𝑆 –1-1-onto→ 𝑇 ) )
109 106 107 108 sylancl ⊢ ( 𝜑 → ( 𝐹 : 𝑆 –1-1→ 𝑇 ↔ 𝐹 : 𝑆 –1-1-onto→ 𝑇 ) )
110 83 109 mpbid ⊢ ( 𝜑 → 𝐹 : 𝑆 –1-1-onto→ 𝑇 )