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	syl5eq	⊢ ( ( 𝑀 ∈ ℕ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→ 𝑇 )