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 elfzelz ⊢ ( 𝑉 ∈ ( 0 ... 𝑁 ) → 𝑉 ∈ ℤ )
200 6 199 syl ⊢ ( 𝜑 → 𝑉 ∈ ℤ )
201 200 zred ⊢ ( 𝜑 → 𝑉 ∈ ℝ )
202 201 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < 𝑉 ) → 𝑉 ∈ ℝ )
203 zre ⊢ ( 𝑉 ∈ ℤ → 𝑉 ∈ ℝ )
204 zre ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
205 lenlt ⊢ ( ( 𝑉 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑉 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑉 ) )
206 203 204 205 syl2an ⊢ ( ( 𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑉 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑉 ) )
207 zleltp1 ⊢ ( ( 𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑉 ≤ 𝑦 ↔ 𝑉 < ( 𝑦 + 1 ) ) )
208 206 207 bitr3d ⊢ ( ( 𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ¬ 𝑦 < 𝑉 ↔ 𝑉 < ( 𝑦 + 1 ) ) )
209 200 190 208 syl2an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ¬ 𝑦 < 𝑉 ↔ 𝑉 < ( 𝑦 + 1 ) ) )
210 209 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < 𝑉 ) → 𝑉 < ( 𝑦 + 1 ) )
211 202 210 gtned ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < 𝑉 ) → ( 𝑦 + 1 ) ≠ 𝑉 )
212 eldifsn ⊢ ( ( 𝑦 + 1 ) ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ↔ ( ( 𝑦 + 1 ) ∈ ( 0 ... 𝑁 ) ∧ ( 𝑦 + 1 ) ≠ 𝑉 ) )
213 198 211 212 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑦 < 𝑉 ) → ( 𝑦 + 1 ) ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) )
214 197 213 ifclda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) )
215 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
216 215 nfeq2 ⊢ Ⅎ 𝑗 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
217 csbeq1a ⊢ ( 𝑗 = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
218 217 eqeq2d ⊢ ( 𝑗 = if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
219 216 218 rspce ⊢ ( ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ∧ 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
220 219 ex ⊢ ( if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → ( 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
221 214 220 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
222 221 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
223 nfv ⊢ Ⅎ 𝑗 𝜑
224 nfcv ⊢ Ⅎ 𝑗 ( 0 ... ( 𝑁 − 1 ) )
225 224 216 nfrex ⊢ Ⅎ 𝑗 ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
226 eldifi ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
227 226 60 syl ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ∈ ℕ0 )
228 227 nn0ge0d ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 0 ≤ 𝑗 )
229 228 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 0 ≤ 𝑗 )
230 227 nn0red ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ∈ ℝ )
231 230 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 ∈ ℝ )
232 201 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑉 ∈ ℝ )
233 21 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
234 233 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑁 ∈ ℝ )
235 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 < 𝑉 )
236 elfzle2 ⊢ ( 𝑉 ∈ ( 0 ... 𝑁 ) → 𝑉 ≤ 𝑁 )
237 6 236 syl ⊢ ( 𝜑 → 𝑉 ≤ 𝑁 )
238 237 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑉 ≤ 𝑁 )
239 231 232 234 235 238 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 < 𝑁 )
240 227 nn0zd ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ∈ ℤ )
241 zltlem1 ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 < 𝑁 ↔ 𝑗 ≤ ( 𝑁 − 1 ) ) )
242 240 21 241 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 < 𝑁 ↔ 𝑗 ≤ ( 𝑁 − 1 ) ) )
243 242 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → ( 𝑗 < 𝑁 ↔ 𝑗 ≤ ( 𝑁 − 1 ) ) )
244 239 243 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 ≤ ( 𝑁 − 1 ) )
245 0z ⊢ 0 ∈ ℤ
246 elfz ⊢ ( ( 𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝑁 − 1 ) ) ) )
247 245 246 mp3an2 ⊢ ( ( 𝑗 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝑁 − 1 ) ) ) )
248 240 23 247 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝑁 − 1 ) ) ) )
249 248 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝑁 − 1 ) ) ) )
250 229 244 249 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
251 0red ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 0 ∈ ℝ )
252 201 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑉 ∈ ℝ )
253 230 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑗 ∈ ℝ )
254 elfzle1 ⊢ ( 𝑉 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑉 )
255 6 254 syl ⊢ ( 𝜑 → 0 ≤ 𝑉 )
256 255 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 0 ≤ 𝑉 )
257 lenlt ⊢ ( ( 𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( 𝑉 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑉 ) )
258 201 230 257 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑉 ≤ 𝑗 ↔ ¬ 𝑗 < 𝑉 ) )
259 258 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑉 ≤ 𝑗 )
260 eldifsni ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ≠ 𝑉 )
261 260 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑗 ≠ 𝑉 )
262 ltlen ⊢ ( ( 𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( 𝑉 < 𝑗 ↔ ( 𝑉 ≤ 𝑗 ∧ 𝑗 ≠ 𝑉 ) ) )
263 201 230 262 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑉 < 𝑗 ↔ ( 𝑉 ≤ 𝑗 ∧ 𝑗 ≠ 𝑉 ) ) )
264 263 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ( 𝑉 < 𝑗 ↔ ( 𝑉 ≤ 𝑗 ∧ 𝑗 ≠ 𝑉 ) ) )
265 259 261 264 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑉 < 𝑗 )
266 251 252 253 256 265 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 0 < 𝑗 )
267 zgt0ge1 ⊢ ( 𝑗 ∈ ℤ → ( 0 < 𝑗 ↔ 1 ≤ 𝑗 ) )
268 240 267 syl ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → ( 0 < 𝑗 ↔ 1 ≤ 𝑗 ) )
269 268 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ( 0 < 𝑗 ↔ 1 ≤ 𝑗 ) )
270 266 269 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 1 ≤ 𝑗 )
271 elfzle2 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ≤ 𝑁 )
272 226 271 syl ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ≤ 𝑁 )
273 272 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑗 ≤ 𝑁 )
274 1z ⊢ 1 ∈ ℤ
275 elfz ⊢ ( ( 𝑗 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
276 274 275 mp3an2 ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
277 240 21 276 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
278 277 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
279 270 273 278 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
280 elfzmlbm ⊢ ( 𝑗 ∈ ( 1 ... 𝑁 ) → ( 𝑗 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
281 279 280 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ( 𝑗 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
282 250 281 ifclda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
283 breq1 ⊢ ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑗 < 𝑉 ↔ if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 ) )
284 id ⊢ ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) )
285 oveq1 ⊢ ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑗 + 1 ) = ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) )
286 283 284 285 ifbieq12d ⊢ ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 + 1 ) ) = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) )
287 286 eqeq2d ⊢ ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 + 1 ) ) ↔ 𝑗 = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) ) )
288 breq1 ⊢ ( ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( ( 𝑗 − 1 ) < 𝑉 ↔ if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 ) )
289 id ⊢ ( ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) )
290 oveq1 ⊢ ( ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( ( 𝑗 − 1 ) + 1 ) = ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) )
291 288 289 290 ifbieq12d ⊢ ( ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → if ( ( 𝑗 − 1 ) < 𝑉 , ( 𝑗 − 1 ) , ( ( 𝑗 − 1 ) + 1 ) ) = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) )
292 291 eqeq2d ⊢ ( ( 𝑗 − 1 ) = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑗 = if ( ( 𝑗 − 1 ) < 𝑉 , ( 𝑗 − 1 ) , ( ( 𝑗 − 1 ) + 1 ) ) ↔ 𝑗 = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) ) )
293 iftrue ⊢ ( 𝑗 < 𝑉 → if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 + 1 ) ) = 𝑗 )
294 293 eqcomd ⊢ ( 𝑗 < 𝑉 → 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 + 1 ) ) )
295 294 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ 𝑗 < 𝑉 ) → 𝑗 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 + 1 ) ) )
296 zlem1lt ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑉 ∈ ℤ ) → ( 𝑗 ≤ 𝑉 ↔ ( 𝑗 − 1 ) < 𝑉 ) )
297 240 200 296 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 ≤ 𝑉 ↔ ( 𝑗 − 1 ) < 𝑉 ) )
298 260 necomd ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑉 ≠ 𝑗 )
299 298 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → 𝑉 ≠ 𝑗 )
300 ltlen ⊢ ( ( 𝑗 ∈ ℝ ∧ 𝑉 ∈ ℝ ) → ( 𝑗 < 𝑉 ↔ ( 𝑗 ≤ 𝑉 ∧ 𝑉 ≠ 𝑗 ) ) )
301 230 201 300 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 < 𝑉 ↔ ( 𝑗 ≤ 𝑉 ∧ 𝑉 ≠ 𝑗 ) ) )
302 301 biimprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( ( 𝑗 ≤ 𝑉 ∧ 𝑉 ≠ 𝑗 ) → 𝑗 < 𝑉 ) )
303 299 302 mpan2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑗 ≤ 𝑉 → 𝑗 < 𝑉 ) )
304 297 303 sylbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( ( 𝑗 − 1 ) < 𝑉 → 𝑗 < 𝑉 ) )
305 304 con3dimp ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ¬ ( 𝑗 − 1 ) < 𝑉 )
306 305 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → if ( ( 𝑗 − 1 ) < 𝑉 , ( 𝑗 − 1 ) , ( ( 𝑗 − 1 ) + 1 ) ) = ( ( 𝑗 − 1 ) + 1 ) )
307 227 nn0cnd ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → 𝑗 ∈ ℂ )
308 npcan1 ⊢ ( 𝑗 ∈ ℂ → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
309 307 308 syl ⊢ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
310 309 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
311 306 310 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) ∧ ¬ 𝑗 < 𝑉 ) → 𝑗 = if ( ( 𝑗 − 1 ) < 𝑉 , ( 𝑗 − 1 ) , ( ( 𝑗 − 1 ) + 1 ) ) )
312 287 292 295 311 ifbothda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → 𝑗 = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) )
313 csbeq1a ⊢ ( 𝑗 = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
314 312 313 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
315 314 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
316 315 biimpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑖 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
317 breq1 ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑦 < 𝑉 ↔ if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 ) )
318 id ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) )
319 oveq1 ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑦 + 1 ) = ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) )
320 317 318 319 ifbieq12d ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) = if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) )
321 320 csbeq1d ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
322 321 eqeq2d ⊢ ( 𝑦 = if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) → ( 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
323 322 rspcev ⊢ ( ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑖 = ⦋ if ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) < 𝑉 , if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) , ( if ( 𝑗 < 𝑉 , 𝑗 , ( 𝑗 − 1 ) ) + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
324 282 316 323 syl6an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
325 324 ex ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
326 223 225 325 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
327 222 326 impbid ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
328 187 327 bitr3d ⊢ ( 𝜑 → ( 𝑖 ∈ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
329 328 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝑖 ∈ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
330 132 329 syl5bb ⊢ ( 𝜑 → ( ( 0 ... ( 𝑁 − 1 ) ) ⊆ ran ( 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ↦ 𝐵 ) ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
331 330 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 ) ) )
332 1 4 5 6 poimirlem23 ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ↔ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) )
333 332 anbi2d ⊢ ( 𝜑 → ( ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ) ↔ ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑉 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) ) )
334 131 331 333 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 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) ) )