Metamath Proof Explorer

Theorem poimirlem25

Description: Lemma for poimir stating that for a given simplex such that no vertex maps to N , the number of admissible faces is even. (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 ... 𝑁 ) )
poimirlem25.5 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ≠ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
Assertion poimirlem25 ( 𝜑 → 2 ∥ ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 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 poimirlem25.5 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ≠ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
7 neq0 ⊢ ( ¬ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } = ∅ ↔ ∃ 𝑡 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } )
8 2z ⊢ 2 ∈ ℤ
9 iddvds ⊢ ( 2 ∈ ℤ → 2 ∥ 2 )
10 8 9 ax-mp ⊢ 2 ∥ 2
11 df-2 ⊢ 2 = ( 1 + 1 )
12 10 11 breqtri ⊢ 2 ∥ ( 1 + 1 )
13 vex ⊢ 𝑡 ∈ V
14 fzfi ⊢ ( 0 ... 𝑁 ) ∈ Fin
15 rabfi ⊢ ( ( 0 ... 𝑁 ) ∈ Fin → { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∈ Fin )
16 14 15 ax-mp ⊢ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∈ Fin
17 diffi ⊢ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∈ Fin → ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ∈ Fin )
18 16 17 ax-mp ⊢ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ∈ Fin
19 neldifsn ⊢ ¬ 𝑡 ∈ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } )
20 18 19 pm3.2i ⊢ ( ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ∈ Fin ∧ ¬ 𝑡 ∈ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) )
21 hashunsng ⊢ ( 𝑡 ∈ V → ( ( ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ∈ Fin ∧ ¬ 𝑡 ∈ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) → ( ♯ ‘ ( ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ∪ { 𝑡 } ) ) = ( ( ♯ ‘ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) + 1 ) ) )
22 13 20 21 mp2 ⊢ ( ♯ ‘ ( ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ∪ { 𝑡 } ) ) = ( ( ♯ ‘ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) + 1 )
23 difsnid ⊢ ( 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } → ( ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ∪ { 𝑡 } ) = { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } )
24 23 fveq2d ⊢ ( 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } → ( ♯ ‘ ( ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ∪ { 𝑡 } ) ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) )
25 22 24 eqtr3id ⊢ ( 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } → ( ( ♯ ‘ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) + 1 ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) → ( ( ♯ ‘ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) + 1 ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) )
27 sneq ⊢ ( 𝑦 = 𝑡 → { 𝑦 } = { 𝑡 } )
28 27 difeq2d ⊢ ( 𝑦 = 𝑡 → ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) = ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) )
29 28 rexeqdv ⊢ ( 𝑦 = 𝑡 → ( ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
30 29 ralbidv ⊢ ( 𝑦 = 𝑡 → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
31 30 elrab ⊢ ( 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ↔ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
32 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑁 ≠ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
33 nfcv ⊢ Ⅎ 𝑗 𝑁
34 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
35 33 34 nfne ⊢ Ⅎ 𝑗 𝑁 ≠ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
36 csbeq1a ⊢ ( 𝑗 = 𝑡 → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
37 36 neeq2d ⊢ ( 𝑗 = 𝑡 → ( 𝑁 ≠ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑁 ≠ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
38 35 37 rspc ⊢ ( 𝑡 ∈ ( 0 ... 𝑁 ) → ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑁 ≠ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑁 ≠ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
39 32 38 mpan9 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ≠ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
40 nesym ⊢ ( 𝑁 ≠ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 )
41 39 40 sylib ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 )
42 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) )
43 34 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 )
44 42 43 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) )
45 eleq1w ⊢ ( 𝑗 = 𝑡 → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ 𝑡 ∈ ( 0 ... 𝑁 ) ) )
46 45 anbi2d ⊢ ( 𝑗 = 𝑡 → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ) )
47 36 eleq1d ⊢ ( 𝑗 = 𝑡 → ( ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ) )
48 46 47 imbi12d ⊢ ( 𝑗 = 𝑡 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ) ↔ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ) ) )
49 ovex ⊢ ( 0 ..^ 𝐾 ) ∈ V
50 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
51 49 50 elmap ⊢ ( 𝑇 ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ↔ 𝑇 : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
52 4 51 sylibr ⊢ ( 𝜑 → 𝑇 ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
53 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
54 f1oexrnex ⊢ ( ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ( 1 ... 𝑁 ) ∈ Fin ) → 𝑈 ∈ V )
55 53 54 mpan2 ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 ∈ V )
56 f1oeq1 ⊢ ( 𝑓 = 𝑈 → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
57 56 elabg ⊢ ( 𝑈 ∈ V → ( 𝑈 ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
58 55 57 syl ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 𝑈 ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
59 58 ibir ⊢ ( 𝑈 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → 𝑈 ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
60 5 59 syl ⊢ ( 𝜑 → 𝑈 ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
61 opelxpi ⊢ ( ( 𝑇 ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) ∧ 𝑈 ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ⟨ 𝑇 , 𝑈 ⟩ ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
62 52 60 61 syl2anc ⊢ ( 𝜑 → ⟨ 𝑇 , 𝑈 ⟩ ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ⟨ 𝑇 , 𝑈 ⟩ ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
64 nfcv ⊢ Ⅎ 𝑠 ⟨ 𝑇 , 𝑈 ⟩
65 nfv ⊢ Ⅎ 𝑠 ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) )
66 nfcsb1v ⊢ Ⅎ 𝑠 ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
67 66 nfel1 ⊢ Ⅎ 𝑠 ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 )
68 65 67 nfim ⊢ Ⅎ 𝑠 ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) )
69 csbeq1a ⊢ ( 𝑠 = ⟨ 𝑇 , 𝑈 ⟩ → 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
70 69 eleq1d ⊢ ( 𝑠 = ⟨ 𝑇 , 𝑈 ⟩ → ( 𝐶 ∈ ( 0 ... 𝑁 ) ↔ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ) )
71 70 imbi2d ⊢ ( 𝑠 = ⟨ 𝑇 , 𝑈 ⟩ → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ∈ ( 0 ... 𝑁 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ) ) )
72 elun ⊢ ( 𝑝 ∈ ( { 1 } ∪ { 0 } ) ↔ ( 𝑝 ∈ { 1 } ∨ 𝑝 ∈ { 0 } ) )
73 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝐾 ) )
74 elsni ⊢ ( 𝑝 ∈ { 1 } → 𝑝 = 1 )
75 74 oveq2d ⊢ ( 𝑝 ∈ { 1 } → ( 𝑖 + 𝑝 ) = ( 𝑖 + 1 ) )
76 75 eleq1d ⊢ ( 𝑝 ∈ { 1 } → ( ( 𝑖 + 𝑝 ) ∈ ( 0 ... 𝐾 ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... 𝐾 ) ) )
77 73 76 syl5ibrcom ⊢ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) → ( 𝑝 ∈ { 1 } → ( 𝑖 + 𝑝 ) ∈ ( 0 ... 𝐾 ) ) )
78 elfzonn0 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) → 𝑖 ∈ ℕ0 )
79 78 nn0cnd ⊢ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) → 𝑖 ∈ ℂ )
80 79 addid1d ⊢ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) → ( 𝑖 + 0 ) = 𝑖 )
81 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) → 𝑖 ∈ ( 0 ... 𝐾 ) )
82 80 81 eqeltrd ⊢ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) → ( 𝑖 + 0 ) ∈ ( 0 ... 𝐾 ) )
83 elsni ⊢ ( 𝑝 ∈ { 0 } → 𝑝 = 0 )
84 83 oveq2d ⊢ ( 𝑝 ∈ { 0 } → ( 𝑖 + 𝑝 ) = ( 𝑖 + 0 ) )
85 84 eleq1d ⊢ ( 𝑝 ∈ { 0 } → ( ( 𝑖 + 𝑝 ) ∈ ( 0 ... 𝐾 ) ↔ ( 𝑖 + 0 ) ∈ ( 0 ... 𝐾 ) ) )
86 82 85 syl5ibrcom ⊢ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) → ( 𝑝 ∈ { 0 } → ( 𝑖 + 𝑝 ) ∈ ( 0 ... 𝐾 ) ) )
87 77 86 jaod ⊢ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) → ( ( 𝑝 ∈ { 1 } ∨ 𝑝 ∈ { 0 } ) → ( 𝑖 + 𝑝 ) ∈ ( 0 ... 𝐾 ) ) )
88 72 87 syl5bi ⊢ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) → ( 𝑝 ∈ ( { 1 } ∪ { 0 } ) → ( 𝑖 + 𝑝 ) ∈ ( 0 ... 𝐾 ) ) )
89 88 imp ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝐾 ) ∧ 𝑝 ∈ ( { 1 } ∪ { 0 } ) ) → ( 𝑖 + 𝑝 ) ∈ ( 0 ... 𝐾 ) )
90 89 adantl ⊢ ( ( ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑖 ∈ ( 0 ..^ 𝐾 ) ∧ 𝑝 ∈ ( { 1 } ∪ { 0 } ) ) ) → ( 𝑖 + 𝑝 ) ∈ ( 0 ... 𝐾 ) )
91 xp1st ⊢ ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ 𝑠 ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) )
92 elmapi ⊢ ( ( 1st ‘ 𝑠 ) ∈ ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) → ( 1st ‘ 𝑠 ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
93 91 92 syl ⊢ ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ 𝑠 ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
94 93 adantr ⊢ ( ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1st ‘ 𝑠 ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝐾 ) )
95 xp2nd ⊢ ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2nd ‘ 𝑠 ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
96 fvex ⊢ ( 2nd ‘ 𝑠 ) ∈ V
97 f1oeq1 ⊢ ( 𝑓 = ( 2nd ‘ 𝑠 ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
98 96 97 elab ⊢ ( ( 2nd ‘ 𝑠 ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
99 95 98 sylib ⊢ ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
100 1ex ⊢ 1 ∈ V
101 100 fconst ⊢ ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ⟶ { 1 }
102 c0ex ⊢ 0 ∈ V
103 102 fconst ⊢ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 }
104 101 103 pm3.2i ⊢ ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } )
105 dff1o3 ⊢ ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ◡ ( 2nd ‘ 𝑠 ) ) )
106 imain ⊢ ( Fun ◡ ( 2nd ‘ 𝑠 ) → ( ( 2nd ‘ 𝑠 ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
107 105 106 simplbiim ⊢ ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( ( 2nd ‘ 𝑠 ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
108 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℕ0 )
109 108 nn0red ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℝ )
110 109 ltp1d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 < ( 𝑗 + 1 ) )
111 fzdisj ⊢ ( 𝑗 < ( 𝑗 + 1 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
112 110 111 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
113 112 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 2nd ‘ 𝑠 ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 2nd ‘ 𝑠 ) “ ∅ ) )
114 ima0 ⊢ ( ( 2nd ‘ 𝑠 ) “ ∅ ) = ∅
115 113 114 eqtrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 2nd ‘ 𝑠 ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
116 107 115 sylan9req ⊢ ( ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
117 fun ⊢ ( ( ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } ) ∧ ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
118 104 116 117 sylancr ⊢ ( ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
119 nn0p1nn ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ )
120 108 119 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ℕ )
121 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
122 120 121 eleqtrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
123 elfzuz3 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) )
124 fzsplit2 ⊢ ( ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
125 122 123 124 syl2anc ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
126 125 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑁 ) ) = ( ( 2nd ‘ 𝑠 ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
127 imaundi ⊢ ( ( 2nd ‘ 𝑠 ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
128 126 127 eqtr2di ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑁 ) ) )
129 f1ofo ⊢ ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
130 foima ⊢ ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
131 129 130 syl ⊢ ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
132 128 131 sylan9eqr ⊢ ( ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
133 132 feq2d ⊢ ( ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) ↔ ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) ) )
134 118 133 mpbid ⊢ ( ( ( 2nd ‘ 𝑠 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) )
135 99 134 sylan ⊢ ( ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) )
136 fzfid ⊢ ( ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1 ... 𝑁 ) ∈ Fin )
137 inidm ⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
138 90 94 135 136 136 137 off ⊢ ( ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) )
139 ovex ⊢ ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∈ V
140 feq1 ⊢ ( 𝑝 = ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( 𝑝 : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ↔ ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) )
141 140 anbi2d ⊢ ( 𝑝 = ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( ( 𝜑 ∧ 𝑝 : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) ↔ ( 𝜑 ∧ ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) ) )
142 2 eleq1d ⊢ ( 𝑝 = ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( 𝐵 ∈ ( 0 ... 𝑁 ) ↔ 𝐶 ∈ ( 0 ... 𝑁 ) ) )
143 141 142 imbi12d ⊢ ( 𝑝 = ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) → ( ( ( 𝜑 ∧ 𝑝 : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) → 𝐵 ∈ ( 0 ... 𝑁 ) ) ↔ ( ( 𝜑 ∧ ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) → 𝐶 ∈ ( 0 ... 𝑁 ) ) ) )
144 139 143 3 vtocl ⊢ ( ( 𝜑 ∧ ( ( 1st ‘ 𝑠 ) ∘f + ( ( ( ( 2nd ‘ 𝑠 ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ 𝑠 ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝐾 ) ) → 𝐶 ∈ ( 0 ... 𝑁 ) )
145 138 144 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ) → 𝐶 ∈ ( 0 ... 𝑁 ) )
146 145 an12s ⊢ ( ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) ∧ ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ) → 𝐶 ∈ ( 0 ... 𝑁 ) )
147 146 ex ⊢ ( 𝑠 ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ∈ ( 0 ... 𝑁 ) ) )
148 64 68 71 147 vtoclgaf ⊢ ( ⟨ 𝑇 , 𝑈 ⟩ ∈ ( ( ( 0 ..^ 𝐾 ) ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ) )
149 63 148 mpcom ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) )
150 44 48 149 chvarfv ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) )
151 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
152 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
153 151 152 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
154 fzm1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ↔ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 ) ) )
155 153 154 syl ⊢ ( 𝜑 → ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ↔ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 ) ) )
156 155 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ↔ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 ) ) )
157 150 156 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 ) )
158 157 ord ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ( ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 ) )
159 41 158 mt3d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
160 159 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
161 fzfi ⊢ ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin
162 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
163 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
164 162 163 163 addsubd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = ( ( 𝑁 − 1 ) + 1 ) )
165 hashfz0 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝑁 ) ) = ( 𝑁 + 1 ) )
166 151 165 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... 𝑁 ) ) = ( 𝑁 + 1 ) )
167 166 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ... 𝑁 ) ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
168 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
169 hashfz0 ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ( 𝑁 − 1 ) + 1 ) )
170 1 168 169 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ( 𝑁 − 1 ) + 1 ) )
171 164 167 170 3eqtr4rd ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ( ♯ ‘ ( 0 ... 𝑁 ) ) − 1 ) )
172 hashdifsn ⊢ ( ( ( 0 ... 𝑁 ) ∈ Fin ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ( ♯ ‘ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) = ( ( ♯ ‘ ( 0 ... 𝑁 ) ) − 1 ) )
173 14 172 mpan ⊢ ( 𝑡 ∈ ( 0 ... 𝑁 ) → ( ♯ ‘ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) = ( ( ♯ ‘ ( 0 ... 𝑁 ) ) − 1 ) )
174 173 eqcomd ⊢ ( 𝑡 ∈ ( 0 ... 𝑁 ) → ( ( ♯ ‘ ( 0 ... 𝑁 ) ) − 1 ) = ( ♯ ‘ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) )
175 171 174 sylan9eq ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ♯ ‘ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) )
176 diffi ⊢ ( ( 0 ... 𝑁 ) ∈ Fin → ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∈ Fin )
177 14 176 ax-mp ⊢ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∈ Fin
178 hashen ⊢ ( ( ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin ∧ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∈ Fin ) → ( ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ♯ ‘ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ↔ ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) )
179 161 177 178 mp2an ⊢ ( ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ♯ ‘ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ↔ ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) )
180 175 179 sylib ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) )
181 phpreu ⊢ ( ( ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin ∧ ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
182 161 180 181 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
183 182 biimpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
184 183 impr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) → ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
185 nfv ⊢ Ⅎ 𝑧 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
186 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
187 186 nfeq2 ⊢ Ⅎ 𝑗 𝑖 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
188 csbeq1a ⊢ ( 𝑗 = 𝑧 → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
189 188 eqeq2d ⊢ ( 𝑗 = 𝑧 → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
190 185 187 189 cbvreuw ⊢ ( ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
191 eqeq1 ⊢ ( 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( 𝑖 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
192 191 reubidv ⊢ ( 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
193 190 192 syl5bb ⊢ ( 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
194 193 rspcv ⊢ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
195 160 184 194 sylc ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) → ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
196 an32 ⊢ ( ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ↔ ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
197 196 biimpi ⊢ ( ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) → ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
198 197 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) → ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
199 eqeq2 ⊢ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
200 rexsns ⊢ ( ∃ 𝑗 ∈ { 𝑡 } 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ [ 𝑡 / 𝑗 ] 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
201 34 nfeq2 ⊢ Ⅎ 𝑗 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
202 36 eqeq2d ⊢ ( 𝑗 = 𝑡 → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
203 201 202 sbciegf ⊢ ( 𝑡 ∈ V → ( [ 𝑡 / 𝑗 ] 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
204 13 203 ax-mp ⊢ ( [ 𝑡 / 𝑗 ] 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
205 200 204 bitri ⊢ ( ∃ 𝑗 ∈ { 𝑡 } 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
206 rexsns ⊢ ( ∃ 𝑗 ∈ { 𝑧 } 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ [ 𝑧 / 𝑗 ] 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
207 vex ⊢ 𝑧 ∈ V
208 187 189 sbciegf ⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑗 ] 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
209 207 208 ax-mp ⊢ ( [ 𝑧 / 𝑗 ] 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
210 206 209 bitri ⊢ ( ∃ 𝑗 ∈ { 𝑧 } 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ 𝑖 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
211 199 205 210 3bitr4g ⊢ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( ∃ 𝑗 ∈ { 𝑡 } 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ { 𝑧 } 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
212 211 orbi1d ⊢ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( ( ∃ 𝑗 ∈ { 𝑡 } 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∨ ∃ 𝑗 ∈ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ( ∃ 𝑗 ∈ { 𝑧 } 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∨ ∃ 𝑗 ∈ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
213 rexun ⊢ ( ∃ 𝑗 ∈ ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ( ∃ 𝑗 ∈ { 𝑡 } 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∨ ∃ 𝑗 ∈ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
214 rexun ⊢ ( ∃ 𝑗 ∈ ( { 𝑧 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ( ∃ 𝑗 ∈ { 𝑧 } 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∨ ∃ 𝑗 ∈ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
215 212 213 214 3bitr4g ⊢ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( ∃ 𝑗 ∈ ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( { 𝑧 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
216 215 adantl ⊢ ( ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ( ∃ 𝑗 ∈ ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( { 𝑧 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
217 eldifsni ⊢ ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) → 𝑧 ≠ 𝑡 )
218 217 necomd ⊢ ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) → 𝑡 ≠ 𝑧 )
219 dif32 ⊢ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) = ( ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∖ { 𝑡 } )
220 219 uneq2i ⊢ ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) = ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∖ { 𝑡 } ) )
221 snssi ⊢ ( 𝑡 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) → { 𝑡 } ⊆ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
222 eldifsn ⊢ ( 𝑡 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ↔ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ≠ 𝑧 ) )
223 undif ⊢ ( { 𝑡 } ⊆ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ↔ ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∖ { 𝑡 } ) ) = ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
224 221 222 223 3imtr3i ⊢ ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ≠ 𝑧 ) → ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∖ { 𝑡 } ) ) = ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
225 220 224 syl5eq ⊢ ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ≠ 𝑧 ) → ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) = ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
226 218 225 sylan2 ⊢ ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) → ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) = ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
227 226 rexeqdv ⊢ ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) → ( ∃ 𝑗 ∈ ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
228 227 adantr ⊢ ( ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ( ∃ 𝑗 ∈ ( { 𝑡 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
229 snssi ⊢ ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) → { 𝑧 } ⊆ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) )
230 undif ⊢ ( { 𝑧 } ⊆ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ↔ ( { 𝑧 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) = ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) )
231 229 230 sylib ⊢ ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) → ( { 𝑧 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) = ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) )
232 231 rexeqdv ⊢ ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) → ( ∃ 𝑗 ∈ ( { 𝑧 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
233 232 ad2antlr ⊢ ( ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ( ∃ 𝑗 ∈ ( { 𝑧 } ∪ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
234 216 228 233 3bitr3d ⊢ ( ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ( ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
235 234 ralbidv ⊢ ( ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
236 235 biimpar ⊢ ( ( ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
237 236 an32s ⊢ ( ( ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
238 198 237 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
239 simpl ⊢ ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → 𝑡 ∈ ( 0 ... 𝑁 ) )
240 239 anim2i ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) → ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) )
241 necom ⊢ ( 𝑧 ≠ 𝑡 ↔ 𝑡 ≠ 𝑧 )
242 241 biimpi ⊢ ( 𝑧 ≠ 𝑡 → 𝑡 ≠ 𝑧 )
243 242 adantl ⊢ ( ( 𝑧 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ≠ 𝑡 ) → 𝑡 ≠ 𝑧 )
244 243 anim2i ⊢ ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑧 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ≠ 𝑡 ) ) → ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ≠ 𝑧 ) )
245 eldifsn ⊢ ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ↔ ( 𝑧 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ≠ 𝑡 ) )
246 245 anbi2i ⊢ ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ↔ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑧 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ≠ 𝑡 ) ) )
247 244 246 222 3imtr4i ⊢ ( ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) → 𝑡 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
248 247 adantll ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) → 𝑡 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
249 248 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → 𝑡 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
250 34 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) )
251 42 250 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
252 36 eleq1d ⊢ ( 𝑗 = 𝑡 → ( ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
253 46 252 imbi12d ⊢ ( 𝑗 = 𝑡 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ) )
254 6 necomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ≠ 𝑁 )
255 254 neneqd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ¬ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 )
256 fzm1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ↔ ( ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 ) ) )
257 153 256 syl ⊢ ( 𝜑 → ( ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ↔ ( ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 ) ) )
258 257 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... 𝑁 ) ↔ ( ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 ) ) )
259 149 258 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 ) )
260 259 ord ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ¬ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = 𝑁 ) )
261 255 260 mt3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
262 251 253 261 chvarfv ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
263 262 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
264 eldifi ⊢ ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) → 𝑧 ∈ ( 0 ... 𝑁 ) )
265 eleq1w ⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∈ ( 0 ... 𝑁 ) ↔ 𝑧 ∈ ( 0 ... 𝑁 ) ) )
266 265 anbi2d ⊢ ( 𝑡 = 𝑧 → ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑧 ∈ ( 0 ... 𝑁 ) ) ) )
267 sneq ⊢ ( 𝑡 = 𝑧 → { 𝑡 } = { 𝑧 } )
268 267 difeq2d ⊢ ( 𝑡 = 𝑧 → ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) = ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
269 268 breq2d ⊢ ( 𝑡 = 𝑧 → ( ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ↔ ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ) )
270 266 269 imbi12d ⊢ ( 𝑡 = 𝑧 → ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ↔ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 ... 𝑁 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ) ) )
271 270 180 chvarvv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 0 ... 𝑁 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
272 264 271 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
273 272 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
274 phpreu ⊢ ( ( ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin ∧ ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ) → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
275 161 274 mpan ⊢ ( ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
276 275 biimpa ⊢ ( ( ( 0 ... ( 𝑁 − 1 ) ) ≈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
277 273 276 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
278 eqeq1 ⊢ ( 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
279 278 adantr ⊢ ( ( 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ) → ( 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
280 201 279 reubida ⊢ ( 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
281 280 rspcv ⊢ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
282 263 277 281 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
283 reurmo ⊢ ( ∃! 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃* 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
284 282 283 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃* 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
285 nfv ⊢ Ⅎ 𝑖 ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
286 285 rmo3 ⊢ ( ∃* 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∀ 𝑖 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → 𝑗 = 𝑖 ) )
287 284 286 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∀ 𝑖 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → 𝑗 = 𝑖 ) )
288 equcomi ⊢ ( 𝑖 = 𝑡 → 𝑡 = 𝑖 )
289 288 csbeq1d ⊢ ( 𝑖 = 𝑡 → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑖 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
290 sbsbc ⊢ ( [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
291 vex ⊢ 𝑖 ∈ V
292 sbceqg ⊢ ( 𝑖 ∈ V → ( [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ⦋ 𝑖 / 𝑗 ⦌ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑖 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
293 34 csbconstgf ⊢ ( 𝑖 ∈ V → ⦋ 𝑖 / 𝑗 ⦌ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
294 293 eqeq1d ⊢ ( 𝑖 ∈ V → ( ⦋ 𝑖 / 𝑗 ⦌ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑖 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑖 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
295 292 294 bitrd ⊢ ( 𝑖 ∈ V → ( [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑖 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
296 291 295 ax-mp ⊢ ( [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑖 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
297 290 296 bitri ⊢ ( [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑖 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
298 289 297 sylibr ⊢ ( 𝑖 = 𝑡 → [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
299 298 biantrud ⊢ ( 𝑖 = 𝑡 → ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
300 299 bicomd ⊢ ( 𝑖 = 𝑡 → ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
301 eqeq2 ⊢ ( 𝑖 = 𝑡 → ( 𝑗 = 𝑖 ↔ 𝑗 = 𝑡 ) )
302 300 301 imbi12d ⊢ ( 𝑖 = 𝑡 → ( ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → 𝑗 = 𝑖 ) ↔ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑡 ) ) )
303 302 rspcv ⊢ ( 𝑡 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) → ( ∀ 𝑖 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → 𝑗 = 𝑖 ) → ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑡 ) ) )
304 303 ralimdv ⊢ ( 𝑡 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) → ( ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∀ 𝑖 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∧ [ 𝑖 / 𝑗 ] ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → 𝑗 = 𝑖 ) → ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑡 ) ) )
305 249 287 304 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑡 ) )
306 dif32 ⊢ ( ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∖ { 𝑡 } ) = ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } )
307 306 eleq2i ⊢ ( 𝑗 ∈ ( ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∖ { 𝑡 } ) ↔ 𝑗 ∈ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) )
308 eldifsn ⊢ ( 𝑗 ∈ ( ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∖ { 𝑡 } ) ↔ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∧ 𝑗 ≠ 𝑡 ) )
309 eldifsn ⊢ ( 𝑗 ∈ ( ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∖ { 𝑧 } ) ↔ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∧ 𝑗 ≠ 𝑧 ) )
310 307 308 309 3bitr3ri ⊢ ( ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∧ 𝑗 ≠ 𝑧 ) ↔ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∧ 𝑗 ≠ 𝑡 ) )
311 310 imbi1i ⊢ ( ( ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∧ 𝑗 ≠ 𝑧 ) → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ( ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∧ 𝑗 ≠ 𝑡 ) → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
312 impexp ⊢ ( ( ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∧ 𝑗 ≠ 𝑧 ) → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) → ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
313 impexp ⊢ ( ( ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ∧ 𝑗 ≠ 𝑡 ) → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) → ( 𝑗 ≠ 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
314 311 312 313 3bitr3ri ⊢ ( ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) → ( 𝑗 ≠ 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) ↔ ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) → ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
315 314 albii ⊢ ( ∀ 𝑗 ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) → ( 𝑗 ≠ 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) ↔ ∀ 𝑗 ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) → ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
316 con34b ⊢ ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑡 ) ↔ ( ¬ 𝑗 = 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
317 df-ne ⊢ ( 𝑗 ≠ 𝑡 ↔ ¬ 𝑗 = 𝑡 )
318 317 imbi1i ⊢ ( ( 𝑗 ≠ 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ( ¬ 𝑗 = 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
319 316 318 bitr4i ⊢ ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑡 ) ↔ ( 𝑗 ≠ 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
320 319 ralbii ⊢ ( ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑡 ) ↔ ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( 𝑗 ≠ 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
321 df-ral ⊢ ( ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( 𝑗 ≠ 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ∀ 𝑗 ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) → ( 𝑗 ≠ 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
322 320 321 bitri ⊢ ( ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑡 ) ↔ ∀ 𝑗 ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) → ( 𝑗 ≠ 𝑡 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
323 df-ral ⊢ ( ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ∀ 𝑗 ( 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) → ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
324 315 322 323 3bitr4i ⊢ ( ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑡 ) ↔ ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
325 305 324 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
326 df-ne ⊢ ( 𝑗 ≠ 𝑧 ↔ ¬ 𝑗 = 𝑧 )
327 326 imbi1i ⊢ ( ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ( ¬ 𝑗 = 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
328 con34b ⊢ ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑧 ) ↔ ( ¬ 𝑗 = 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
329 327 328 bitr4i ⊢ ( ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑧 ) )
330 ancr ⊢ ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → 𝑗 = 𝑧 ) → ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
331 329 330 sylbi ⊢ ( ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
332 331 ralimi ⊢ ( ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( 𝑗 ≠ 𝑧 → ¬ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
333 325 332 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
334 240 333 sylanl1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
335 201 278 rexbid ⊢ ( 𝑖 = ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
336 335 rspcva ⊢ ( ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
337 262 336 sylan ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 ... 𝑁 ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
338 337 anasss ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
339 338 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
340 rexim ⊢ ( ∀ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) → ( ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) )
341 334 339 340 sylc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
342 rexex ⊢ ( ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃ 𝑗 ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
343 341 342 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ∃ 𝑗 ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
344 34 186 nfeq ⊢ Ⅎ 𝑗 ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶
345 188 eqeq2d ⊢ ( 𝑗 = 𝑧 → ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
346 344 345 equsexv ⊢ ( ∃ 𝑗 ( 𝑗 = 𝑧 ∧ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
347 343 346 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) → ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
348 238 347 impbida ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) ∧ 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ) → ( ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
349 348 reubidva ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) → ( ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ⦋ 𝑡 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 = ⦋ 𝑧 / 𝑗 ⦌ ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
350 195 349 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) → ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 )
351 an32 ⊢ ( ( ( 𝑧 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ≠ 𝑡 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ( ( 𝑧 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ∧ 𝑧 ≠ 𝑡 ) )
352 245 anbi1i ⊢ ( ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ( ( 𝑧 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ≠ 𝑡 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
353 sneq ⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
354 353 difeq2d ⊢ ( 𝑦 = 𝑧 → ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) = ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) )
355 354 rexeqdv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
356 355 ralbidv ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
357 356 elrab ⊢ ( 𝑧 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ↔ ( 𝑧 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
358 357 anbi1i ⊢ ( ( 𝑧 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∧ 𝑧 ≠ 𝑡 ) ↔ ( ( 𝑧 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ∧ 𝑧 ≠ 𝑡 ) )
359 351 352 358 3bitr4i ⊢ ( ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ( 𝑧 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∧ 𝑧 ≠ 𝑡 ) )
360 eldifsn ⊢ ( 𝑧 ∈ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ↔ ( 𝑧 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∧ 𝑧 ≠ 𝑡 ) )
361 359 360 bitr4i ⊢ ( ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ 𝑧 ∈ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) )
362 361 eubii ⊢ ( ∃! 𝑧 ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ↔ ∃! 𝑧 𝑧 ∈ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) )
363 df-reu ⊢ ( ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ∃! 𝑧 ( 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) )
364 euhash1 ⊢ ( ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ∈ Fin → ( ( ♯ ‘ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) = 1 ↔ ∃! 𝑧 𝑧 ∈ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) )
365 18 364 ax-mp ⊢ ( ( ♯ ‘ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) = 1 ↔ ∃! 𝑧 𝑧 ∈ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) )
366 362 363 365 3bitr4i ⊢ ( ∃! 𝑧 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑧 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ↔ ( ♯ ‘ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) = 1 )
367 350 366 sylib ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑡 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 ) ) → ( ♯ ‘ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) = 1 )
368 31 367 sylan2b ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) → ( ♯ ‘ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) = 1 )
369 368 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) → ( ( ♯ ‘ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ∖ { 𝑡 } ) ) + 1 ) = ( 1 + 1 ) )
370 26 369 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) → ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) = ( 1 + 1 ) )
371 12 370 breqtrrid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) → 2 ∥ ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) )
372 371 ex ⊢ ( 𝜑 → ( 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } → 2 ∥ ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) ) )
373 372 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑡 𝑡 ∈ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } → 2 ∥ ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) ) )
374 7 373 syl5bi ⊢ ( 𝜑 → ( ¬ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } = ∅ → 2 ∥ ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) ) )
375 dvds0 ⊢ ( 2 ∈ ℤ → 2 ∥ 0 )
376 8 375 ax-mp ⊢ 2 ∥ 0
377 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
378 376 377 breqtrri ⊢ 2 ∥ ( ♯ ‘ ∅ )
379 fveq2 ⊢ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } = ∅ → ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) = ( ♯ ‘ ∅ ) )
380 378 379 breqtrrid ⊢ ( { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } = ∅ → 2 ∥ ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) )
381 374 380 pm2.61d2 ⊢ ( 𝜑 → 2 ∥ ( ♯ ‘ { 𝑦 ∈ ( 0 ... 𝑁 ) ∣ ∀ 𝑖 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∃ 𝑗 ∈ ( ( 0 ... 𝑁 ) ∖ { 𝑦 } ) 𝑖 = ⦋ ⟨ 𝑇 , 𝑈 ⟩ / 𝑠 ⦌ 𝐶 } ) )