Metamath Proof Explorer

Theorem erdszelem9

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses erdsze.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
erdsze.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
erdszelem.i ⊢ 𝐼 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
erdszelem.j ⊢ 𝐽 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
erdszelem.t ⊢ 𝑇 = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ⟨ ( 𝐼 ‘ 𝑛 ) , ( 𝐽 ‘ 𝑛 ) ⟩ )
Assertion erdszelem9 ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) –1-1→ ( ℕ × ℕ ) )

Proof

Step Hyp Ref Expression
1 erdsze.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 erdsze.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
3 erdszelem.i ⊢ 𝐼 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
4 erdszelem.j ⊢ 𝐽 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
5 erdszelem.t ⊢ 𝑇 = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ⟨ ( 𝐼 ‘ 𝑛 ) , ( 𝐽 ‘ 𝑛 ) ⟩ )
6 ltso ⊢ < Or ℝ
7 1 2 3 6 erdszelem6 ⊢ ( 𝜑 → 𝐼 : ( 1 ... 𝑁 ) ⟶ ℕ )
8 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝐼 ‘ 𝑛 ) ∈ ℕ )
9 gtso ⊢ ◡ < Or ℝ
10 1 2 4 9 erdszelem6 ⊢ ( 𝜑 → 𝐽 : ( 1 ... 𝑁 ) ⟶ ℕ )
11 10 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝐽 ‘ 𝑛 ) ∈ ℕ )
12 opelxpi ⊢ ( ( ( 𝐼 ‘ 𝑛 ) ∈ ℕ ∧ ( 𝐽 ‘ 𝑛 ) ∈ ℕ ) → ⟨ ( 𝐼 ‘ 𝑛 ) , ( 𝐽 ‘ 𝑛 ) ⟩ ∈ ( ℕ × ℕ ) )
13 8 11 12 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ⟨ ( 𝐼 ‘ 𝑛 ) , ( 𝐽 ‘ 𝑛 ) ⟩ ∈ ( ℕ × ℕ ) )
14 13 5 fmptd ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ( ℕ × ℕ ) )
15 fveq2 ⊢ ( 𝑎 = 𝑧 → ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ 𝑧 ) )
16 fveq2 ⊢ ( 𝑏 = 𝑤 → ( 𝑇 ‘ 𝑏 ) = ( 𝑇 ‘ 𝑤 ) )
17 15 16 eqeqan12d ⊢ ( ( 𝑎 = 𝑧 ∧ 𝑏 = 𝑤 ) → ( ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ 𝑏 ) ↔ ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) ) )
18 eqeq12 ⊢ ( ( 𝑎 = 𝑧 ∧ 𝑏 = 𝑤 ) → ( 𝑎 = 𝑏 ↔ 𝑧 = 𝑤 ) )
19 17 18 imbi12d ⊢ ( ( 𝑎 = 𝑧 ∧ 𝑏 = 𝑤 ) → ( ( ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ↔ ( ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
20 fveq2 ⊢ ( 𝑎 = 𝑤 → ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ 𝑤 ) )
21 fveq2 ⊢ ( 𝑏 = 𝑧 → ( 𝑇 ‘ 𝑏 ) = ( 𝑇 ‘ 𝑧 ) )
22 20 21 eqeqan12d ⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑧 ) → ( ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ 𝑏 ) ↔ ( 𝑇 ‘ 𝑤 ) = ( 𝑇 ‘ 𝑧 ) ) )
23 eqcom ⊢ ( ( 𝑇 ‘ 𝑤 ) = ( 𝑇 ‘ 𝑧 ) ↔ ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) )
24 22 23 bitrdi ⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑧 ) → ( ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ 𝑏 ) ↔ ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) ) )
25 eqeq12 ⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑧 ) → ( 𝑎 = 𝑏 ↔ 𝑤 = 𝑧 ) )
26 eqcom ⊢ ( 𝑤 = 𝑧 ↔ 𝑧 = 𝑤 )
27 25 26 bitrdi ⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑧 ) → ( 𝑎 = 𝑏 ↔ 𝑧 = 𝑤 ) )
28 24 27 imbi12d ⊢ ( ( 𝑎 = 𝑤 ∧ 𝑏 = 𝑧 ) → ( ( ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ↔ ( ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
29 elfzelz ⊢ ( 𝑧 ∈ ( 1 ... 𝑁 ) → 𝑧 ∈ ℤ )
30 29 zred ⊢ ( 𝑧 ∈ ( 1 ... 𝑁 ) → 𝑧 ∈ ℝ )
31 30 ssriv ⊢ ( 1 ... 𝑁 ) ⊆ ℝ
32 31 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℝ )
33 biidd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
34 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → 𝑧 ∈ ( 1 ... 𝑁 ) )
35 fveq2 ⊢ ( 𝑛 = 𝑧 → ( 𝐼 ‘ 𝑛 ) = ( 𝐼 ‘ 𝑧 ) )
36 fveq2 ⊢ ( 𝑛 = 𝑧 → ( 𝐽 ‘ 𝑛 ) = ( 𝐽 ‘ 𝑧 ) )
37 35 36 opeq12d ⊢ ( 𝑛 = 𝑧 → ⟨ ( 𝐼 ‘ 𝑛 ) , ( 𝐽 ‘ 𝑛 ) ⟩ = ⟨ ( 𝐼 ‘ 𝑧 ) , ( 𝐽 ‘ 𝑧 ) ⟩ )
38 opex ⊢ ⟨ ( 𝐼 ‘ 𝑧 ) , ( 𝐽 ‘ 𝑧 ) ⟩ ∈ V
39 37 5 38 fvmpt ⊢ ( 𝑧 ∈ ( 1 ... 𝑁 ) → ( 𝑇 ‘ 𝑧 ) = ⟨ ( 𝐼 ‘ 𝑧 ) , ( 𝐽 ‘ 𝑧 ) ⟩ )
40 34 39 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( 𝑇 ‘ 𝑧 ) = ⟨ ( 𝐼 ‘ 𝑧 ) , ( 𝐽 ‘ 𝑧 ) ⟩ )
41 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → 𝑤 ∈ ( 1 ... 𝑁 ) )
42 fveq2 ⊢ ( 𝑛 = 𝑤 → ( 𝐼 ‘ 𝑛 ) = ( 𝐼 ‘ 𝑤 ) )
43 fveq2 ⊢ ( 𝑛 = 𝑤 → ( 𝐽 ‘ 𝑛 ) = ( 𝐽 ‘ 𝑤 ) )
44 42 43 opeq12d ⊢ ( 𝑛 = 𝑤 → ⟨ ( 𝐼 ‘ 𝑛 ) , ( 𝐽 ‘ 𝑛 ) ⟩ = ⟨ ( 𝐼 ‘ 𝑤 ) , ( 𝐽 ‘ 𝑤 ) ⟩ )
45 opex ⊢ ⟨ ( 𝐼 ‘ 𝑤 ) , ( 𝐽 ‘ 𝑤 ) ⟩ ∈ V
46 44 5 45 fvmpt ⊢ ( 𝑤 ∈ ( 1 ... 𝑁 ) → ( 𝑇 ‘ 𝑤 ) = ⟨ ( 𝐼 ‘ 𝑤 ) , ( 𝐽 ‘ 𝑤 ) ⟩ )
47 41 46 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( 𝑇 ‘ 𝑤 ) = ⟨ ( 𝐼 ‘ 𝑤 ) , ( 𝐽 ‘ 𝑤 ) ⟩ )
48 40 47 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) ↔ ⟨ ( 𝐼 ‘ 𝑧 ) , ( 𝐽 ‘ 𝑧 ) ⟩ = ⟨ ( 𝐼 ‘ 𝑤 ) , ( 𝐽 ‘ 𝑤 ) ⟩ ) )
49 fvex ⊢ ( 𝐼 ‘ 𝑧 ) ∈ V
50 fvex ⊢ ( 𝐽 ‘ 𝑧 ) ∈ V
51 49 50 opth ⊢ ( ⟨ ( 𝐼 ‘ 𝑧 ) , ( 𝐽 ‘ 𝑧 ) ⟩ = ⟨ ( 𝐼 ‘ 𝑤 ) , ( 𝐽 ‘ 𝑤 ) ⟩ ↔ ( ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑤 ) ∧ ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 𝑤 ) ) )
52 34 30 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → 𝑧 ∈ ℝ )
53 31 41 sselid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → 𝑤 ∈ ℝ )
54 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → 𝑧 ≤ 𝑤 )
55 52 53 54 leltned ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( 𝑧 < 𝑤 ↔ 𝑤 ≠ 𝑧 ) )
56 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
57 f1fveq ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ 𝑧 = 𝑤 ) )
58 56 34 41 57 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ 𝑧 = 𝑤 ) )
59 58 26 bitr4di ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ 𝑤 = 𝑧 ) )
60 59 necon3bid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ↔ 𝑤 ≠ 𝑧 ) )
61 55 60 bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( 𝑧 < 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ) )
62 61 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) )
63 f1f ⊢ ( 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ → 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ )
64 2 63 syl ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ )
65 64 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → 𝐹 : ( 1 ... 𝑁 ) ⟶ ℝ )
66 34 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → 𝑧 ∈ ( 1 ... 𝑁 ) )
67 65 66 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
68 41 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → 𝑤 ∈ ( 1 ... 𝑁 ) )
69 65 68 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → ( 𝐹 ‘ 𝑤 ) ∈ ℝ )
70 67 69 lttri2d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ↔ ( ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) < ( 𝐹 ‘ 𝑧 ) ) ) )
71 62 70 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) < ( 𝐹 ‘ 𝑧 ) ) )
72 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → 𝑁 ∈ ℕ )
73 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
74 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → 𝑧 < 𝑤 )
75 72 73 3 6 66 68 74 erdszelem8 ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → ( ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑤 ) → ¬ ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ) )
76 72 73 4 9 66 68 74 erdszelem8 ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → ( ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 𝑤 ) → ¬ ( 𝐹 ‘ 𝑧 ) ◡ < ( 𝐹 ‘ 𝑤 ) ) )
77 75 76 anim12d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → ( ( ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑤 ) ∧ ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 𝑤 ) ) → ( ¬ ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ∧ ¬ ( 𝐹 ‘ 𝑧 ) ◡ < ( 𝐹 ‘ 𝑤 ) ) ) )
78 ioran ⊢ ( ¬ ( ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) < ( 𝐹 ‘ 𝑧 ) ) ↔ ( ¬ ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ∧ ¬ ( 𝐹 ‘ 𝑤 ) < ( 𝐹 ‘ 𝑧 ) ) )
79 fvex ⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
80 fvex ⊢ ( 𝐹 ‘ 𝑤 ) ∈ V
81 79 80 brcnv ⊢ ( ( 𝐹 ‘ 𝑧 ) ◡ < ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) < ( 𝐹 ‘ 𝑧 ) )
82 81 notbii ⊢ ( ¬ ( 𝐹 ‘ 𝑧 ) ◡ < ( 𝐹 ‘ 𝑤 ) ↔ ¬ ( 𝐹 ‘ 𝑤 ) < ( 𝐹 ‘ 𝑧 ) )
83 82 anbi2i ⊢ ( ( ¬ ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ∧ ¬ ( 𝐹 ‘ 𝑧 ) ◡ < ( 𝐹 ‘ 𝑤 ) ) ↔ ( ¬ ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ∧ ¬ ( 𝐹 ‘ 𝑤 ) < ( 𝐹 ‘ 𝑧 ) ) )
84 78 83 bitr4i ⊢ ( ¬ ( ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) < ( 𝐹 ‘ 𝑧 ) ) ↔ ( ¬ ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ∧ ¬ ( 𝐹 ‘ 𝑧 ) ◡ < ( 𝐹 ‘ 𝑤 ) ) )
85 77 84 imbitrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → ( ( ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑤 ) ∧ ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 𝑤 ) ) → ¬ ( ( 𝐹 ‘ 𝑧 ) < ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) < ( 𝐹 ‘ 𝑧 ) ) ) )
86 71 85 mt2d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) ∧ 𝑧 < 𝑤 ) → ¬ ( ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑤 ) ∧ ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 𝑤 ) ) )
87 86 ex ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( 𝑧 < 𝑤 → ¬ ( ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑤 ) ∧ ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 𝑤 ) ) ) )
88 55 87 sylbird ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( 𝑤 ≠ 𝑧 → ¬ ( ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑤 ) ∧ ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 𝑤 ) ) ) )
89 88 necon4ad ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( ( ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑤 ) ∧ ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 𝑤 ) ) → 𝑤 = 𝑧 ) )
90 51 89 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( ⟨ ( 𝐼 ‘ 𝑧 ) , ( 𝐽 ‘ 𝑧 ) ⟩ = ⟨ ( 𝐼 ‘ 𝑤 ) , ( 𝐽 ‘ 𝑤 ) ⟩ → 𝑤 = 𝑧 ) )
91 48 90 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) → 𝑤 = 𝑧 ) )
92 91 26 imbitrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ≤ 𝑤 ) ) → ( ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
93 19 28 32 33 92 wlogle ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... 𝑁 ) ∧ 𝑤 ∈ ( 1 ... 𝑁 ) ) ) → ( ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
94 93 ralrimivva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 ... 𝑁 ) ∀ 𝑤 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
95 dff13 ⊢ ( 𝑇 : ( 1 ... 𝑁 ) –1-1→ ( ℕ × ℕ ) ↔ ( 𝑇 : ( 1 ... 𝑁 ) ⟶ ( ℕ × ℕ ) ∧ ∀ 𝑧 ∈ ( 1 ... 𝑁 ) ∀ 𝑤 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
96 14 94 95 sylanbrc ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) –1-1→ ( ℕ × ℕ ) )