Metamath Proof Explorer

Theorem poimirlem1

Description: Lemma for poimir - the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
poimirlem2.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
poimirlem2.2 ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ℤ )
poimirlem2.3 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
poimirlem1.4 ⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
Assertion poimirlem1 ( 𝜑 → ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 poimirlem2.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
3 poimirlem2.2 ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ℤ )
4 poimirlem2.3 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
5 poimirlem1.4 ⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
6 f1of ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
7 4 6 syl ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
8 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
9 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
10 8 9 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
11 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
12 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
13 uzid ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
14 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
15 11 12 13 14 4syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
16 10 15 eqeltrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
17 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
18 16 17 syl ⊢ ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
19 18 5 sseldd ⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... 𝑁 ) )
20 7 19 ffvelrnd ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑀 ) ∈ ( 1 ... 𝑁 ) )
21 fzp1elp1 ⊢ ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑀 + 1 ) ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
22 5 21 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
23 10 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
24 22 23 eleqtrd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) )
25 7 24 ffvelrnd ⊢ ( 𝜑 → ( 𝑈 ‘ ( 𝑀 + 1 ) ) ∈ ( 1 ... 𝑁 ) )
26 imassrn ⊢ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ⊆ ran 𝑈
27 frn ⊢ ( 𝑈 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) → ran 𝑈 ⊆ ( 1 ... 𝑁 ) )
28 4 6 27 3syl ⊢ ( 𝜑 → ran 𝑈 ⊆ ( 1 ... 𝑁 ) )
29 26 28 sstrid ⊢ ( 𝜑 → ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ⊆ ( 1 ... 𝑁 ) )
30 29 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
31 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑛 ) ∈ ℤ )
32 31 zred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑛 ) ∈ ℝ )
33 32 ltp1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑛 ) < ( ( 𝑇 ‘ 𝑛 ) + 1 ) )
34 32 33 ltned ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑛 ) ≠ ( ( 𝑇 ‘ 𝑛 ) + 1 ) )
35 30 34 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( 𝑇 ‘ 𝑛 ) ≠ ( ( 𝑇 ‘ 𝑛 ) + 1 ) )
36 breq1 ⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( 𝑦 < 𝑀 ↔ ( 𝑀 − 1 ) < 𝑀 ) )
37 id ⊢ ( 𝑦 = ( 𝑀 − 1 ) → 𝑦 = ( 𝑀 − 1 ) )
38 36 37 ifbieq1d ⊢ ( 𝑦 = ( 𝑀 − 1 ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = if ( ( 𝑀 − 1 ) < 𝑀 , ( 𝑀 − 1 ) , ( 𝑦 + 1 ) ) )
39 elfzelz ⊢ ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑀 ∈ ℤ )
40 5 39 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
41 40 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
42 41 ltm1d ⊢ ( 𝜑 → ( 𝑀 − 1 ) < 𝑀 )
43 42 iftrued ⊢ ( 𝜑 → if ( ( 𝑀 − 1 ) < 𝑀 , ( 𝑀 − 1 ) , ( 𝑦 + 1 ) ) = ( 𝑀 − 1 ) )
44 38 43 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑀 − 1 ) ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑀 − 1 ) )
45 44 csbeq1d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑀 − 1 ) ) → ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ ( 𝑀 − 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
46 11 12 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
47 elfzm1b ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( 𝑀 − 1 ) ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ) )
48 40 46 47 syl2anc ⊢ ( 𝜑 → ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↔ ( 𝑀 − 1 ) ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ) )
49 5 48 mpbid ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) )
50 oveq2 ⊢ ( 𝑗 = ( 𝑀 − 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑀 − 1 ) ) )
51 50 imaeq2d ⊢ ( 𝑗 = ( 𝑀 − 1 ) → ( 𝑈 “ ( 1 ... 𝑗 ) ) = ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) )
52 51 xpeq1d ⊢ ( 𝑗 = ( 𝑀 − 1 ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) )
54 oveq1 ⊢ ( 𝑗 = ( 𝑀 − 1 ) → ( 𝑗 + 1 ) = ( ( 𝑀 − 1 ) + 1 ) )
55 40 zcnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
56 npcan1 ⊢ ( 𝑀 ∈ ℂ → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
57 55 56 syl ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
58 54 57 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( 𝑗 + 1 ) = 𝑀 )
59 58 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( 𝑀 ... 𝑁 ) )
60 59 imaeq2d ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) )
61 60 xpeq1d ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) )
62 53 61 uneq12d ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) )
63 62 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑀 − 1 ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) )
64 49 63 csbied ⊢ ( 𝜑 → ⦋ ( 𝑀 − 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑀 − 1 ) ) → ⦋ ( 𝑀 − 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) )
66 45 65 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑀 − 1 ) ) → ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) )
67 46 zcnd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℂ )
68 npcan1 ⊢ ( ( 𝑁 − 1 ) ∈ ℂ → ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) = ( 𝑁 − 1 ) )
69 67 68 syl ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) = ( 𝑁 − 1 ) )
70 peano2zm ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( ( 𝑁 − 1 ) − 1 ) ∈ ℤ )
71 uzid ⊢ ( ( ( 𝑁 − 1 ) − 1 ) ∈ ℤ → ( ( 𝑁 − 1 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) − 1 ) ) )
72 peano2uz ⊢ ( ( ( 𝑁 − 1 ) − 1 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) − 1 ) ) → ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) − 1 ) ) )
73 46 70 71 72 4syl ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) − 1 ) ) )
74 69 73 eqeltrrd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) − 1 ) ) )
75 fzss2 ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) − 1 ) ) → ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ⊆ ( 0 ... ( 𝑁 − 1 ) ) )
76 74 75 syl ⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ⊆ ( 0 ... ( 𝑁 − 1 ) ) )
77 76 49 sseldd ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
78 ovexd ⊢ ( 𝜑 → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ∈ V )
79 2 66 77 78 fvmptd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑀 − 1 ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) )
80 79 fveq1d ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
82 3 ffnd ⊢ ( 𝜑 → 𝑇 Fn ( 1 ... 𝑁 ) )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → 𝑇 Fn ( 1 ... 𝑁 ) )
84 1ex ⊢ 1 ∈ V
85 fnconstg ⊢ ( 1 ∈ V → ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) )
86 84 85 ax-mp ⊢ ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) )
87 c0ex ⊢ 0 ∈ V
88 fnconstg ⊢ ( 0 ∈ V → ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) )
89 87 88 ax-mp ⊢ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑀 ... 𝑁 ) )
90 86 89 pm3.2i ⊢ ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∧ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) )
91 dff1o3 ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ◡ 𝑈 ) )
92 91 simprbi ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ◡ 𝑈 )
93 imain ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) )
94 4 92 93 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) )
95 fzdisj ⊢ ( ( 𝑀 − 1 ) < 𝑀 → ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) = ∅ )
96 42 95 syl ⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) = ∅ )
97 96 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
98 ima0 ⊢ ( 𝑈 “ ∅ ) = ∅
99 97 98 eqtrdi ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑁 ) ) ) = ∅ )
100 94 99 eqtr3d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) = ∅ )
101 fnun ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∧ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) ∧ ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) = ∅ ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) )
102 90 100 101 sylancr ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) )
103 elfzuz ⊢ ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
104 5 103 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
105 57 104 eqeltrd ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
106 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
107 uzid ⊢ ( ( 𝑀 − 1 ) ∈ ℤ → ( 𝑀 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
108 peano2uz ⊢ ( ( 𝑀 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) → ( ( 𝑀 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
109 40 106 107 108 4syl ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
110 57 109 eqeltrrd ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
111 peano2uz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
112 uzss ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) → ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
113 110 111 112 3syl ⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
114 elfzuz3 ⊢ ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
115 eluzp1p1 ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
116 5 114 115 3syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
117 10 116 eqeltrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
118 113 117 sseldd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
119 fzsplit2 ⊢ ( ( ( ( 𝑀 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑁 ) ) )
120 105 118 119 syl2anc ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑁 ) ) )
121 57 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑁 ) = ( 𝑀 ... 𝑁 ) )
122 121 uneq2d ⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( ( ( 𝑀 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑁 ) ) )
123 120 122 eqtrd ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑁 ) ) )
124 123 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 𝑈 “ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑁 ) ) ) )
125 imaundi ⊢ ( 𝑈 “ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) )
126 124 125 eqtrdi ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) )
127 f1ofo ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
128 foima ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
129 4 127 128 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
130 126 129 eqtr3d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
131 130 fneq2d ⊢ ( 𝜑 → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) ↔ ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) ) )
132 102 131 mpbid ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
133 132 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
134 ovexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( 1 ... 𝑁 ) ∈ V )
135 inidm ⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
136 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
137 100 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) = ∅ )
138 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝑀 ... ( 𝑀 + 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) )
139 imass2 ⊢ ( ( 𝑀 ... ( 𝑀 + 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) → ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ⊆ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) )
140 117 138 139 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ⊆ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) )
141 140 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) )
142 fvun2 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∧ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ∧ ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
143 86 89 142 mp3an12 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
144 137 141 143 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
145 87 fvconst2 ⊢ ( 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) = 0 )
146 141 145 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) = 0 )
147 144 146 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
148 147 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
149 83 133 134 134 135 136 148 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 0 ) )
150 30 149 mpdan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑀 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 0 ) )
151 31 zcnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑛 ) ∈ ℂ )
152 151 addid1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ‘ 𝑛 ) + 0 ) = ( 𝑇 ‘ 𝑛 ) )
153 30 152 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( 𝑇 ‘ 𝑛 ) + 0 ) = ( 𝑇 ‘ 𝑛 ) )
154 81 150 153 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
155 breq1 ⊢ ( 𝑦 = 𝑀 → ( 𝑦 < 𝑀 ↔ 𝑀 < 𝑀 ) )
156 oveq1 ⊢ ( 𝑦 = 𝑀 → ( 𝑦 + 1 ) = ( 𝑀 + 1 ) )
157 155 156 ifbieq2d ⊢ ( 𝑦 = 𝑀 → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑀 < 𝑀 , 𝑦 , ( 𝑀 + 1 ) ) )
158 41 ltnrd ⊢ ( 𝜑 → ¬ 𝑀 < 𝑀 )
159 158 iffalsed ⊢ ( 𝜑 → if ( 𝑀 < 𝑀 , 𝑦 , ( 𝑀 + 1 ) ) = ( 𝑀 + 1 ) )
160 157 159 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑀 + 1 ) )
161 160 csbeq1d ⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ ( 𝑀 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
162 ovex ⊢ ( 𝑀 + 1 ) ∈ V
163 oveq2 ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑀 + 1 ) ) )
164 163 imaeq2d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑈 “ ( 1 ... 𝑗 ) ) = ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) )
165 164 xpeq1d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) )
166 oveq1 ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑗 + 1 ) = ( ( 𝑀 + 1 ) + 1 ) )
167 166 oveq1d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) )
168 167 imaeq2d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) )
169 168 xpeq1d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
170 165 169 uneq12d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
171 170 oveq2d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
172 162 171 csbie ⊢ ⦋ ( 𝑀 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
173 161 172 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
174 fz1ssfz0 ⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( 𝑁 − 1 ) )
175 174 5 sseldi ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
176 ovexd ⊢ ( 𝜑 → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V )
177 2 173 175 176 fvmptd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
178 177 fveq1d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
179 178 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
180 fnconstg ⊢ ( 1 ∈ V → ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) )
181 84 180 ax-mp ⊢ ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) )
182 fnconstg ⊢ ( 0 ∈ V → ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) )
183 87 182 ax-mp ⊢ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) )
184 181 183 pm3.2i ⊢ ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∧ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) )
185 imain ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... ( 𝑀 + 1 ) ) ∩ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) )
186 4 92 185 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑀 + 1 ) ) ∩ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) )
187 peano2re ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 + 1 ) ∈ ℝ )
188 41 187 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℝ )
189 188 ltp1d ⊢ ( 𝜑 → ( 𝑀 + 1 ) < ( ( 𝑀 + 1 ) + 1 ) )
190 fzdisj ⊢ ( ( 𝑀 + 1 ) < ( ( 𝑀 + 1 ) + 1 ) → ( ( 1 ... ( 𝑀 + 1 ) ) ∩ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
191 189 190 syl ⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 + 1 ) ) ∩ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
192 191 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑀 + 1 ) ) ∩ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
193 186 192 eqtr3d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
194 193 98 eqtrdi ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
195 fnun ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∧ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) ∧ ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∪ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) )
196 184 194 195 sylancr ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∪ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) )
197 fzsplit ⊢ ( ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑀 + 1 ) ) ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) )
198 24 197 syl ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑀 + 1 ) ) ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) )
199 198 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 𝑈 “ ( ( 1 ... ( 𝑀 + 1 ) ) ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) )
200 imaundi ⊢ ( 𝑈 “ ( ( 1 ... ( 𝑀 + 1 ) ) ∪ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∪ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) )
201 199 200 eqtrdi ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∪ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) )
202 201 129 eqtr3d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∪ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
203 202 fneq2d ⊢ ( 𝜑 → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∪ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) ↔ ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) ) )
204 196 203 mpbid ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
205 204 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
206 194 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
207 fzss1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑀 ... ( 𝑀 + 1 ) ) ⊆ ( 1 ... ( 𝑀 + 1 ) ) )
208 imass2 ⊢ ( ( 𝑀 ... ( 𝑀 + 1 ) ) ⊆ ( 1 ... ( 𝑀 + 1 ) ) → ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ⊆ ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) )
209 104 207 208 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ⊆ ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) )
210 209 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) )
211 fvun1 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∧ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ∧ ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ‘ 𝑛 ) )
212 181 183 211 mp3an12 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ‘ 𝑛 ) )
213 206 210 212 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ‘ 𝑛 ) )
214 84 fvconst2 ⊢ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ‘ 𝑛 ) = 1 )
215 210 214 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ‘ 𝑛 ) = 1 )
216 213 215 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
217 216 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
218 83 205 134 134 135 136 217 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 1 ) )
219 30 218 mpdan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑀 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑀 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 1 ) )
220 179 219 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 1 ) )
221 35 154 220 3netr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) )
222 221 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) )
223 fzpr ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 + 1 ) ) = { 𝑀 , ( 𝑀 + 1 ) } )
224 5 39 223 3syl ⊢ ( 𝜑 → ( 𝑀 ... ( 𝑀 + 1 ) ) = { 𝑀 , ( 𝑀 + 1 ) } )
225 224 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) = ( 𝑈 “ { 𝑀 , ( 𝑀 + 1 ) } ) )
226 f1ofn ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 Fn ( 1 ... 𝑁 ) )
227 4 226 syl ⊢ ( 𝜑 → 𝑈 Fn ( 1 ... 𝑁 ) )
228 fnimapr ⊢ ( ( 𝑈 Fn ( 1 ... 𝑁 ) ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑈 “ { 𝑀 , ( 𝑀 + 1 ) } ) = { ( 𝑈 ‘ 𝑀 ) , ( 𝑈 ‘ ( 𝑀 + 1 ) ) } )
229 227 19 24 228 syl3anc ⊢ ( 𝜑 → ( 𝑈 “ { 𝑀 , ( 𝑀 + 1 ) } ) = { ( 𝑈 ‘ 𝑀 ) , ( 𝑈 ‘ ( 𝑀 + 1 ) ) } )
230 225 229 eqtrd ⊢ ( 𝜑 → ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) = { ( 𝑈 ‘ 𝑀 ) , ( 𝑈 ‘ ( 𝑀 + 1 ) ) } )
231 230 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ( 𝑈 “ ( 𝑀 ... ( 𝑀 + 1 ) ) ) ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ { ( 𝑈 ‘ 𝑀 ) , ( 𝑈 ‘ ( 𝑀 + 1 ) ) } ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ) )
232 222 231 mpbid ⊢ ( 𝜑 → ∀ 𝑛 ∈ { ( 𝑈 ‘ 𝑀 ) , ( 𝑈 ‘ ( 𝑀 + 1 ) ) } ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) )
233 fvex ⊢ ( 𝑈 ‘ 𝑀 ) ∈ V
234 fvex ⊢ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ∈ V
235 fveq2 ⊢ ( 𝑛 = ( 𝑈 ‘ 𝑀 ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) )
236 fveq2 ⊢ ( 𝑛 = ( 𝑈 ‘ 𝑀 ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) )
237 235 236 neeq12d ⊢ ( 𝑛 = ( 𝑈 ‘ 𝑀 ) → ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ↔ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) ) )
238 fveq2 ⊢ ( 𝑛 = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) )
239 fveq2 ⊢ ( 𝑛 = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) )
240 238 239 neeq12d ⊢ ( 𝑛 = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ↔ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ) )
241 233 234 237 240 ralpr ⊢ ( ∀ 𝑛 ∈ { ( 𝑈 ‘ 𝑀 ) , ( 𝑈 ‘ ( 𝑀 + 1 ) ) } ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ↔ ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ) )
242 232 241 sylib ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ) )
243 41 ltp1d ⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
244 41 243 ltned ⊢ ( 𝜑 → 𝑀 ≠ ( 𝑀 + 1 ) )
245 f1of1 ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
246 4 245 syl ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) )
247 f1veqaeq ⊢ ( ( 𝑈 : ( 1 ... 𝑁 ) –1-1→ ( 1 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) ) ) → ( ( 𝑈 ‘ 𝑀 ) = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → 𝑀 = ( 𝑀 + 1 ) ) )
248 246 19 24 247 syl12anc ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑀 ) = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → 𝑀 = ( 𝑀 + 1 ) ) )
249 248 necon3d ⊢ ( 𝜑 → ( 𝑀 ≠ ( 𝑀 + 1 ) → ( 𝑈 ‘ 𝑀 ) ≠ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) )
250 244 249 mpd ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑀 ) ≠ ( 𝑈 ‘ ( 𝑀 + 1 ) ) )
251 237 anbi1d ⊢ ( 𝑛 = ( 𝑈 ‘ 𝑀 ) → ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ↔ ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ) )
252 neeq1 ⊢ ( 𝑛 = ( 𝑈 ‘ 𝑀 ) → ( 𝑛 ≠ 𝑚 ↔ ( 𝑈 ‘ 𝑀 ) ≠ 𝑚 ) )
253 251 252 anbi12d ⊢ ( 𝑛 = ( 𝑈 ‘ 𝑀 ) → ( ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) ↔ ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ ( 𝑈 ‘ 𝑀 ) ≠ 𝑚 ) ) )
254 fveq2 ⊢ ( 𝑚 = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) )
255 fveq2 ⊢ ( 𝑚 = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) )
256 254 255 neeq12d ⊢ ( 𝑚 = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ↔ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ) )
257 256 anbi2d ⊢ ( 𝑚 = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ↔ ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ) ) )
258 neeq2 ⊢ ( 𝑚 = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → ( ( 𝑈 ‘ 𝑀 ) ≠ 𝑚 ↔ ( 𝑈 ‘ 𝑀 ) ≠ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) )
259 257 258 anbi12d ⊢ ( 𝑚 = ( 𝑈 ‘ ( 𝑀 + 1 ) ) → ( ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ ( 𝑈 ‘ 𝑀 ) ≠ 𝑚 ) ↔ ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑈 ‘ 𝑀 ) ≠ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ) )
260 253 259 rspc2ev ⊢ ( ( ( 𝑈 ‘ 𝑀 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ∈ ( 1 ... 𝑁 ) ∧ ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ 𝑀 ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ 𝑀 ) ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ) ∧ ( 𝑈 ‘ 𝑀 ) ≠ ( 𝑈 ‘ ( 𝑀 + 1 ) ) ) ) → ∃ 𝑛 ∈ ( 1 ... 𝑁 ) ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) )
261 20 25 242 250 260 syl112anc ⊢ ( 𝜑 → ∃ 𝑛 ∈ ( 1 ... 𝑁 ) ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) )
262 dfrex2 ⊢ ( ∃ 𝑛 ∈ ( 1 ... 𝑁 ) ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) ↔ ¬ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ¬ ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) )
263 fveq2 ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) )
264 fveq2 ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) )
265 263 264 neeq12d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ↔ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) )
266 265 rmo4 ⊢ ( ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) → 𝑛 = 𝑚 ) )
267 dfral2 ⊢ ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) → 𝑛 = 𝑚 ) ↔ ¬ ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ¬ ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) → 𝑛 = 𝑚 ) )
268 df-ne ⊢ ( 𝑛 ≠ 𝑚 ↔ ¬ 𝑛 = 𝑚 )
269 268 anbi2i ⊢ ( ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) ↔ ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ ¬ 𝑛 = 𝑚 ) )
270 annim ⊢ ( ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ ¬ 𝑛 = 𝑚 ) ↔ ¬ ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) → 𝑛 = 𝑚 ) )
271 269 270 bitri ⊢ ( ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) ↔ ¬ ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) → 𝑛 = 𝑚 ) )
272 271 rexbii ⊢ ( ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) ↔ ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ¬ ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) → 𝑛 = 𝑚 ) )
273 267 272 xchbinxr ⊢ ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) → 𝑛 = 𝑚 ) ↔ ¬ ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) )
274 273 ralbii ⊢ ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) → 𝑛 = 𝑚 ) ↔ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ¬ ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) )
275 266 274 bitri ⊢ ( ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ¬ ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) )
276 262 275 xchbinxr ⊢ ( ∃ 𝑛 ∈ ( 1 ... 𝑁 ) ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) ∧ ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑚 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑚 ) ) ∧ 𝑛 ≠ 𝑚 ) ↔ ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) )
277 261 276 sylib ⊢ ( 𝜑 → ¬ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑀 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑀 ) ‘ 𝑛 ) )