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