Metamath Proof Explorer

Theorem poimirlem2

Description: Lemma for poimir - consecutive vertices differ in at most one dimension. (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 ... 𝑁 ) )
poimirlem2.4 ⊢ ( 𝜑 → 𝑉 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
poimirlem2.5 ⊢ ( 𝜑 → 𝑀 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) )
Assertion poimirlem2 ( 𝜑 → ∃* 𝑛 ∈ ( 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 poimirlem2.4 ⊢ ( 𝜑 → 𝑉 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
6 poimirlem2.5 ⊢ ( 𝜑 → 𝑀 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) )
7 dff1o3 ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ◡ 𝑈 ) )
8 7 simprbi ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ◡ 𝑈 )
9 4 8 syl ⊢ ( 𝜑 → Fun ◡ 𝑈 )
10 imadif ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { ( 𝑉 + 1 ) } ) ) = ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) )
11 9 10 syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { ( 𝑉 + 1 ) } ) ) = ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) )
12 fzp1elp1 ⊢ ( 𝑉 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑉 + 1 ) ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
13 5 12 syl ⊢ ( 𝜑 → ( 𝑉 + 1 ) ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
14 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
15 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
16 14 15 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
17 16 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
18 13 17 eleqtrd ⊢ ( 𝜑 → ( 𝑉 + 1 ) ∈ ( 1 ... 𝑁 ) )
19 fzsplit ⊢ ( ( 𝑉 + 1 ) ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑉 + 1 ) ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) )
20 18 19 syl ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑉 + 1 ) ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) )
21 20 difeq1d ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { ( 𝑉 + 1 ) } ) = ( ( ( 1 ... ( 𝑉 + 1 ) ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ∖ { ( 𝑉 + 1 ) } ) )
22 difundir ⊢ ( ( ( 1 ... ( 𝑉 + 1 ) ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ∖ { ( 𝑉 + 1 ) } ) = ( ( ( 1 ... ( 𝑉 + 1 ) ) ∖ { ( 𝑉 + 1 ) } ) ∪ ( ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 𝑉 + 1 ) } ) )
23 elfzuz ⊢ ( 𝑉 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑉 ∈ ( ℤ≥ ‘ 1 ) )
24 5 23 syl ⊢ ( 𝜑 → 𝑉 ∈ ( ℤ≥ ‘ 1 ) )
25 fzsuc ⊢ ( 𝑉 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... ( 𝑉 + 1 ) ) = ( ( 1 ... 𝑉 ) ∪ { ( 𝑉 + 1 ) } ) )
26 24 25 syl ⊢ ( 𝜑 → ( 1 ... ( 𝑉 + 1 ) ) = ( ( 1 ... 𝑉 ) ∪ { ( 𝑉 + 1 ) } ) )
27 26 difeq1d ⊢ ( 𝜑 → ( ( 1 ... ( 𝑉 + 1 ) ) ∖ { ( 𝑉 + 1 ) } ) = ( ( ( 1 ... 𝑉 ) ∪ { ( 𝑉 + 1 ) } ) ∖ { ( 𝑉 + 1 ) } ) )
28 difun2 ⊢ ( ( ( 1 ... 𝑉 ) ∪ { ( 𝑉 + 1 ) } ) ∖ { ( 𝑉 + 1 ) } ) = ( ( 1 ... 𝑉 ) ∖ { ( 𝑉 + 1 ) } )
29 5 elfzelzd ⊢ ( 𝜑 → 𝑉 ∈ ℤ )
30 29 zred ⊢ ( 𝜑 → 𝑉 ∈ ℝ )
31 30 ltp1d ⊢ ( 𝜑 → 𝑉 < ( 𝑉 + 1 ) )
32 29 peano2zd ⊢ ( 𝜑 → ( 𝑉 + 1 ) ∈ ℤ )
33 32 zred ⊢ ( 𝜑 → ( 𝑉 + 1 ) ∈ ℝ )
34 30 33 ltnled ⊢ ( 𝜑 → ( 𝑉 < ( 𝑉 + 1 ) ↔ ¬ ( 𝑉 + 1 ) ≤ 𝑉 ) )
35 31 34 mpbid ⊢ ( 𝜑 → ¬ ( 𝑉 + 1 ) ≤ 𝑉 )
36 elfzle2 ⊢ ( ( 𝑉 + 1 ) ∈ ( 1 ... 𝑉 ) → ( 𝑉 + 1 ) ≤ 𝑉 )
37 35 36 nsyl ⊢ ( 𝜑 → ¬ ( 𝑉 + 1 ) ∈ ( 1 ... 𝑉 ) )
38 difsn ⊢ ( ¬ ( 𝑉 + 1 ) ∈ ( 1 ... 𝑉 ) → ( ( 1 ... 𝑉 ) ∖ { ( 𝑉 + 1 ) } ) = ( 1 ... 𝑉 ) )
39 37 38 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑉 ) ∖ { ( 𝑉 + 1 ) } ) = ( 1 ... 𝑉 ) )
40 28 39 eqtrid ⊢ ( 𝜑 → ( ( ( 1 ... 𝑉 ) ∪ { ( 𝑉 + 1 ) } ) ∖ { ( 𝑉 + 1 ) } ) = ( 1 ... 𝑉 ) )
41 27 40 eqtrd ⊢ ( 𝜑 → ( ( 1 ... ( 𝑉 + 1 ) ) ∖ { ( 𝑉 + 1 ) } ) = ( 1 ... 𝑉 ) )
42 33 ltp1d ⊢ ( 𝜑 → ( 𝑉 + 1 ) < ( ( 𝑉 + 1 ) + 1 ) )
43 peano2re ⊢ ( ( 𝑉 + 1 ) ∈ ℝ → ( ( 𝑉 + 1 ) + 1 ) ∈ ℝ )
44 33 43 syl ⊢ ( 𝜑 → ( ( 𝑉 + 1 ) + 1 ) ∈ ℝ )
45 33 44 ltnled ⊢ ( 𝜑 → ( ( 𝑉 + 1 ) < ( ( 𝑉 + 1 ) + 1 ) ↔ ¬ ( ( 𝑉 + 1 ) + 1 ) ≤ ( 𝑉 + 1 ) ) )
46 42 45 mpbid ⊢ ( 𝜑 → ¬ ( ( 𝑉 + 1 ) + 1 ) ≤ ( 𝑉 + 1 ) )
47 elfzle1 ⊢ ( ( 𝑉 + 1 ) ∈ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) → ( ( 𝑉 + 1 ) + 1 ) ≤ ( 𝑉 + 1 ) )
48 46 47 nsyl ⊢ ( 𝜑 → ¬ ( 𝑉 + 1 ) ∈ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) )
49 difsn ⊢ ( ¬ ( 𝑉 + 1 ) ∈ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) → ( ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 𝑉 + 1 ) } ) = ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) )
50 48 49 syl ⊢ ( 𝜑 → ( ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 𝑉 + 1 ) } ) = ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) )
51 41 50 uneq12d ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝑉 + 1 ) ) ∖ { ( 𝑉 + 1 ) } ) ∪ ( ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ∖ { ( 𝑉 + 1 ) } ) ) = ( ( 1 ... 𝑉 ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) )
52 22 51 eqtrid ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝑉 + 1 ) ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ∖ { ( 𝑉 + 1 ) } ) = ( ( 1 ... 𝑉 ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) )
53 21 52 eqtrd ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { ( 𝑉 + 1 ) } ) = ( ( 1 ... 𝑉 ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) )
54 53 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { ( 𝑉 + 1 ) } ) ) = ( 𝑈 “ ( ( 1 ... 𝑉 ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) )
55 11 54 eqtr3d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) = ( 𝑈 “ ( ( 1 ... 𝑉 ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) )
56 imaundi ⊢ ( 𝑈 “ ( ( 1 ... 𝑉 ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∪ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) )
57 55 56 eqtrdi ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) = ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∪ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) )
58 57 eleq2d ⊢ ( 𝜑 → ( 𝑛 ∈ ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) ↔ 𝑛 ∈ ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∪ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ) )
59 eldif ⊢ ( 𝑛 ∈ ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) ↔ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑛 ∈ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) )
60 elun ⊢ ( 𝑛 ∈ ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∪ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ↔ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) )
61 58 59 60 3bitr3g ⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑛 ∈ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) ↔ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ) )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ( ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑛 ∈ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) ↔ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ) )
63 imassrn ⊢ ( 𝑈 “ ( 1 ... 𝑉 ) ) ⊆ ran 𝑈
64 f1of ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
65 4 64 syl ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑁 ) )
66 65 frnd ⊢ ( 𝜑 → ran 𝑈 ⊆ ( 1 ... 𝑁 ) )
67 63 66 sstrid ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑉 ) ) ⊆ ( 1 ... 𝑁 ) )
68 67 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
69 3 ffnd ⊢ ( 𝜑 → 𝑇 Fn ( 1 ... 𝑁 ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → 𝑇 Fn ( 1 ... 𝑁 ) )
71 1ex ⊢ 1 ∈ V
72 fnconstg ⊢ ( 1 ∈ V → ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑉 ) ) )
73 71 72 ax-mp ⊢ ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑉 ) )
74 c0ex ⊢ 0 ∈ V
75 fnconstg ⊢ ( 0 ∈ V → ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
76 74 75 ax-mp ⊢ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) )
77 73 76 pm3.2i ⊢ ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑉 ) ) ∧ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
78 imain ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... 𝑉 ) ∩ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∩ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) )
79 9 78 syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑉 ) ∩ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∩ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) )
80 fzdisj ⊢ ( 𝑉 < ( 𝑉 + 1 ) → ( ( 1 ... 𝑉 ) ∩ ( ( 𝑉 + 1 ) ... 𝑁 ) ) = ∅ )
81 31 80 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑉 ) ∩ ( ( 𝑉 + 1 ) ... 𝑁 ) ) = ∅ )
82 81 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑉 ) ∩ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
83 ima0 ⊢ ( 𝑈 “ ∅ ) = ∅
84 82 83 eqtrdi ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑉 ) ∩ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ∅ )
85 79 84 eqtr3d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∩ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ∅ )
86 fnun ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑉 ) ) ∧ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ∧ ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∩ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∪ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) )
87 77 85 86 sylancr ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∪ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) )
88 imaundi ⊢ ( 𝑈 “ ( ( 1 ... 𝑉 ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∪ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
89 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
90 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
91 uzid ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
92 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
93 89 90 91 92 4syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
94 16 93 eqeltrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
95 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
96 94 95 syl ⊢ ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
97 96 5 sseldd ⊢ ( 𝜑 → 𝑉 ∈ ( 1 ... 𝑁 ) )
98 fzsplit ⊢ ( 𝑉 ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑉 ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
99 97 98 syl ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑉 ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
100 99 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 𝑈 “ ( ( 1 ... 𝑉 ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) )
101 f1ofo ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
102 4 101 syl ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
103 foima ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
104 102 103 syl ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
105 100 104 eqtr3d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑉 ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
106 88 105 eqtr3id ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∪ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
107 106 fneq2d ⊢ ( 𝜑 → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∪ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ↔ ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) ) )
108 87 107 mpbid ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
109 108 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
110 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
111 inidm ⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
112 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
113 fvun1 ⊢ ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑉 ) ) ∧ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ∧ ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∩ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ‘ 𝑛 ) )
114 73 76 113 mp3an12 ⊢ ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∩ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ‘ 𝑛 ) )
115 85 114 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ‘ 𝑛 ) )
116 71 fvconst2 ⊢ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ‘ 𝑛 ) = 1 )
117 116 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ‘ 𝑛 ) = 1 )
118 115 117 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
119 118 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
120 70 109 110 110 111 112 119 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 1 ) )
121 fnconstg ⊢ ( 1 ∈ V → ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) )
122 71 121 ax-mp ⊢ ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) )
123 fnconstg ⊢ ( 0 ∈ V → ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) )
124 74 123 ax-mp ⊢ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) )
125 122 124 pm3.2i ⊢ ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ∧ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) )
126 imain ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... ( 𝑉 + 1 ) ) ∩ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) )
127 9 126 syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑉 + 1 ) ) ∩ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) )
128 fzdisj ⊢ ( ( 𝑉 + 1 ) < ( ( 𝑉 + 1 ) + 1 ) → ( ( 1 ... ( 𝑉 + 1 ) ) ∩ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
129 42 128 syl ⊢ ( 𝜑 → ( ( 1 ... ( 𝑉 + 1 ) ) ∩ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
130 129 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑉 + 1 ) ) ∩ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
131 130 83 eqtrdi ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑉 + 1 ) ) ∩ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
132 127 131 eqtr3d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
133 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 ) ... 𝑁 ) ) ) )
134 125 132 133 sylancr ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ∪ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) )
135 imaundi ⊢ ( 𝑈 “ ( ( 1 ... ( 𝑉 + 1 ) ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ∪ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) )
136 20 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 𝑈 “ ( ( 1 ... ( 𝑉 + 1 ) ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) )
137 136 104 eqtr3d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑉 + 1 ) ) ∪ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
138 135 137 eqtr3id ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ∪ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
139 138 fneq2d ⊢ ( 𝜑 → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ∪ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ↔ ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) ) )
140 134 139 mpbid ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
141 140 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
142 uzid ⊢ ( 𝑉 ∈ ℤ → 𝑉 ∈ ( ℤ≥ ‘ 𝑉 ) )
143 29 142 syl ⊢ ( 𝜑 → 𝑉 ∈ ( ℤ≥ ‘ 𝑉 ) )
144 peano2uz ⊢ ( 𝑉 ∈ ( ℤ≥ ‘ 𝑉 ) → ( 𝑉 + 1 ) ∈ ( ℤ≥ ‘ 𝑉 ) )
145 fzss2 ⊢ ( ( 𝑉 + 1 ) ∈ ( ℤ≥ ‘ 𝑉 ) → ( 1 ... 𝑉 ) ⊆ ( 1 ... ( 𝑉 + 1 ) ) )
146 imass2 ⊢ ( ( 1 ... 𝑉 ) ⊆ ( 1 ... ( 𝑉 + 1 ) ) → ( 𝑈 “ ( 1 ... 𝑉 ) ) ⊆ ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) )
147 143 144 145 146 4syl ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑉 ) ) ⊆ ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) )
148 147 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) )
149 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 } ) ‘ 𝑛 ) )
150 122 124 149 mp3an12 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ‘ 𝑛 ) )
151 132 150 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ‘ 𝑛 ) )
152 71 fvconst2 ⊢ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ‘ 𝑛 ) = 1 )
153 152 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ‘ 𝑛 ) = 1 )
154 151 153 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
155 148 154 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
156 155 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
157 70 141 110 110 111 112 156 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 1 ) )
158 120 157 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
159 68 158 mpdan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
160 imassrn ⊢ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ⊆ ran 𝑈
161 160 66 sstrid ⊢ ( 𝜑 → ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ⊆ ( 1 ... 𝑁 ) )
162 161 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
163 69 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → 𝑇 Fn ( 1 ... 𝑁 ) )
164 108 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
165 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
166 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
167 uzid ⊢ ( ( 𝑉 + 1 ) ∈ ℤ → ( 𝑉 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 + 1 ) ) )
168 32 167 syl ⊢ ( 𝜑 → ( 𝑉 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 + 1 ) ) )
169 peano2uz ⊢ ( ( 𝑉 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 + 1 ) ) → ( ( 𝑉 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 + 1 ) ) )
170 fzss1 ⊢ ( ( ( 𝑉 + 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 + 1 ) ) → ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 𝑉 + 1 ) ... 𝑁 ) )
171 imass2 ⊢ ( ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ⊆ ( ( 𝑉 + 1 ) ... 𝑁 ) → ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ⊆ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
172 168 169 170 171 4syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ⊆ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
173 172 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
174 fvun2 ⊢ ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑉 ) ) ∧ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ∧ ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∩ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
175 73 76 174 mp3an12 ⊢ ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) ∩ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
176 85 175 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
177 74 fvconst2 ⊢ ( 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) → ( ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) = 0 )
178 177 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → ( ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) = 0 )
179 176 178 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
180 173 179 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
181 180 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
182 163 164 165 165 111 166 181 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 0 ) )
183 140 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
184 fvun2 ⊢ ( ( ( ( 𝑈 “ ( 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 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
185 122 124 184 mp3an12 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
186 132 185 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
187 74 fvconst2 ⊢ ( 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) → ( ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) = 0 )
188 187 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → ( ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) = 0 )
189 186 188 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
190 189 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
191 163 183 165 165 111 166 190 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 0 ) )
192 182 191 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
193 162 192 mpdan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
194 159 193 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
195 194 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
196 2 adantr ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
197 vex ⊢ 𝑦 ∈ V
198 ovex ⊢ ( 𝑦 + 1 ) ∈ V
199 197 198 ifex ⊢ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ∈ V
200 199 a1i ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ∈ V )
201 breq1 ⊢ ( 𝑦 = ( 𝑉 − 1 ) → ( 𝑦 < 𝑀 ↔ ( 𝑉 − 1 ) < 𝑀 ) )
202 201 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑉 − 1 ) ) → ( 𝑦 < 𝑀 ↔ ( 𝑉 − 1 ) < 𝑀 ) )
203 simpr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑉 − 1 ) ) → 𝑦 = ( 𝑉 − 1 ) )
204 oveq1 ⊢ ( 𝑦 = ( 𝑉 − 1 ) → ( 𝑦 + 1 ) = ( ( 𝑉 − 1 ) + 1 ) )
205 29 zcnd ⊢ ( 𝜑 → 𝑉 ∈ ℂ )
206 npcan1 ⊢ ( 𝑉 ∈ ℂ → ( ( 𝑉 − 1 ) + 1 ) = 𝑉 )
207 205 206 syl ⊢ ( 𝜑 → ( ( 𝑉 − 1 ) + 1 ) = 𝑉 )
208 204 207 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑉 − 1 ) ) → ( 𝑦 + 1 ) = 𝑉 )
209 202 203 208 ifbieq12d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑉 − 1 ) ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = if ( ( 𝑉 − 1 ) < 𝑀 , ( 𝑉 − 1 ) , 𝑉 ) )
210 209 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = if ( ( 𝑉 − 1 ) < 𝑀 , ( 𝑉 − 1 ) , 𝑉 ) )
211 6 eldifad ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑁 ) )
212 211 elfzelzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
213 zltlem1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑉 ∈ ℤ ) → ( 𝑀 < 𝑉 ↔ 𝑀 ≤ ( 𝑉 − 1 ) ) )
214 212 29 213 syl2anc ⊢ ( 𝜑 → ( 𝑀 < 𝑉 ↔ 𝑀 ≤ ( 𝑉 − 1 ) ) )
215 212 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
216 peano2zm ⊢ ( 𝑉 ∈ ℤ → ( 𝑉 − 1 ) ∈ ℤ )
217 29 216 syl ⊢ ( 𝜑 → ( 𝑉 − 1 ) ∈ ℤ )
218 217 zred ⊢ ( 𝜑 → ( 𝑉 − 1 ) ∈ ℝ )
219 215 218 lenltd ⊢ ( 𝜑 → ( 𝑀 ≤ ( 𝑉 − 1 ) ↔ ¬ ( 𝑉 − 1 ) < 𝑀 ) )
220 214 219 bitrd ⊢ ( 𝜑 → ( 𝑀 < 𝑉 ↔ ¬ ( 𝑉 − 1 ) < 𝑀 ) )
221 220 biimpa ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ¬ ( 𝑉 − 1 ) < 𝑀 )
222 221 iffalsed ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → if ( ( 𝑉 − 1 ) < 𝑀 , ( 𝑉 − 1 ) , 𝑉 ) = 𝑉 )
223 222 adantr ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → if ( ( 𝑉 − 1 ) < 𝑀 , ( 𝑉 − 1 ) , 𝑉 ) = 𝑉 )
224 210 223 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = 𝑉 )
225 224 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → ( 𝑗 = if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ↔ 𝑗 = 𝑉 ) )
226 225 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) ∧ 𝑗 = if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ) → 𝑗 = 𝑉 )
227 oveq2 ⊢ ( 𝑗 = 𝑉 → ( 1 ... 𝑗 ) = ( 1 ... 𝑉 ) )
228 227 imaeq2d ⊢ ( 𝑗 = 𝑉 → ( 𝑈 “ ( 1 ... 𝑗 ) ) = ( 𝑈 “ ( 1 ... 𝑉 ) ) )
229 228 xpeq1d ⊢ ( 𝑗 = 𝑉 → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) )
230 oveq1 ⊢ ( 𝑗 = 𝑉 → ( 𝑗 + 1 ) = ( 𝑉 + 1 ) )
231 230 oveq1d ⊢ ( 𝑗 = 𝑉 → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( 𝑉 + 1 ) ... 𝑁 ) )
232 231 imaeq2d ⊢ ( 𝑗 = 𝑉 → ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
233 232 xpeq1d ⊢ ( 𝑗 = 𝑉 → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) )
234 229 233 uneq12d ⊢ ( 𝑗 = 𝑉 → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
235 234 oveq2d ⊢ ( 𝑗 = 𝑉 → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
236 226 235 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) ∧ 𝑗 = if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
237 200 236 csbied ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
238 elfzm1b ⊢ ( ( 𝑉 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑉 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑉 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
239 29 89 238 syl2anc ⊢ ( 𝜑 → ( 𝑉 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑉 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
240 97 239 mpbid ⊢ ( 𝜑 → ( 𝑉 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
241 240 adantr ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ( 𝑉 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
242 ovexd ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V )
243 196 237 241 242 fvmptd ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ( 𝐹 ‘ ( 𝑉 − 1 ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
244 243 fveq1d ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
245 244 adantr ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
246 199 a1i ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = 𝑉 ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ∈ V )
247 breq1 ⊢ ( 𝑦 = 𝑉 → ( 𝑦 < 𝑀 ↔ 𝑉 < 𝑀 ) )
248 id ⊢ ( 𝑦 = 𝑉 → 𝑦 = 𝑉 )
249 oveq1 ⊢ ( 𝑦 = 𝑉 → ( 𝑦 + 1 ) = ( 𝑉 + 1 ) )
250 247 248 249 ifbieq12d ⊢ ( 𝑦 = 𝑉 → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑉 < 𝑀 , 𝑉 , ( 𝑉 + 1 ) ) )
251 ltnsym ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑉 ∈ ℝ ) → ( 𝑀 < 𝑉 → ¬ 𝑉 < 𝑀 ) )
252 215 30 251 syl2anc ⊢ ( 𝜑 → ( 𝑀 < 𝑉 → ¬ 𝑉 < 𝑀 ) )
253 252 imp ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ¬ 𝑉 < 𝑀 )
254 253 iffalsed ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → if ( 𝑉 < 𝑀 , 𝑉 , ( 𝑉 + 1 ) ) = ( 𝑉 + 1 ) )
255 250 254 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = 𝑉 ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑉 + 1 ) )
256 255 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = 𝑉 ) → ( 𝑗 = if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ↔ 𝑗 = ( 𝑉 + 1 ) ) )
257 256 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = 𝑉 ) ∧ 𝑗 = if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ) → 𝑗 = ( 𝑉 + 1 ) )
258 oveq2 ⊢ ( 𝑗 = ( 𝑉 + 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑉 + 1 ) ) )
259 258 imaeq2d ⊢ ( 𝑗 = ( 𝑉 + 1 ) → ( 𝑈 “ ( 1 ... 𝑗 ) ) = ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) )
260 259 xpeq1d ⊢ ( 𝑗 = ( 𝑉 + 1 ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) )
261 oveq1 ⊢ ( 𝑗 = ( 𝑉 + 1 ) → ( 𝑗 + 1 ) = ( ( 𝑉 + 1 ) + 1 ) )
262 261 oveq1d ⊢ ( 𝑗 = ( 𝑉 + 1 ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) )
263 262 imaeq2d ⊢ ( 𝑗 = ( 𝑉 + 1 ) → ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) )
264 263 xpeq1d ⊢ ( 𝑗 = ( 𝑉 + 1 ) → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
265 260 264 uneq12d ⊢ ( 𝑗 = ( 𝑉 + 1 ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
266 265 oveq2d ⊢ ( 𝑗 = ( 𝑉 + 1 ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
267 257 266 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = 𝑉 ) ∧ 𝑗 = if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
268 246 267 csbied ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑦 = 𝑉 ) → ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
269 fz1ssfz0 ⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( 𝑁 − 1 ) )
270 269 5 sselid ⊢ ( 𝜑 → 𝑉 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
271 270 adantr ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → 𝑉 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
272 ovexd ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V )
273 196 268 271 272 fvmptd ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ( 𝐹 ‘ 𝑉 ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
274 273 fveq1d ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
275 274 adantr ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ) → ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 + 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
276 195 245 275 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) )
277 276 ex ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ( ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( ( 𝑉 + 1 ) + 1 ) ... 𝑁 ) ) ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ) )
278 62 277 sylbid ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ( ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑛 ∈ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ) )
279 278 expdimp ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ) → ( ¬ 𝑛 ∈ ( 𝑈 “ { ( 𝑉 + 1 ) } ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ) )
280 279 necon1ad ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 ∈ ( 𝑈 “ { ( 𝑉 + 1 ) } ) ) )
281 elimasni ⊢ ( 𝑛 ∈ ( 𝑈 “ { ( 𝑉 + 1 ) } ) → ( 𝑉 + 1 ) 𝑈 𝑛 )
282 eqcom ⊢ ( 𝑛 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) ↔ ( 𝑈 ‘ ( 𝑉 + 1 ) ) = 𝑛 )
283 f1ofn ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 Fn ( 1 ... 𝑁 ) )
284 4 283 syl ⊢ ( 𝜑 → 𝑈 Fn ( 1 ... 𝑁 ) )
285 fnbrfvb ⊢ ( ( 𝑈 Fn ( 1 ... 𝑁 ) ∧ ( 𝑉 + 1 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑈 ‘ ( 𝑉 + 1 ) ) = 𝑛 ↔ ( 𝑉 + 1 ) 𝑈 𝑛 ) )
286 284 18 285 syl2anc ⊢ ( 𝜑 → ( ( 𝑈 ‘ ( 𝑉 + 1 ) ) = 𝑛 ↔ ( 𝑉 + 1 ) 𝑈 𝑛 ) )
287 282 286 bitrid ⊢ ( 𝜑 → ( 𝑛 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) ↔ ( 𝑉 + 1 ) 𝑈 𝑛 ) )
288 281 287 imbitrrid ⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝑈 “ { ( 𝑉 + 1 ) } ) → 𝑛 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) ) )
289 288 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ) → ( 𝑛 ∈ ( 𝑈 “ { ( 𝑉 + 1 ) } ) → 𝑛 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) ) )
290 280 289 syld ⊢ ( ( ( 𝜑 ∧ 𝑀 < 𝑉 ) ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) ) )
291 290 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) ) )
292 fvex ⊢ ( 𝑈 ‘ ( 𝑉 + 1 ) ) ∈ V
293 eqeq2 ⊢ ( 𝑚 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) → ( 𝑛 = 𝑚 ↔ 𝑛 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) ) )
294 293 imbi2d ⊢ ( 𝑚 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) → ( ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) ↔ ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) ) ) )
295 294 ralbidv ⊢ ( 𝑚 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) → ( ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) ↔ ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) ) ) )
296 292 295 spcev ⊢ ( ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = ( 𝑈 ‘ ( 𝑉 + 1 ) ) ) → ∃ 𝑚 ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) )
297 291 296 syl ⊢ ( ( 𝜑 ∧ 𝑀 < 𝑉 ) → ∃ 𝑚 ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) )
298 imadif ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { 𝑉 } ) ) = ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑉 } ) ) )
299 9 298 syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { 𝑉 } ) ) = ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑉 } ) ) )
300 99 difeq1d ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { 𝑉 } ) = ( ( ( 1 ... 𝑉 ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ∖ { 𝑉 } ) )
301 difundir ⊢ ( ( ( 1 ... 𝑉 ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ∖ { 𝑉 } ) = ( ( ( 1 ... 𝑉 ) ∖ { 𝑉 } ) ∪ ( ( ( 𝑉 + 1 ) ... 𝑁 ) ∖ { 𝑉 } ) )
302 207 24 eqeltrd ⊢ ( 𝜑 → ( ( 𝑉 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
303 uzid ⊢ ( ( 𝑉 − 1 ) ∈ ℤ → ( 𝑉 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) )
304 peano2uz ⊢ ( ( 𝑉 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) → ( ( 𝑉 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) )
305 29 216 303 304 4syl ⊢ ( 𝜑 → ( ( 𝑉 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) )
306 207 305 eqeltrrd ⊢ ( 𝜑 → 𝑉 ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) )
307 fzsplit2 ⊢ ( ( ( ( 𝑉 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑉 ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) ) → ( 1 ... 𝑉 ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( ( 𝑉 − 1 ) + 1 ) ... 𝑉 ) ) )
308 302 306 307 syl2anc ⊢ ( 𝜑 → ( 1 ... 𝑉 ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( ( 𝑉 − 1 ) + 1 ) ... 𝑉 ) ) )
309 207 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑉 − 1 ) + 1 ) ... 𝑉 ) = ( 𝑉 ... 𝑉 ) )
310 fzsn ⊢ ( 𝑉 ∈ ℤ → ( 𝑉 ... 𝑉 ) = { 𝑉 } )
311 29 310 syl ⊢ ( 𝜑 → ( 𝑉 ... 𝑉 ) = { 𝑉 } )
312 309 311 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑉 − 1 ) + 1 ) ... 𝑉 ) = { 𝑉 } )
313 312 uneq2d ⊢ ( 𝜑 → ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( ( 𝑉 − 1 ) + 1 ) ... 𝑉 ) ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ { 𝑉 } ) )
314 308 313 eqtrd ⊢ ( 𝜑 → ( 1 ... 𝑉 ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ { 𝑉 } ) )
315 314 difeq1d ⊢ ( 𝜑 → ( ( 1 ... 𝑉 ) ∖ { 𝑉 } ) = ( ( ( 1 ... ( 𝑉 − 1 ) ) ∪ { 𝑉 } ) ∖ { 𝑉 } ) )
316 difun2 ⊢ ( ( ( 1 ... ( 𝑉 − 1 ) ) ∪ { 𝑉 } ) ∖ { 𝑉 } ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∖ { 𝑉 } )
317 30 ltm1d ⊢ ( 𝜑 → ( 𝑉 − 1 ) < 𝑉 )
318 218 30 ltnled ⊢ ( 𝜑 → ( ( 𝑉 − 1 ) < 𝑉 ↔ ¬ 𝑉 ≤ ( 𝑉 − 1 ) ) )
319 317 318 mpbid ⊢ ( 𝜑 → ¬ 𝑉 ≤ ( 𝑉 − 1 ) )
320 elfzle2 ⊢ ( 𝑉 ∈ ( 1 ... ( 𝑉 − 1 ) ) → 𝑉 ≤ ( 𝑉 − 1 ) )
321 319 320 nsyl ⊢ ( 𝜑 → ¬ 𝑉 ∈ ( 1 ... ( 𝑉 − 1 ) ) )
322 difsn ⊢ ( ¬ 𝑉 ∈ ( 1 ... ( 𝑉 − 1 ) ) → ( ( 1 ... ( 𝑉 − 1 ) ) ∖ { 𝑉 } ) = ( 1 ... ( 𝑉 − 1 ) ) )
323 321 322 syl ⊢ ( 𝜑 → ( ( 1 ... ( 𝑉 − 1 ) ) ∖ { 𝑉 } ) = ( 1 ... ( 𝑉 − 1 ) ) )
324 316 323 eqtrid ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝑉 − 1 ) ) ∪ { 𝑉 } ) ∖ { 𝑉 } ) = ( 1 ... ( 𝑉 − 1 ) ) )
325 315 324 eqtrd ⊢ ( 𝜑 → ( ( 1 ... 𝑉 ) ∖ { 𝑉 } ) = ( 1 ... ( 𝑉 − 1 ) ) )
326 elfzle1 ⊢ ( 𝑉 ∈ ( ( 𝑉 + 1 ) ... 𝑁 ) → ( 𝑉 + 1 ) ≤ 𝑉 )
327 35 326 nsyl ⊢ ( 𝜑 → ¬ 𝑉 ∈ ( ( 𝑉 + 1 ) ... 𝑁 ) )
328 difsn ⊢ ( ¬ 𝑉 ∈ ( ( 𝑉 + 1 ) ... 𝑁 ) → ( ( ( 𝑉 + 1 ) ... 𝑁 ) ∖ { 𝑉 } ) = ( ( 𝑉 + 1 ) ... 𝑁 ) )
329 327 328 syl ⊢ ( 𝜑 → ( ( ( 𝑉 + 1 ) ... 𝑁 ) ∖ { 𝑉 } ) = ( ( 𝑉 + 1 ) ... 𝑁 ) )
330 325 329 uneq12d ⊢ ( 𝜑 → ( ( ( 1 ... 𝑉 ) ∖ { 𝑉 } ) ∪ ( ( ( 𝑉 + 1 ) ... 𝑁 ) ∖ { 𝑉 } ) ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
331 301 330 eqtrid ⊢ ( 𝜑 → ( ( ( 1 ... 𝑉 ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ∖ { 𝑉 } ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
332 300 331 eqtrd ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { 𝑉 } ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
333 332 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { 𝑉 } ) ) = ( 𝑈 “ ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) )
334 299 333 eqtr3d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑉 } ) ) = ( 𝑈 “ ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) )
335 imaundi ⊢ ( 𝑈 “ ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∪ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) )
336 334 335 eqtrdi ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑉 } ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∪ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) )
337 336 eleq2d ⊢ ( 𝜑 → ( 𝑛 ∈ ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑉 } ) ) ↔ 𝑛 ∈ ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∪ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ) )
338 eldif ⊢ ( 𝑛 ∈ ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑉 } ) ) ↔ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑛 ∈ ( 𝑈 “ { 𝑉 } ) ) )
339 elun ⊢ ( 𝑛 ∈ ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∪ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ↔ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) )
340 337 338 339 3bitr3g ⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑛 ∈ ( 𝑈 “ { 𝑉 } ) ) ↔ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ) )
341 340 adantr ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑛 ∈ ( 𝑈 “ { 𝑉 } ) ) ↔ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ) )
342 imassrn ⊢ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ⊆ ran 𝑈
343 342 66 sstrid ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ⊆ ( 1 ... 𝑁 ) )
344 343 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
345 69 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → 𝑇 Fn ( 1 ... 𝑁 ) )
346 fnconstg ⊢ ( 1 ∈ V → ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) )
347 71 346 ax-mp ⊢ ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) )
348 fnconstg ⊢ ( 0 ∈ V → ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) )
349 74 348 ax-mp ⊢ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑉 ... 𝑁 ) )
350 347 349 pm3.2i ⊢ ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∧ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) )
351 imain ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... ( 𝑉 − 1 ) ) ∩ ( 𝑉 ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) )
352 9 351 syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑉 − 1 ) ) ∩ ( 𝑉 ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) )
353 fzdisj ⊢ ( ( 𝑉 − 1 ) < 𝑉 → ( ( 1 ... ( 𝑉 − 1 ) ) ∩ ( 𝑉 ... 𝑁 ) ) = ∅ )
354 317 353 syl ⊢ ( 𝜑 → ( ( 1 ... ( 𝑉 − 1 ) ) ∩ ( 𝑉 ... 𝑁 ) ) = ∅ )
355 354 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑉 − 1 ) ) ∩ ( 𝑉 ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
356 355 83 eqtrdi ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑉 − 1 ) ) ∩ ( 𝑉 ... 𝑁 ) ) ) = ∅ )
357 352 356 eqtr3d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) = ∅ )
358 fnun ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∧ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) ∧ ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) = ∅ ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) )
359 350 357 358 sylancr ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) )
360 imaundi ⊢ ( 𝑈 “ ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( 𝑉 ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) )
361 uzss ⊢ ( 𝑉 ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) → ( ℤ≥ ‘ 𝑉 ) ⊆ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) )
362 306 361 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑉 ) ⊆ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) )
363 elfzuz3 ⊢ ( 𝑉 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑉 ) )
364 5 363 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑉 ) )
365 362 364 sseldd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) )
366 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) )
367 365 366 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) )
368 16 367 eqeltrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) )
369 fzsplit2 ⊢ ( ( ( ( 𝑉 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( ( 𝑉 − 1 ) + 1 ) ... 𝑁 ) ) )
370 302 368 369 syl2anc ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( ( 𝑉 − 1 ) + 1 ) ... 𝑁 ) ) )
371 207 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑉 − 1 ) + 1 ) ... 𝑁 ) = ( 𝑉 ... 𝑁 ) )
372 371 uneq2d ⊢ ( 𝜑 → ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( ( ( 𝑉 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( 𝑉 ... 𝑁 ) ) )
373 370 372 eqtrd ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( 𝑉 ... 𝑁 ) ) )
374 373 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 𝑈 “ ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( 𝑉 ... 𝑁 ) ) ) )
375 374 104 eqtr3d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑉 − 1 ) ) ∪ ( 𝑉 ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
376 360 375 eqtr3id ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
377 376 fneq2d ⊢ ( 𝜑 → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) Fn ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∪ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) ↔ ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) ) )
378 359 377 mpbid ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
379 378 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
380 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
381 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
382 fvun1 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∧ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ∧ ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ‘ 𝑛 ) )
383 347 349 382 mp3an12 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ‘ 𝑛 ) )
384 357 383 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ‘ 𝑛 ) )
385 71 fvconst2 ⊢ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ‘ 𝑛 ) = 1 )
386 385 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ‘ 𝑛 ) = 1 )
387 384 386 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
388 387 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
389 345 379 380 380 111 381 388 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 1 ) )
390 108 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
391 fzss2 ⊢ ( 𝑉 ∈ ( ℤ≥ ‘ ( 𝑉 − 1 ) ) → ( 1 ... ( 𝑉 − 1 ) ) ⊆ ( 1 ... 𝑉 ) )
392 306 391 syl ⊢ ( 𝜑 → ( 1 ... ( 𝑉 − 1 ) ) ⊆ ( 1 ... 𝑉 ) )
393 imass2 ⊢ ( ( 1 ... ( 𝑉 − 1 ) ) ⊆ ( 1 ... 𝑉 ) → ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ⊆ ( 𝑈 “ ( 1 ... 𝑉 ) ) )
394 392 393 syl ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ⊆ ( 𝑈 “ ( 1 ... 𝑉 ) ) )
395 394 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑉 ) ) )
396 395 118 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
397 396 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 1 )
398 345 390 380 380 111 381 397 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 1 ) )
399 389 398 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
400 344 399 mpdan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
401 imassrn ⊢ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ⊆ ran 𝑈
402 401 66 sstrid ⊢ ( 𝜑 → ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ⊆ ( 1 ... 𝑁 ) )
403 402 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
404 69 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → 𝑇 Fn ( 1 ... 𝑁 ) )
405 378 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
406 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
407 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑛 ) = ( 𝑇 ‘ 𝑛 ) )
408 fzss1 ⊢ ( ( 𝑉 + 1 ) ∈ ( ℤ≥ ‘ 𝑉 ) → ( ( 𝑉 + 1 ) ... 𝑁 ) ⊆ ( 𝑉 ... 𝑁 ) )
409 imass2 ⊢ ( ( ( 𝑉 + 1 ) ... 𝑁 ) ⊆ ( 𝑉 ... 𝑁 ) → ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ⊆ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) )
410 143 144 408 409 4syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ⊆ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) )
411 410 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) )
412 fvun2 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∧ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ∧ ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
413 347 349 412 mp3an12 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∩ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) = ∅ ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
414 357 413 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = ( ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) )
415 74 fvconst2 ⊢ ( 𝑛 ∈ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) → ( ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) = 0 )
416 415 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) → ( ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ‘ 𝑛 ) = 0 )
417 414 416 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
418 411 417 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
419 418 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
420 404 405 406 406 111 407 419 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 0 ) )
421 108 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
422 179 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑛 ) = 0 )
423 404 421 406 406 111 407 422 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑛 ) + 0 ) )
424 420 423 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
425 403 424 mpdan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
426 400 425 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
427 426 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
428 2 adantr ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → 𝐹 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
429 199 a1i ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ∈ V )
430 209 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = if ( ( 𝑉 − 1 ) < 𝑀 , ( 𝑉 − 1 ) , 𝑉 ) )
431 lttr ⊢ ( ( ( 𝑉 − 1 ) ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( ( 𝑉 − 1 ) < 𝑉 ∧ 𝑉 < 𝑀 ) → ( 𝑉 − 1 ) < 𝑀 ) )
432 218 30 215 431 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑉 − 1 ) < 𝑉 ∧ 𝑉 < 𝑀 ) → ( 𝑉 − 1 ) < 𝑀 ) )
433 317 432 mpand ⊢ ( 𝜑 → ( 𝑉 < 𝑀 → ( 𝑉 − 1 ) < 𝑀 ) )
434 433 imp ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( 𝑉 − 1 ) < 𝑀 )
435 434 iftrued ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → if ( ( 𝑉 − 1 ) < 𝑀 , ( 𝑉 − 1 ) , 𝑉 ) = ( 𝑉 − 1 ) )
436 435 adantr ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → if ( ( 𝑉 − 1 ) < 𝑀 , ( 𝑉 − 1 ) , 𝑉 ) = ( 𝑉 − 1 ) )
437 430 436 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑉 − 1 ) )
438 simpll ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → 𝜑 )
439 oveq2 ⊢ ( 𝑗 = ( 𝑉 − 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑉 − 1 ) ) )
440 439 imaeq2d ⊢ ( 𝑗 = ( 𝑉 − 1 ) → ( 𝑈 “ ( 1 ... 𝑗 ) ) = ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) )
441 440 xpeq1d ⊢ ( 𝑗 = ( 𝑉 − 1 ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) )
442 441 adantl ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑉 − 1 ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) )
443 oveq1 ⊢ ( 𝑗 = ( 𝑉 − 1 ) → ( 𝑗 + 1 ) = ( ( 𝑉 − 1 ) + 1 ) )
444 443 207 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑉 − 1 ) ) → ( 𝑗 + 1 ) = 𝑉 )
445 444 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑉 − 1 ) ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( 𝑉 ... 𝑁 ) )
446 445 imaeq2d ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑉 − 1 ) ) → ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) )
447 446 xpeq1d ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑉 − 1 ) ) → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) )
448 442 447 uneq12d ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑉 − 1 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) )
449 448 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑉 − 1 ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) )
450 438 449 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) ∧ 𝑗 = ( 𝑉 − 1 ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) )
451 429 437 450 csbied2 ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑦 = ( 𝑉 − 1 ) ) → ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) )
452 240 adantr ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( 𝑉 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
453 ovexd ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ∈ V )
454 428 451 452 453 fvmptd ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( 𝐹 ‘ ( 𝑉 − 1 ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) )
455 454 fveq1d ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
456 455 adantr ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( 𝑉 ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
457 199 a1i ⊢ ( ( 𝑉 < 𝑀 ∧ 𝑦 = 𝑉 ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ∈ V )
458 iftrue ⊢ ( 𝑉 < 𝑀 → if ( 𝑉 < 𝑀 , 𝑉 , ( 𝑉 + 1 ) ) = 𝑉 )
459 250 458 sylan9eqr ⊢ ( ( 𝑉 < 𝑀 ∧ 𝑦 = 𝑉 ) → if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) = 𝑉 )
460 459 eqeq2d ⊢ ( ( 𝑉 < 𝑀 ∧ 𝑦 = 𝑉 ) → ( 𝑗 = if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ↔ 𝑗 = 𝑉 ) )
461 460 biimpa ⊢ ( ( ( 𝑉 < 𝑀 ∧ 𝑦 = 𝑉 ) ∧ 𝑗 = if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ) → 𝑗 = 𝑉 )
462 461 235 syl ⊢ ( ( ( 𝑉 < 𝑀 ∧ 𝑦 = 𝑉 ) ∧ 𝑗 = if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
463 457 462 csbied ⊢ ( ( 𝑉 < 𝑀 ∧ 𝑦 = 𝑉 ) → ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
464 463 adantll ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑦 = 𝑉 ) → ⦋ if ( 𝑦 < 𝑀 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
465 270 adantr ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → 𝑉 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
466 ovexd ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V )
467 428 464 465 466 fvmptd ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( 𝐹 ‘ 𝑉 ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
468 467 fveq1d ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
469 468 adantr ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ) → ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) = ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑉 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑛 ) )
470 427 456 469 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) )
471 470 ex ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( ( 𝑛 ∈ ( 𝑈 “ ( 1 ... ( 𝑉 − 1 ) ) ) ∨ 𝑛 ∈ ( 𝑈 “ ( ( 𝑉 + 1 ) ... 𝑁 ) ) ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ) )
472 341 471 sylbid ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ( ( 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑛 ∈ ( 𝑈 “ { 𝑉 } ) ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ) )
473 472 expdimp ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ) → ( ¬ 𝑛 ∈ ( 𝑈 “ { 𝑉 } ) → ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ) )
474 473 necon1ad ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 ∈ ( 𝑈 “ { 𝑉 } ) ) )
475 elimasni ⊢ ( 𝑛 ∈ ( 𝑈 “ { 𝑉 } ) → 𝑉 𝑈 𝑛 )
476 eqcom ⊢ ( 𝑛 = ( 𝑈 ‘ 𝑉 ) ↔ ( 𝑈 ‘ 𝑉 ) = 𝑛 )
477 fnbrfvb ⊢ ( ( 𝑈 Fn ( 1 ... 𝑁 ) ∧ 𝑉 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑈 ‘ 𝑉 ) = 𝑛 ↔ 𝑉 𝑈 𝑛 ) )
478 284 97 477 syl2anc ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑉 ) = 𝑛 ↔ 𝑉 𝑈 𝑛 ) )
479 476 478 bitrid ⊢ ( 𝜑 → ( 𝑛 = ( 𝑈 ‘ 𝑉 ) ↔ 𝑉 𝑈 𝑛 ) )
480 475 479 imbitrrid ⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝑈 “ { 𝑉 } ) → 𝑛 = ( 𝑈 ‘ 𝑉 ) ) )
481 480 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ) → ( 𝑛 ∈ ( 𝑈 “ { 𝑉 } ) → 𝑛 = ( 𝑈 ‘ 𝑉 ) ) )
482 474 481 syld ⊢ ( ( ( 𝜑 ∧ 𝑉 < 𝑀 ) ∧ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = ( 𝑈 ‘ 𝑉 ) ) )
483 482 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = ( 𝑈 ‘ 𝑉 ) ) )
484 fvex ⊢ ( 𝑈 ‘ 𝑉 ) ∈ V
485 eqeq2 ⊢ ( 𝑚 = ( 𝑈 ‘ 𝑉 ) → ( 𝑛 = 𝑚 ↔ 𝑛 = ( 𝑈 ‘ 𝑉 ) ) )
486 485 imbi2d ⊢ ( 𝑚 = ( 𝑈 ‘ 𝑉 ) → ( ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) ↔ ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = ( 𝑈 ‘ 𝑉 ) ) ) )
487 486 ralbidv ⊢ ( 𝑚 = ( 𝑈 ‘ 𝑉 ) → ( ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) ↔ ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = ( 𝑈 ‘ 𝑉 ) ) ) )
488 484 487 spcev ⊢ ( ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = ( 𝑈 ‘ 𝑉 ) ) → ∃ 𝑚 ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) )
489 483 488 syl ⊢ ( ( 𝜑 ∧ 𝑉 < 𝑀 ) → ∃ 𝑚 ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) )
490 eldifsni ⊢ ( 𝑀 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑀 ≠ 𝑉 )
491 6 490 syl ⊢ ( 𝜑 → 𝑀 ≠ 𝑉 )
492 215 30 lttri2d ⊢ ( 𝜑 → ( 𝑀 ≠ 𝑉 ↔ ( 𝑀 < 𝑉 ∨ 𝑉 < 𝑀 ) ) )
493 491 492 mpbid ⊢ ( 𝜑 → ( 𝑀 < 𝑉 ∨ 𝑉 < 𝑀 ) )
494 297 489 493 mpjaodan ⊢ ( 𝜑 → ∃ 𝑚 ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) )
495 nfv ⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 )
496 495 rmo2 ⊢ ( ∃* 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ↔ ∃ 𝑚 ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) )
497 rmoeq1 ⊢ ( ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) → ( ∃* 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ↔ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ) )
498 4 101 103 497 4syl ⊢ ( 𝜑 → ( ∃* 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ↔ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ) )
499 496 498 bitr3id ⊢ ( 𝜑 → ( ∃ 𝑚 ∀ 𝑛 ∈ ( 𝑈 “ ( 1 ... 𝑁 ) ) ( ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) → 𝑛 = 𝑚 ) ↔ ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) ) )
500 494 499 mpbid ⊢ ( 𝜑 → ∃* 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑉 − 1 ) ) ‘ 𝑛 ) ≠ ( ( 𝐹 ‘ 𝑉 ) ‘ 𝑛 ) )