Metamath Proof Explorer

Theorem poimirlem23

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

Ref Expression
Hypotheses poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
poimirlem23.1 ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
poimirlem23.2 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
poimirlem23.3 ⊢ ( 𝜑 → 𝑉 ∈ ( 0 ... 𝑁 ) )
Assertion poimirlem23 ( 𝜑 → ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ↔ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 poimirlem23.1 ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
3 poimirlem23.2 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
4 poimirlem23.3 ⊢ ( 𝜑 → 𝑉 ∈ ( 0 ... 𝑁 ) )
5 ovex ⊢ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
6 5 csbex ⊢ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
7 6 rgenw ⊢ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
8 eqid ⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
9 fveq1 ⊢ ( 𝑝 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( 𝑝 ‘ 𝑁 ) = ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) )
10 9 neeq1d ⊢ ( 𝑝 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( ( 𝑝 ‘ 𝑁 ) ≠ 0 ↔ ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ) )
11 df-ne ⊢ ( ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ↔ ¬ ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
12 10 11 bitrdi ⊢ ( 𝑝 = ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( ( 𝑝 ‘ 𝑁 ) ≠ 0 ↔ ¬ ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
13 8 12 rexrnmptw ⊢ ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V → ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
14 7 13 ax-mp ⊢ ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ↔ ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
15 rexnal ⊢ ( ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
16 14 15 bitri ⊢ ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ↔ ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
17 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
18 elfzelz ⊢ ( 𝑉 ∈ ( 0 ... 𝑁 ) → 𝑉 ∈ ℤ )
19 4 18 syl ⊢ ( 𝜑 → 𝑉 ∈ ℤ )
20 zlem1lt ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ ) → ( 𝑁 ≤ 𝑉 ↔ ( 𝑁 − 1 ) < 𝑉 ) )
21 17 19 20 syl2anc ⊢ ( 𝜑 → ( 𝑁 ≤ 𝑉 ↔ ( 𝑁 − 1 ) < 𝑉 ) )
22 elfzle2 ⊢ ( 𝑉 ∈ ( 0 ... 𝑁 ) → 𝑉 ≤ 𝑁 )
23 4 22 syl ⊢ ( 𝜑 → 𝑉 ≤ 𝑁 )
24 19 zred ⊢ ( 𝜑 → 𝑉 ∈ ℝ )
25 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
26 24 25 letri3d ⊢ ( 𝜑 → ( 𝑉 = 𝑁 ↔ ( 𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉 ) ) )
27 26 biimprd ⊢ ( 𝜑 → ( ( 𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉 ) → 𝑉 = 𝑁 ) )
28 23 27 mpand ⊢ ( 𝜑 → ( 𝑁 ≤ 𝑉 → 𝑉 = 𝑁 ) )
29 21 28 sylbird ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) < 𝑉 → 𝑉 = 𝑁 ) )
30 29 necon3ad ⊢ ( 𝜑 → ( 𝑉 ≠ 𝑁 → ¬ ( 𝑁 − 1 ) < 𝑉 ) )
31 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
32 1 31 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
33 nn0fz0 ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 ↔ ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
34 32 33 sylib ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
36 iffalse ⊢ ( ¬ ( 𝑁 − 1 ) < 𝑉 → if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝑁 − 1 ) + 1 ) )
37 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
38 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
39 37 38 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
40 36 39 sylan9eqr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) = 𝑁 )
41 40 csbeq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ⦋ if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ 𝑁 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
42 oveq2 ⊢ ( 𝑗 = 𝑁 → ( 1 ... 𝑗 ) = ( 1 ... 𝑁 ) )
43 42 imaeq2d ⊢ ( 𝑗 = 𝑁 → ( 𝑈 “ ( 1 ... 𝑗 ) ) = ( 𝑈 “ ( 1 ... 𝑁 ) ) )
44 43 xpeq1d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... 𝑁 ) ) × { 1 } ) )
45 oveq1 ⊢ ( 𝑗 = 𝑁 → ( 𝑗 + 1 ) = ( 𝑁 + 1 ) )
46 45 oveq1d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( 𝑁 + 1 ) ... 𝑁 ) )
47 46 imaeq2d ⊢ ( 𝑗 = 𝑁 → ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) )
48 47 xpeq1d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) )
49 44 48 uneq12d ⊢ ( 𝑗 = 𝑁 → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... 𝑁 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
50 f1ofo ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
51 foima ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
52 3 50 51 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
53 52 xpeq1d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... 𝑁 ) ) × { 1 } ) = ( ( 1 ... 𝑁 ) × { 1 } ) )
54 25 ltp1d ⊢ ( 𝜑 → 𝑁 < ( 𝑁 + 1 ) )
55 17 peano2zd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
56 fzn ⊢ ( ( ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 < ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) ... 𝑁 ) = ∅ ) )
57 55 17 56 syl2anc ⊢ ( 𝜑 → ( 𝑁 < ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) ... 𝑁 ) = ∅ ) )
58 54 57 mpbid ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) ... 𝑁 ) = ∅ )
59 58 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ∅ ) )
60 59 xpeq1d ⊢ ( 𝜑 → ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ∅ ) × { 0 } ) )
61 ima0 ⊢ ( 𝑈 “ ∅ ) = ∅
62 61 xpeq1i ⊢ ( ( 𝑈 “ ∅ ) × { 0 } ) = ( ∅ × { 0 } )
63 0xp ⊢ ( ∅ × { 0 } ) = ∅
64 62 63 eqtri ⊢ ( ( 𝑈 “ ∅ ) × { 0 } ) = ∅
65 60 64 eqtrdi ⊢ ( 𝜑 → ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) = ∅ )
66 53 65 uneq12d ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... 𝑁 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 1 ... 𝑁 ) × { 1 } ) ∪ ∅ ) )
67 un0 ⊢ ( ( ( 1 ... 𝑁 ) × { 1 } ) ∪ ∅ ) = ( ( 1 ... 𝑁 ) × { 1 } )
68 66 67 eqtrdi ⊢ ( 𝜑 → ( ( ( 𝑈 “ ( 1 ... 𝑁 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑁 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( 1 ... 𝑁 ) × { 1 } ) )
69 49 68 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑗 = 𝑁 ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( 1 ... 𝑁 ) × { 1 } ) )
70 69 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 = 𝑁 ) → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( 1 ... 𝑁 ) × { 1 } ) ) )
71 1 70 csbied ⊢ ( 𝜑 → ⦋ 𝑁 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( 1 ... 𝑁 ) × { 1 } ) ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ⦋ 𝑁 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( 1 ... 𝑁 ) × { 1 } ) ) )
73 41 72 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ⦋ if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ( 𝑇 ∘f + ( ( 1 ... 𝑁 ) × { 1 } ) ) )
74 73 fveq1d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ( ⦋ if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( ( 𝑇 ∘f + ( ( 1 ... 𝑁 ) × { 1 } ) ) ‘ 𝑁 ) )
75 elfzonn0 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝐾 ) → 𝑗 ∈ ℕ0 )
76 nn0p1nn ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ )
77 75 76 syl ⊢ ( 𝑗 ∈ ( 0 ..^ 𝐾 ) → ( 𝑗 + 1 ) ∈ ℕ )
78 elsni ⊢ ( 𝑦 ∈ { 1 } → 𝑦 = 1 )
79 78 oveq2d ⊢ ( 𝑦 ∈ { 1 } → ( 𝑗 + 𝑦 ) = ( 𝑗 + 1 ) )
80 79 eleq1d ⊢ ( 𝑦 ∈ { 1 } → ( ( 𝑗 + 𝑦 ) ∈ ℕ ↔ ( 𝑗 + 1 ) ∈ ℕ ) )
81 77 80 syl5ibrcom ⊢ ( 𝑗 ∈ ( 0 ..^ 𝐾 ) → ( 𝑦 ∈ { 1 } → ( 𝑗 + 𝑦 ) ∈ ℕ ) )
82 81 imp ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝐾 ) ∧ 𝑦 ∈ { 1 } ) → ( 𝑗 + 𝑦 ) ∈ ℕ )
83 82 adantl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ..^ 𝐾 ) ∧ 𝑦 ∈ { 1 } ) ) → ( 𝑗 + 𝑦 ) ∈ ℕ )
84 1ex ⊢ 1 ∈ V
85 84 fconst ⊢ ( ( 1 ... 𝑁 ) × { 1 } ) : ( 1 ... 𝑁 ) ⟶ { 1 }
86 85 a1i ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) × { 1 } ) : ( 1 ... 𝑁 ) ⟶ { 1 } )
87 ovexd ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ V )
88 inidm ⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
89 83 2 86 87 87 88 off ⊢ ( 𝜑 → ( 𝑇 ∘f + ( ( 1 ... 𝑁 ) × { 1 } ) ) : ( 1 ... 𝑁 ) ⟶ ℕ )
90 elfz1end ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( 1 ... 𝑁 ) )
91 1 90 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑁 ) )
92 89 91 ffvelrnd ⊢ ( 𝜑 → ( ( 𝑇 ∘f + ( ( 1 ... 𝑁 ) × { 1 } ) ) ‘ 𝑁 ) ∈ ℕ )
93 92 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ( ( 𝑇 ∘f + ( ( 1 ... 𝑁 ) × { 1 } ) ) ‘ 𝑁 ) ∈ ℕ )
94 74 93 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ( ⦋ if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ∈ ℕ )
95 94 nnne0d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ( ⦋ if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 )
96 breq1 ⊢ ( 𝑦 = ( 𝑁 − 1 ) → ( 𝑦 < 𝑉 ↔ ( 𝑁 − 1 ) < 𝑉 ) )
97 id ⊢ ( 𝑦 = ( 𝑁 − 1 ) → 𝑦 = ( 𝑁 − 1 ) )
98 oveq1 ⊢ ( 𝑦 = ( 𝑁 − 1 ) → ( 𝑦 + 1 ) = ( ( 𝑁 − 1 ) + 1 ) )
99 96 97 98 ifbieq12d ⊢ ( 𝑦 = ( 𝑁 − 1 ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) = if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) )
100 99 csbeq1d ⊢ ( 𝑦 = ( 𝑁 − 1 ) → ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
101 100 fveq1d ⊢ ( 𝑦 = ( 𝑁 − 1 ) → ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( ⦋ if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) )
102 101 neeq1d ⊢ ( 𝑦 = ( 𝑁 − 1 ) → ( ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ↔ ( ⦋ if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ) )
103 11 102 bitr3id ⊢ ( 𝑦 = ( 𝑁 − 1 ) → ( ¬ ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ⦋ if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ) )
104 103 rspcev ⊢ ( ( ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ ( ⦋ if ( ( 𝑁 − 1 ) < 𝑉 , ( 𝑁 − 1 ) , ( ( 𝑁 − 1 ) + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) ≠ 0 ) → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
105 35 95 104 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ∃ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
106 105 15 sylib ⊢ ( ( 𝜑 ∧ ¬ ( 𝑁 − 1 ) < 𝑉 ) → ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
107 106 ex ⊢ ( 𝜑 → ( ¬ ( 𝑁 − 1 ) < 𝑉 → ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
108 30 107 syld ⊢ ( 𝜑 → ( 𝑉 ≠ 𝑁 → ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
109 108 necon4ad ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 → 𝑉 = 𝑁 ) )
110 109 pm4.71rd ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( 𝑉 = 𝑁 ∧ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) ) )
111 32 nn0zd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
112 uzid ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
113 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
114 111 112 113 3syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
115 39 114 eqeltrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
116 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
117 115 116 syl ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
118 117 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
119 91 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
120 2 ffnd ⊢ ( 𝜑 → 𝑇 Fn ( 1 ... 𝑁 ) )
121 120 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑇 Fn ( 1 ... 𝑁 ) )
122 84 fconst ⊢ ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( 𝑈 “ ( 1 ... 𝑗 ) ) ⟶ { 1 }
123 c0ex ⊢ 0 ∈ V
124 123 fconst ⊢ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 }
125 122 124 pm3.2i ⊢ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( 𝑈 “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } )
126 dff1o3 ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 𝑈 : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ◡ 𝑈 ) )
127 126 simprbi ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ◡ 𝑈 )
128 imain ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
129 3 127 128 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
130 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℤ )
131 130 zred ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℝ )
132 131 ltp1d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 < ( 𝑗 + 1 ) )
133 fzdisj ⊢ ( 𝑗 < ( 𝑗 + 1 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
134 132 133 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
135 134 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
136 135 61 eqtrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
137 129 136 sylan9req ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
138 fun ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( 𝑈 “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } ) ∧ ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
139 125 137 138 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
140 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℕ0 )
141 140 76 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ℕ )
142 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
143 141 142 eleqtrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
144 elfzuz3 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) )
145 fzsplit2 ⊢ ( ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
146 143 144 145 syl2anc ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
147 146 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑈 “ ( 1 ... 𝑁 ) ) = ( 𝑈 “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
148 imaundi ⊢ ( 𝑈 “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
149 147 148 eqtr2di ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ( 1 ... 𝑁 ) ) )
150 149 52 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
151 150 feq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∪ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) ↔ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) ) )
152 139 151 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) )
153 152 ffnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
154 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1 ... 𝑁 ) ∈ V )
155 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑁 ) = ( 𝑇 ‘ 𝑁 ) )
156 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
157 121 153 154 154 88 155 156 ofval ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝑁 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) )
158 119 157 mpdan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝑁 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) )
159 158 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ( 𝑇 ‘ 𝑁 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) = 0 ) )
160 2 91 ffvelrnd ⊢ ( 𝜑 → ( 𝑇 ‘ 𝑁 ) ∈ ( 0 ..^ 𝐾 ) )
161 elfzonn0 ⊢ ( ( 𝑇 ‘ 𝑁 ) ∈ ( 0 ..^ 𝐾 ) → ( 𝑇 ‘ 𝑁 ) ∈ ℕ0 )
162 160 161 syl ⊢ ( 𝜑 → ( 𝑇 ‘ 𝑁 ) ∈ ℕ0 )
163 162 nn0red ⊢ ( 𝜑 → ( 𝑇 ‘ 𝑁 ) ∈ ℝ )
164 163 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑁 ) ∈ ℝ )
165 162 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑇 ‘ 𝑁 ) )
166 165 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( 𝑇 ‘ 𝑁 ) )
167 1re ⊢ 1 ∈ ℝ
168 snssi ⊢ ( 1 ∈ ℝ → { 1 } ⊆ ℝ )
169 167 168 ax-mp ⊢ { 1 } ⊆ ℝ
170 0re ⊢ 0 ∈ ℝ
171 snssi ⊢ ( 0 ∈ ℝ → { 0 } ⊆ ℝ )
172 170 171 ax-mp ⊢ { 0 } ⊆ ℝ
173 169 172 unssi ⊢ ( { 1 } ∪ { 0 } ) ⊆ ℝ
174 152 119 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ ( { 1 } ∪ { 0 } ) )
175 173 174 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ ℝ )
176 elun ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ ( { 1 } ∪ { 0 } ) ↔ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 1 } ∨ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 0 } ) )
177 0le1 ⊢ 0 ≤ 1
178 elsni ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 1 } → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 1 )
179 177 178 breqtrrid ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 1 } → 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
180 0le0 ⊢ 0 ≤ 0
181 elsni ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 0 } → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
182 180 181 breqtrrid ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 0 } → 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
183 179 182 jaoi ⊢ ( ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 1 } ∨ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ { 0 } ) → 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
184 176 183 sylbi ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ ( { 1 } ∪ { 0 } ) → 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
185 174 184 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
186 add20 ⊢ ( ( ( ( 𝑇 ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝑇 ‘ 𝑁 ) ) ∧ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) ) → ( ( ( 𝑇 ‘ 𝑁 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) = 0 ↔ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
187 164 166 175 185 186 syl22anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑇 ‘ 𝑁 ) + ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ) = 0 ↔ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
188 159 187 bitrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
189 118 188 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
190 189 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
191 190 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑁 ) → ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
192 breq2 ⊢ ( 𝑉 = 𝑁 → ( 𝑦 < 𝑉 ↔ 𝑦 < 𝑁 ) )
193 192 ifbid ⊢ ( 𝑉 = 𝑁 → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑦 < 𝑁 , 𝑦 , ( 𝑦 + 1 ) ) )
194 elfzelz ⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℤ )
195 194 zred ⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ∈ ℝ )
196 195 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 ∈ ℝ )
197 32 nn0red ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
198 197 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
199 25 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
200 elfzle2 ⊢ ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑦 ≤ ( 𝑁 − 1 ) )
201 200 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 ≤ ( 𝑁 − 1 ) )
202 25 ltm1d ⊢ ( 𝜑 → ( 𝑁 − 1 ) < 𝑁 )
203 202 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
204 196 198 199 201 203 lelttrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑦 < 𝑁 )
205 204 iftrued ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < 𝑁 , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
206 193 205 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑉 = 𝑁 ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
207 206 an32s ⊢ ( ( ( 𝜑 ∧ 𝑉 = 𝑁 ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
208 207 csbeq1d ⊢ ( ( ( 𝜑 ∧ 𝑉 = 𝑁 ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
209 208 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑉 = 𝑁 ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) )
210 209 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑉 = 𝑁 ) ∧ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
211 210 ralbidva ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑁 ) → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
212 nfv ⊢ Ⅎ 𝑦 ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0
213 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
214 nfcv ⊢ Ⅎ 𝑗 𝑁
215 213 214 nffv ⊢ Ⅎ 𝑗 ( ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 )
216 215 nfeq1 ⊢ Ⅎ 𝑗 ( ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0
217 csbeq1a ⊢ ( 𝑗 = 𝑦 → ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) = ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) )
218 217 fveq1d ⊢ ( 𝑗 = 𝑦 → ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = ( ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) )
219 218 eqeq1d ⊢ ( 𝑗 = 𝑦 → ( ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
220 212 216 219 cbvralw ⊢ ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ 𝑦 / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 )
221 211 220 bitr4di ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑁 ) → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) )
222 ne0i ⊢ ( ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ≠ ∅ )
223 r19.3rzv ⊢ ( ( 0 ... ( 𝑁 − 1 ) ) ≠ ∅ → ( ( 𝑇 ‘ 𝑁 ) = 0 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑇 ‘ 𝑁 ) = 0 ) )
224 34 222 223 3syl ⊢ ( 𝜑 → ( ( 𝑇 ‘ 𝑁 ) = 0 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑇 ‘ 𝑁 ) = 0 ) )
225 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℤ )
226 225 zred ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℝ )
227 226 ltp1d ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 < ( 𝑗 + 1 ) )
228 227 133 syl ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
229 228 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
230 229 61 eqtrdi ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑈 “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
231 129 230 sylan9req ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
232 231 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
233 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑈 ‘ 𝑁 ) = 𝑁 )
234 f1ofn ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 Fn ( 1 ... 𝑁 ) )
235 3 234 syl ⊢ ( 𝜑 → 𝑈 Fn ( 1 ... 𝑁 ) )
236 235 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑈 Fn ( 1 ... 𝑁 ) )
237 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℕ0 )
238 237 76 syl ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑗 + 1 ) ∈ ℕ )
239 238 142 eleqtrdi ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
240 fzss1 ⊢ ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( 𝑗 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
241 239 240 syl ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑗 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
242 241 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑗 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
243 39 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
244 elfzuz3 ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
245 eluzp1p1 ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) )
246 244 245 syl ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) )
247 246 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) )
248 243 247 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) )
249 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) → 𝑁 ∈ ( ( 𝑗 + 1 ) ... 𝑁 ) )
250 248 249 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( ( 𝑗 + 1 ) ... 𝑁 ) )
251 fnfvima ⊢ ( ( 𝑈 Fn ( 1 ... 𝑁 ) ∧ ( ( 𝑗 + 1 ) ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( ( 𝑗 + 1 ) ... 𝑁 ) ) → ( 𝑈 ‘ 𝑁 ) ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
252 236 242 250 251 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑈 ‘ 𝑁 ) ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
253 252 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑈 ‘ 𝑁 ) ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
254 233 253 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
255 fnconstg ⊢ ( 1 ∈ V → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑗 ) ) )
256 84 255 ax-mp ⊢ ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑗 ) )
257 fnconstg ⊢ ( 0 ∈ V → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
258 123 257 ax-mp ⊢ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) )
259 fvun2 ⊢ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... 𝑗 ) ) ∧ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ∧ ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑁 ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑁 ) )
260 256 258 259 mp3an12 ⊢ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) ∩ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑁 ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑁 ) )
261 232 254 260 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑁 ) )
262 123 fvconst2 ⊢ ( 𝑁 ∈ ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) → ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑁 ) = 0 )
263 254 262 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ‘ 𝑁 ) = 0 )
264 261 263 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
265 264 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) → ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
266 265 ex ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑁 ) = 𝑁 → ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) )
267 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
268 ax-1ne0 ⊢ 1 ≠ 0
269 imain ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) )
270 3 127 269 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) )
271 202 39 breqtrrd ⊢ ( 𝜑 → ( 𝑁 − 1 ) < ( ( 𝑁 − 1 ) + 1 ) )
272 fzdisj ⊢ ( ( 𝑁 − 1 ) < ( ( 𝑁 − 1 ) + 1 ) → ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
273 271 272 syl ⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) = ∅ )
274 273 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ( 𝑈 “ ∅ ) )
275 274 61 eqtrdi ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... ( 𝑁 − 1 ) ) ∩ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
276 270 275 eqtr3d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
277 276 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ )
278 91 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
279 elimasni ⊢ ( 𝑁 ∈ ( 𝑈 “ { 𝑁 } ) → 𝑁 𝑈 𝑁 )
280 fnbrfvb ⊢ ( ( 𝑈 Fn ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑈 ‘ 𝑁 ) = 𝑁 ↔ 𝑁 𝑈 𝑁 ) )
281 235 91 280 syl2anc ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑁 ) = 𝑁 ↔ 𝑁 𝑈 𝑁 ) )
282 279 281 syl5ibr ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑈 “ { 𝑁 } ) → ( 𝑈 ‘ 𝑁 ) = 𝑁 ) )
283 282 necon3ad ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 → ¬ 𝑁 ∈ ( 𝑈 “ { 𝑁 } ) ) )
284 283 imp ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → ¬ 𝑁 ∈ ( 𝑈 “ { 𝑁 } ) )
285 278 284 eldifd ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → 𝑁 ∈ ( ( 1 ... 𝑁 ) ∖ ( 𝑈 “ { 𝑁 } ) ) )
286 imadif ⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) = ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑁 } ) ) )
287 3 127 286 3syl ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) = ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑁 } ) ) )
288 difun2 ⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ∖ { 𝑁 } ) = ( ( 1 ... ( 𝑁 − 1 ) ) ∖ { 𝑁 } )
289 elun ⊢ ( 𝑗 ∈ ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ↔ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 ∈ { 𝑁 } ) )
290 velsn ⊢ ( 𝑗 ∈ { 𝑁 } ↔ 𝑗 = 𝑁 )
291 290 orbi2i ⊢ ( ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 ∈ { 𝑁 } ) ↔ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 = 𝑁 ) )
292 289 291 bitri ⊢ ( 𝑗 ∈ ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ↔ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 = 𝑁 ) )
293 1 142 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
294 fzm1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 = 𝑁 ) ) )
295 293 294 syl ⊢ ( 𝜑 → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑗 = 𝑁 ) ) )
296 292 295 bitr4id ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ↔ 𝑗 ∈ ( 1 ... 𝑁 ) ) )
297 296 eqrdv ⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) = ( 1 ... 𝑁 ) )
298 297 difeq1d ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) ∖ { 𝑁 } ) = ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) )
299 197 25 ltnled ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) < 𝑁 ↔ ¬ 𝑁 ≤ ( 𝑁 − 1 ) ) )
300 202 299 mpbid ⊢ ( 𝜑 → ¬ 𝑁 ≤ ( 𝑁 − 1 ) )
301 elfzle2 ⊢ ( 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑁 ≤ ( 𝑁 − 1 ) )
302 300 301 nsyl ⊢ ( 𝜑 → ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
303 difsn ⊢ ( ¬ 𝑁 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( ( 1 ... ( 𝑁 − 1 ) ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
304 302 303 syl ⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 − 1 ) ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
305 288 298 304 3eqtr3a ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
306 305 imaeq2d ⊢ ( 𝜑 → ( 𝑈 “ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) = ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
307 52 difeq1d ⊢ ( 𝜑 → ( ( 𝑈 “ ( 1 ... 𝑁 ) ) ∖ ( 𝑈 “ { 𝑁 } ) ) = ( ( 1 ... 𝑁 ) ∖ ( 𝑈 “ { 𝑁 } ) ) )
308 287 306 307 3eqtr3rd ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ( 𝑈 “ { 𝑁 } ) ) = ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
309 308 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → ( ( 1 ... 𝑁 ) ∖ ( 𝑈 “ { 𝑁 } ) ) = ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
310 285 309 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → 𝑁 ∈ ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
311 fnconstg ⊢ ( 1 ∈ V → ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
312 84 311 ax-mp ⊢ ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) )
313 fnconstg ⊢ ( 0 ∈ V → ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
314 123 313 ax-mp ⊢ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) )
315 fvun1 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) Fn ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) Fn ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ∧ ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑁 ∈ ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ‘ 𝑁 ) )
316 312 314 315 mp3an12 ⊢ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ∩ ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) ) = ∅ ∧ 𝑁 ∈ ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ‘ 𝑁 ) )
317 277 310 316 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ‘ 𝑁 ) )
318 84 fvconst2 ⊢ ( 𝑁 ∈ ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ‘ 𝑁 ) = 1 )
319 310 318 syl ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ‘ 𝑁 ) = 1 )
320 317 319 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 1 )
321 320 neeq1d ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → ( ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ↔ 1 ≠ 0 ) )
322 268 321 mpbiri ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 )
323 df-ne ⊢ ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ↔ ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
324 oveq2 ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( 1 ... 𝑗 ) = ( 1 ... ( 𝑁 − 1 ) ) )
325 324 imaeq2d ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( 𝑈 “ ( 1 ... 𝑗 ) ) = ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) )
326 325 xpeq1d ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) = ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) )
327 oveq1 ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( 𝑗 + 1 ) = ( ( 𝑁 − 1 ) + 1 ) )
328 327 oveq1d ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( ( 𝑗 + 1 ) ... 𝑁 ) = ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) )
329 328 imaeq2d ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
330 329 xpeq1d ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) = ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) )
331 326 330 uneq12d ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) = ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
332 331 fveq1d ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) )
333 332 neeq1d ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ↔ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ) )
334 323 333 bitr3id ⊢ ( 𝑗 = ( 𝑁 − 1 ) → ( ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ↔ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ) )
335 334 rspcev ⊢ ( ( ( 𝑁 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ ( ( ( ( 𝑈 “ ( 1 ... ( 𝑁 − 1 ) ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) ≠ 0 ) → ∃ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
336 267 322 335 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 ) → ∃ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
337 336 ex ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 → ∃ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) )
338 rexnal ⊢ ( ∃ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ¬ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ↔ ¬ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 )
339 337 338 syl6ib ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑁 ) ≠ 𝑁 → ¬ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) )
340 339 necon4ad ⊢ ( 𝜑 → ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 → ( 𝑈 ‘ 𝑁 ) = 𝑁 ) )
341 266 340 impbid ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑁 ) = 𝑁 ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) )
342 224 341 anbi12d ⊢ ( 𝜑 → ( ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ↔ ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑇 ‘ 𝑁 ) = 0 ∧ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
343 r19.26 ⊢ ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ↔ ( ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝑇 ‘ 𝑁 ) = 0 ∧ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) )
344 342 343 bitr4di ⊢ ( 𝜑 → ( ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
345 344 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑁 ) → ( ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑁 ) = 0 ) ) )
346 191 221 345 3bitr4d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑁 ) → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) )
347 346 pm5.32da ⊢ ( 𝜑 → ( ( 𝑉 = 𝑁 ∧ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ) ↔ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) )
348 110 347 bitrd ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) )
349 348 notbid ⊢ ( 𝜑 → ( ¬ ∀ 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑁 ) = 0 ↔ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) )
350 16 349 syl5bb ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ran ( 𝑦 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↦ ⦋ if ( 𝑦 < 𝑉 , 𝑦 , ( 𝑦 + 1 ) ) / 𝑗 ⦌ ( 𝑇 ∘f + ( ( ( 𝑈 “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( 𝑈 “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ) ( 𝑝 ‘ 𝑁 ) ≠ 0 ↔ ¬ ( 𝑉 = 𝑁 ∧ ( ( 𝑇 ‘ 𝑁 ) = 0 ∧ ( 𝑈 ‘ 𝑁 ) = 𝑁 ) ) ) )