Metamath Proof Explorer

Theorem poimirlem24

Description: Lemma for poimir , two ways of expressing that a simplex has an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
poimirlem28.1 ⊢ ( 𝑝 = ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → 𝐵 = 𝐶 )
poimirlem28.2 ⊢ ( ( 𝜑 ∧ 𝑝 : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) → 𝐵 ∈ ( 0 ... 𝑁 ) )
poimirlem25.3 ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
poimirlem25.4 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
poimirlem24.5 ⊢ ( 𝜑 → 𝑉 ∈ ( 0 ... 𝑁 ) )
Assertion poimirlem24 ( 𝜑 → ( ∃ 𝑥 ∈ ( ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ↑m ( 0 ... ( 𝑁 − 1 ) ) ) ( 𝑥 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ∧ ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran 𝑥 ↦ 𝐵 ) ∧ ∃ 𝑝 ∈ ran 𝑥 ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 poimirlem28.1 ⊢ ( 𝑝 = ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → 𝐵 = 𝐶 )
3 poimirlem28.2 ⊢ ( ( 𝜑 ∧ 𝑝 : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) → 𝐵 ∈ ( 0 ... 𝑁 ) )
4 poimirlem25.3 ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
5 poimirlem25.4 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
6 poimirlem24.5 ⊢ ( 𝜑 → 𝑉 ∈ ( 0 ... 𝑁 ) )
7 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
8 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
9 nfcv ⊢ Ⅎ 𝑗 ( 1 ... 𝑁 )
10 nfcv ⊢ Ⅎ 𝑗 ( 0 ... 𝐾 )
11 8 9 10 nff ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 )
12 7 11 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
13 eleq1 ⊢ ( 𝑗 = 𝑦 → ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
14 13 anbi2d ⊢ ( 𝑗 = 𝑦 → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ↔ ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ) )
15 csbeq1a ⊢ ( 𝑗 = 𝑦 → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
16 15 feq1d ⊢ ( 𝑗 = 𝑦 → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ↔ ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) )
17 14 16 imbi12d ⊢ ( 𝑗 = 𝑦 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) ) )
18 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
19 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
20 18 19 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
21 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
22 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
23 21 22 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
24 uzid ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
25 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
26 23 24 25 3syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
27 20 26 eqeltrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
28 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
29 27 28 syl ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
30 29 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
31 elun ⊢ ( 𝑦 ∈ ( { 1 } ∪ { 0 } ) ↔ ( 𝑦 ∈ { 1 } ∨ 𝑦 ∈ { 0 } ) )
32 fzofzp1 ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) → ( 𝑥 + 1 ) ∈ ( 0 ... 𝐾 ) )
33 elsni ⊢ ( 𝑦 ∈ { 1 } → 𝑦 = 1 )
34 33 oveq2d ⊢ ( 𝑦 ∈ { 1 } → ( 𝑥 + 𝑦 ) = ( 𝑥 + 1 ) )
35 34 eleq1d ⊢ ( 𝑦 ∈ { 1 } → ( ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝐾 ) ↔ ( 𝑥 + 1 ) ∈ ( 0 ... 𝐾 ) ) )
36 32 35 syl5ibrcom ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) → ( 𝑦 ∈ { 1 } → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝐾 ) ) )
37 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) → 𝑥 ∈ ℤ )
38 37 zcnd ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) → 𝑥 ∈ ℂ )
39 38 addid1d ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) → ( 𝑥 + 0 ) = 𝑥 )
40 elfzofz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) → 𝑥 ∈ ( 0 ... 𝐾 ) )
41 39 40 eqeltrd ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) → ( 𝑥 + 0 ) ∈ ( 0 ... 𝐾 ) )
42 elsni ⊢ ( 𝑦 ∈ { 0 } → 𝑦 = 0 )
43 42 oveq2d ⊢ ( 𝑦 ∈ { 0 } → ( 𝑥 + 𝑦 ) = ( 𝑥 + 0 ) )
44 43 eleq1d ⊢ ( 𝑦 ∈ { 0 } → ( ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝐾 ) ↔ ( 𝑥 + 0 ) ∈ ( 0 ... 𝐾 ) ) )
45 41 44 syl5ibrcom ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) → ( 𝑦 ∈ { 0 } → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝐾 ) ) )
46 36 45 jaod ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) → ( ( 𝑦 ∈ { 1 } ∨ 𝑦 ∈ { 0 } ) → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝐾 ) ) )
47 31 46 syl5bi ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) → ( 𝑦 ∈ ( { 1 } ∪ { 0 } ) → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝐾 ) ) )
48 47 imp ⊢ ( ( 𝑥 ∈ ( 0 ..^ 𝐾 ) ∧ 𝑦 ∈ ( { 1 } ∪ { 0 } ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝐾 ) )
49 48 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑥 ∈ ( 0 ..^ 𝐾 ) ∧ 𝑦 ∈ ( { 1 } ∪ { 0 } ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝐾 ) )
50 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑇 : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
51 1ex ⊢ 1 ∈ V
52 51 fconst ⊢ ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( 𝑈 “ ( 1 ... 𝑗 ) ) ⟶ { 1 }
53 c0ex ⊢ 0 ∈ V
54 53 fconst ⊢ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 }
55 52 54 pm3.2i ⊢ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( 𝑈 “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } )
56 dff1o3 ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ◡ 𝑈 ) )
57 56 simprbi ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ◡ 𝑈 )
58 imain ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
59 5 57 58 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
60 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℕ0 )
61 60 nn0red ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℝ )
62 61 ltp1d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 < ( 𝑗 + 1 ) )
63 fzdisj ⊢ ( 𝑗 < ( 𝑗 + 1 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
64 62 63 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
65 64 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
66 ima0 ⊢ ( 𝑈 “ ∅ ) = ∅
67 65 66 eqtrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
68 59 67 sylan9req ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
69 fun ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( 𝑈 “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } ) ∧ ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
70 55 68 69 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
71 nn0p1nn ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ )
72 60 71 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ℕ )
73 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
74 72 73 eleqtrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
75 elfzuz3 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) )
76 fzsplit2 ⊢ ( ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
77 74 75 76 syl2anc ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
78 77 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 𝑈 “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
79 imaundi ⊢ ( 𝑈 “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
80 78 79 eqtr2di ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ( 1 ... 𝑁 ) ) )
81 f1ofo ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
82 foima ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
83 5 81 82 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
84 80 83 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
85 84 feq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) ↔ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) ) )
86 70 85 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) )
87 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
88 87 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1 ... 𝑁 ) ∈ V )
89 inidm ⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
90 49 50 86 88 88 89 off ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
91 30 90 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
92 12 17 91 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
93 fzp1elp1 ⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑦 + 1 ) ∈ ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) )
94 20 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 0 ... 𝑁 ) )
95 94 eleq2d ⊢ ( 𝜑 → ( ( 𝑦 + 1 ) ∈ ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) ↔ ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
96 95 biimpa ⊢ ( ( 𝜑 ∧ ( 𝑦 + 1 ) ∈ ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) )
97 93 96 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) )
98 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) )
99 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
100 99 9 10 nff ⊢ Ⅎ 𝑗 ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 )
101 98 100 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
102 ovex ⊢ ( 𝑦 + 1 ) ∈ V
103 eleq1 ⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
104 103 anbi2d ⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑 ∧ ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) )
105 csbeq1a ⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
106 105 feq1d ⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ↔ ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) )
107 104 106 imbi12d ⊢ ( 𝑗 = ( 𝑦 + 1 ) → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) ↔ ( ( 𝜑 ∧ ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) ) )
108 101 102 107 90 vtoclf ⊢ ( ( 𝜑 ∧ ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) ) → ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
109 97 108 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
110 csbeq1 ⊢ ( 𝑦 = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) → ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
111 110 feq1d ⊢ ( 𝑦 = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) → ( ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ↔ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) )
112 csbeq1 ⊢ ( ( 𝑦 + 1 ) = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) → ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
113 112 feq1d ⊢ ( ( 𝑦 + 1 ) = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) → ( ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ↔ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) )
114 111 113 ifboth ⊢ ( ( ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ∧ ⦋ ( 𝑦 + 1 ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) → ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
115 92 109 114 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
116 ovex ⊢ ( 0 ... 𝐾 ) ∈ V
117 116 87 elmap ⊢ ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ↔ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
118 115 117 sylibr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
119 118 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
120 ovex ⊢ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ∈ V
121 ovex ⊢ ( 0 ... ( 𝑁 − 1 ) ) ∈ V
122 120 121 elmap ⊢ ( ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ∈ ( ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ↑m ( 0 ... ( 𝑁 − 1 ) ) ) ↔ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) : ( 0 ... ( 𝑁 − 1 ) ) ⟶ ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
123 119 122 sylibr ⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ∈ ( ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ↑m ( 0 ... ( 𝑁 − 1 ) ) ) )
124 rneq ⊢ ( 𝑥 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) → ran 𝑥 = ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) )
125 124 mpteq1d ⊢ ( 𝑥 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) → ( 𝑝 ∈ ran 𝑥 ↦ 𝐵 ) = ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) )
126 125 rneqd ⊢ ( 𝑥 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) → ran ( 𝑝 ∈ ran 𝑥 ↦ 𝐵 ) = ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) )
127 126 sseq2d ⊢ ( 𝑥 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) → ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran 𝑥 ↦ 𝐵 ) ↔ ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ) )
128 124 rexeqdv ⊢ ( 𝑥 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) → ( ∃ 𝑝 ∈ ran 𝑥 ( 𝑝 ‘ 𝑁 ) ≠ 0 ↔ ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ) )
129 127 128 anbi12d ⊢ ( 𝑥 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) → ( ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran 𝑥 ↦ 𝐵 ) ∧ ∃ 𝑝 ∈ ran 𝑥 ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ↔ ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ∧ ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ) )
130 129 ceqsrexv ⊢ ( ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ∈ ( ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ↑m ( 0 ... ( 𝑁 − 1 ) ) ) → ( ∃ 𝑥 ∈ ( ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ↑m ( 0 ... ( 𝑁 − 1 ) ) ) ( 𝑥 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ∧ ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran 𝑥 ↦ 𝐵 ) ∧ ∃ 𝑝 ∈ ran 𝑥 ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ) ↔ ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ∧ ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ) )
131 123 130 syl ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ↑m ( 0 ... ( 𝑁 − 1 ) ) ) ( 𝑥 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ∧ ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran 𝑥 ↦ 𝐵 ) ∧ ∃ 𝑝 ∈ ran 𝑥 ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ) ↔ ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ∧ ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ) )
132 dfss3 ⊢ ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 ∈ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) )
133 ovex ⊢ ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
134 133 2 csbie ⊢ ⦋ ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 = 𝐶
135 134 csbeq2i ⊢ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ ⦋ ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
136 opex ⊢ ⟨ 𝑇 , 𝑈 ⟩ ∈ V
137 136 a1i ⊢ ( 𝜑 → ⟨ 𝑇 , 𝑈 ⟩ ∈ V )
138 fveq2 ⊢ ( 𝑠 = ⟨ 𝑇 , 𝑈 ⟩ → ( 1st ‘ 𝑠 ) = ( 1st ‘ ⟨ 𝑇 , 𝑈 ⟩ ) )
139 fex ⊢ ( ( 𝑇 : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) ∧ ( 1 ... 𝑁 ) ∈ V ) → 𝑇 ∈ V )
140 4 87 139 sylancl ⊢ ( 𝜑 → 𝑇 ∈ V )
141 f1oexrnex ⊢ ( ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ( 1 ... 𝑁 ) ∈ V ) → 𝑈 ∈ V )
142 5 87 141 sylancl ⊢ ( 𝜑 → 𝑈 ∈ V )
143 op1stg ⊢ ( ( 𝑇 ∈ V ∧ 𝑈 ∈ V ) → ( 1st ‘ ⟨ 𝑇 , 𝑈 ⟩ ) = 𝑇 )
144 140 142 143 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑇 , 𝑈 ⟩ ) = 𝑇 )
145 138 144 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑠 = ⟨ 𝑇 , 𝑈 ⟩ ) → ( 1st ‘ 𝑠 ) = 𝑇 )
146 fveq2 ⊢ ( 𝑠 = ⟨ 𝑇 , 𝑈 ⟩ → ( 2nd ‘ 𝑠 ) = ( 2nd ‘ ⟨ 𝑇 , 𝑈 ⟩ ) )
147 op2ndg ⊢ ( ( 𝑇 ∈ V ∧ 𝑈 ∈ V ) → ( 2nd ‘ ⟨ 𝑇 , 𝑈 ⟩ ) = 𝑈 )
148 140 142 147 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑇 , 𝑈 ⟩ ) = 𝑈 )
149 146 148 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑠 = ⟨ 𝑇 , 𝑈 ⟩ ) → ( 2nd ‘ 𝑠 ) = 𝑈 )
150 imaeq1 ⊢ ( ( 2nd ‘ 𝑠 ) = 𝑈 → ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) = ( 𝑈 “ ( 1 ... 𝑗 ) ) )
151 150 xpeq1d ⊢ ( ( 2nd ‘ 𝑠 ) = 𝑈 → ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) )
152 imaeq1 ⊢ ( ( 2nd ‘ 𝑠 ) = 𝑈 → ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
153 152 xpeq1d ⊢ ( ( 2nd ‘ 𝑠 ) = 𝑈 → ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) )
154 151 153 uneq12d ⊢ ( ( 2nd ‘ 𝑠 ) = 𝑈 → ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
155 149 154 syl ⊢ ( ( 𝜑 ∧ 𝑠 = ⟨ 𝑇 , 𝑈 ⟩ ) → ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
156 145 155 oveq12d ⊢ ( ( 𝜑 ∧ 𝑠 = ⟨ 𝑇 , 𝑈 ⟩ ) → ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
157 156 csbeq1d ⊢ ( ( 𝜑 ∧ 𝑠 = ⟨ 𝑇 , 𝑈 ⟩ ) → ⦋ ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 = ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 )
158 137 157 csbied ⊢ ( 𝜑 → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ ⦋ ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 = ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 )
159 135 158 eqtr3id ⊢ ( 𝜑 → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 )
160 159 csbeq2dv ⊢ ( 𝜑 → ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 )
161 160 eqeq2d ⊢ ( 𝜑 → ( 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 ) )
162 161 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 ) )
163 vex ⊢ 𝑖 ∈ V
164 eqid ⊢ ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) = ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 )
165 164 elrnmpt ⊢ ( 𝑖 ∈ V → ( 𝑖 ∈ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ↔ ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) 𝑖 = 𝐵 ) )
166 163 165 ax-mp ⊢ ( 𝑖 ∈ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ↔ ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) 𝑖 = 𝐵 )
167 nfv ⊢ Ⅎ 𝑘 𝑖 = 𝐵
168 nfcsb1v ⊢ Ⅎ 𝑝 ⦋ 𝑘 / 𝑝 ⦌ 𝐵
169 168 nfeq2 ⊢ Ⅎ 𝑝 𝑖 = ⦋ 𝑘 / 𝑝 ⦌ 𝐵
170 csbeq1a ⊢ ( 𝑝 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑝 ⦌ 𝐵 )
171 170 eqeq2d ⊢ ( 𝑝 = 𝑘 → ( 𝑖 = 𝐵 ↔ 𝑖 = ⦋ 𝑘 / 𝑝 ⦌ 𝐵 ) )
172 167 169 171 cbvrexw ⊢ ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) 𝑖 = 𝐵 ↔ ∃ 𝑘 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) 𝑖 = ⦋ 𝑘 / 𝑝 ⦌ 𝐵 )
173 ovex ⊢ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
174 173 csbex ⊢ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
175 174 rgenw ⊢ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
176 eqid ⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
177 csbeq1 ⊢ ( 𝑘 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ⦋ 𝑘 / 𝑝 ⦌ 𝐵 = ⦋ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 )
178 vex ⊢ 𝑦 ∈ V
179 178 102 ifex ⊢ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) ∈ V
180 csbnestgw ⊢ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) ∈ V → ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 = ⦋ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 )
181 179 180 ax-mp ⊢ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 = ⦋ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵
182 177 181 eqtr4di ⊢ ( 𝑘 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ⦋ 𝑘 / 𝑝 ⦌ 𝐵 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 )
183 182 eqeq2d ⊢ ( 𝑘 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( 𝑖 = ⦋ 𝑘 / 𝑝 ⦌ 𝐵 ↔ 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 ) )
184 176 183 rexrnmptw ⊢ ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V → ( ∃ 𝑘 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) 𝑖 = ⦋ 𝑘 / 𝑝 ⦌ 𝐵 ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 ) )
185 175 184 ax-mp ⊢ ( ∃ 𝑘 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) 𝑖 = ⦋ 𝑘 / 𝑝 ⦌ 𝐵 ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 )
186 166 172 185 3bitri ⊢ ( 𝑖 ∈ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) / 𝑝 ⦌ 𝐵 )
187 162 186 bitr4di ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 ∈ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ) )
188 29 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 ∈ ( 0 ... 𝑁 ) )
189 188 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < 𝑉 ) → 𝑦 ∈ ( 0 ... 𝑁 ) )
190 elfzelz ⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℤ )
191 190 zred ⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℝ )
192 191 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 ∈ ℝ )
193 ltne ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑦 < 𝑉 ) → 𝑉 ≠ 𝑦 )
194 193 necomd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑦 < 𝑉 ) → 𝑦 ≠ 𝑉 )
195 192 194 sylan ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < 𝑉 ) → 𝑦 ≠ 𝑉 )
196 eldifsn ⊢ ( 𝑦 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ↔ ( 𝑦 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ≠ 𝑉 ) )
197 189 195 196 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑦 < 𝑉 ) → 𝑦 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) )
198 97 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < 𝑉 ) → ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) )
199 6 elfzelzd ⊢ ( 𝜑 → 𝑉 ∈ ℤ )
200 199 zred ⊢ ( 𝜑 → 𝑉 ∈ ℝ )
201 200 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < 𝑉 ) → 𝑉 ∈ ℝ )
202 zre ⊢ ( 𝑉 ∈ ℤ → 𝑉 ∈ ℝ )
203 zre ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
204 lenlt ⊢ ( ( 𝑉 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑉 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑉 ) )
205 202 203 204 syl2an ⊢ ( ( 𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑉 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑉 ) )
206 zleltp1 ⊢ ( ( 𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑉 ≤ 𝑦 ↔ 𝑉 < ( 𝑦 + 1 ) ) )
207 205 206 bitr3d ⊢ ( ( 𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ¬ 𝑦 < 𝑉 ↔ 𝑉 < ( 𝑦 + 1 ) ) )
208 199 190 207 syl2an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ¬ 𝑦 < 𝑉 ↔ 𝑉 < ( 𝑦 + 1 ) ) )
209 208 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < 𝑉 ) → 𝑉 < ( 𝑦 + 1 ) )
210 201 209 gtned ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < 𝑉 ) → ( 𝑦 + 1 ) ≠ 𝑉 )
211 eldifsn ⊢ ( ( 𝑦 + 1 ) ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ↔ ( ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) ∧ ( 𝑦 + 1 ) ≠ 𝑉 ) )
212 198 210 211 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < 𝑉 ) → ( 𝑦 + 1 ) ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) )
213 197 212 ifclda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) )
214 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
215 214 nfeq2 ⊢ Ⅎ 𝑗 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
216 csbeq1a ⊢ ( 𝑗 = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
217 216 eqeq2d ⊢ ( 𝑗 = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
218 215 217 rspce ⊢ ( ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ∧ 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
219 218 ex ⊢ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → ( 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
220 213 219 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
221 220 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
222 nfv ⊢ Ⅎ 𝑗 𝜑
223 nfcv ⊢ Ⅎ 𝑗 ( 0 ... ( 𝑁 − 1 ) )
224 223 215 nfrex ⊢ Ⅎ 𝑗 ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
225 eldifi ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
226 225 60 syl ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ∈ ℕ0 )
227 226 nn0ge0d ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 0 ≤ 𝑗 )
228 227 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 0 ≤ 𝑗 )
229 226 nn0red ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ∈ ℝ )
230 229 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 ∈ ℝ )
231 200 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑉 ∈ ℝ )
232 21 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
233 232 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑁 ∈ ℝ )
234 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 < 𝑉 )
235 elfzle2 ⊢ ( 𝑉 ∈ ( 0 ... 𝑁 ) → 𝑉 ≤ 𝑁 )
236 6 235 syl ⊢ ( 𝜑 → 𝑉 ≤ 𝑁 )
237 236 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑉 ≤ 𝑁 )
238 230 231 233 234 237 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 < 𝑁 )
239 225 elfzelzd ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ∈ ℤ )
240 zltlem1 ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 < 𝑁 ↔ 𝑗 ≤ ( 𝑁 − 1 ) ) )
241 239 21 240 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 < 𝑁 ↔ 𝑗 ≤ ( 𝑁 − 1 ) ) )
242 241 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → ( 𝑗 < 𝑁 ↔ 𝑗 ≤ ( 𝑁 − 1 ) ) )
243 238 242 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 ≤ ( 𝑁 − 1 ) )
244 0z ⊢ 0 ∈ ℤ
245 elfz ⊢ ( ( 𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝑁 − 1 ) ) ) )
246 244 245 mp3an2 ⊢ ( ( 𝑗 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝑁 − 1 ) ) ) )
247 239 23 246 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝑁 − 1 ) ) ) )
248 247 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝑁 − 1 ) ) ) )
249 228 243 248 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
250 0red ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 0 ∈ ℝ )
251 200 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑉 ∈ ℝ )
252 229 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑗 ∈ ℝ )
253 elfzle1 ⊢ ( 𝑉 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑉 )
254 6 253 syl ⊢ ( 𝜑 → 0 ≤ 𝑉 )
255 254 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 0 ≤ 𝑉 )
256 lenlt ⊢ ( ( 𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( 𝑉 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑉 ) )
257 200 229 256 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑉 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑉 ) )
258 257 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑉 ≤ 𝑗 )
259 eldifsni ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ≠ 𝑉 )
260 259 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑗 ≠ 𝑉 )
261 ltlen ⊢ ( ( 𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( 𝑉 < 𝑗 ↔ ( 𝑉 ≤ 𝑗 ∧ 𝑗 ≠ 𝑉 ) ) )
262 200 229 261 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑉 < 𝑗 ↔ ( 𝑉 ≤ 𝑗 ∧ 𝑗 ≠ 𝑉 ) ) )
263 262 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ( 𝑉 < 𝑗 ↔ ( 𝑉 ≤ 𝑗 ∧ 𝑗 ≠ 𝑉 ) ) )
264 258 260 263 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑉 < 𝑗 )
265 250 251 252 255 264 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 0 < 𝑗 )
266 zgt0ge1 ⊢ ( 𝑗 ∈ ℤ → ( 0 < 𝑗 ↔ 1 ≤ 𝑗 ) )
267 239 266 syl ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → ( 0 < 𝑗 ↔ 1 ≤ 𝑗 ) )
268 267 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ( 0 < 𝑗 ↔ 1 ≤ 𝑗 ) )
269 265 268 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 1 ≤ 𝑗 )
270 elfzle2 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ≤ 𝑁 )
271 225 270 syl ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ≤ 𝑁 )
272 271 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑗 ≤ 𝑁 )
273 1z ⊢ 1 ∈ ℤ
274 elfz ⊢ ( ( 𝑗 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
275 273 274 mp3an2 ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
276 239 21 275 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
277 276 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
278 269 272 277 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
279 elfzmlbm ⊢ ( 𝑗 ∈ ( 1 ... 𝑁 ) → ( 𝑗 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
280 278 279 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ( 𝑗 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
281 249 280 ifclda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
282 breq1 ⊢ ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑗 < 𝑉 ↔ if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 ) )
283 id ⊢ ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) )
284 oveq1 ⊢ ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑗 + 1 ) = ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) )
285 282 283 284 ifbieq12d ⊢ ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 + 1 ) ) = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) )
286 285 eqeq2d ⊢ ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑗 = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) ) )
287 breq1 ⊢ ( ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( ( 𝑗 − 1 ) < 𝑉 ↔ if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 ) )
288 id ⊢ ( ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) )
289 oveq1 ⊢ ( ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( ( 𝑗 − 1 ) + 1 ) = ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) )
290 287 288 289 ifbieq12d ⊢ ( ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → if ( ( 𝑗 − 1 ) < 𝑉 , ( 𝑗 − 1 ) , ( ( 𝑗 − 1 ) + 1 ) ) = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) )
291 290 eqeq2d ⊢ ( ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑗 = if ( ( 𝑗 − 1 ) < 𝑉 , ( 𝑗 − 1 ) , ( ( 𝑗 − 1 ) + 1 ) ) ↔ 𝑗 = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) ) )
292 iftrue ⊢ ( 𝑗 < 𝑉 → if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 + 1 ) ) = 𝑗 )
293 292 eqcomd ⊢ ( 𝑗 < 𝑉 → 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 + 1 ) ) )
294 293 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 + 1 ) ) )
295 zlem1lt ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑉 ∈ ℤ ) → ( 𝑗 ≤ 𝑉 ↔ ( 𝑗 − 1 ) < 𝑉 ) )
296 239 199 295 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 ≤ 𝑉 ↔ ( 𝑗 − 1 ) < 𝑉 ) )
297 259 necomd ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑉 ≠ 𝑗 )
298 297 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → 𝑉 ≠ 𝑗 )
299 ltlen ⊢ ( ( 𝑗 ∈ ℝ ∧ 𝑉 ∈ ℝ ) → ( 𝑗 < 𝑉 ↔ ( 𝑗 ≤ 𝑉 ∧ 𝑉 ≠ 𝑗 ) ) )
300 229 200 299 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 < 𝑉 ↔ ( 𝑗 ≤ 𝑉 ∧ 𝑉 ≠ 𝑗 ) ) )
301 300 biimprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( ( 𝑗 ≤ 𝑉 ∧ 𝑉 ≠ 𝑗 ) → 𝑗 < 𝑉 ) )
302 298 301 mpan2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 ≤ 𝑉 → 𝑗 < 𝑉 ) )
303 296 302 sylbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( ( 𝑗 − 1 ) < 𝑉 → 𝑗 < 𝑉 ) )
304 303 con3dimp ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ¬ ( 𝑗 − 1 ) < 𝑉 )
305 304 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → if ( ( 𝑗 − 1 ) < 𝑉 , ( 𝑗 − 1 ) , ( ( 𝑗 − 1 ) + 1 ) ) = ( ( 𝑗 − 1 ) + 1 ) )
306 226 nn0cnd ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ∈ ℂ )
307 npcan1 ⊢ ( 𝑗 ∈ ℂ → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
308 306 307 syl ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
309 308 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
310 305 309 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑗 = if ( ( 𝑗 − 1 ) < 𝑉 , ( 𝑗 − 1 ) , ( ( 𝑗 − 1 ) + 1 ) ) )
311 286 291 294 310 ifbothda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → 𝑗 = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) )
312 csbeq1a ⊢ ( 𝑗 = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
313 311 312 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
314 313 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
315 314 biimpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑖 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
316 breq1 ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑦 < 𝑉 ↔ if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 ) )
317 id ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) )
318 oveq1 ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑦 + 1 ) = ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) )
319 316 317 318 ifbieq12d ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) )
320 319 csbeq1d ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
321 320 eqeq2d ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
322 321 rspcev ⊢ ( ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑖 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
323 281 315 322 syl6an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
324 323 ex ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
325 222 224 324 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
326 221 325 impbid ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
327 187 326 bitr3d ⊢ ( 𝜑 → ( 𝑖 ∈ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
328 327 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 ∈ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
329 132 328 syl5bb ⊢ ( 𝜑 → ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
330 329 anbi1d ⊢ ( 𝜑 → ( ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ∧ ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ↔ ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ) )
331 1 4 5 6 poimirlem23 ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ↔ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) )
332 331 anbi2d ⊢ ( 𝜑 → ( ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ↔ ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) ) )
333 131 330 332 3bitrd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( ( 0 ... 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ↑m ( 0 ... ( 𝑁 − 1 ) ) ) ( 𝑥 = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ∧ ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran 𝑥 ↦ 𝐵 ) ∧ ∃ 𝑝 ∈ ran 𝑥 ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) ) )