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