Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem25 Structured version   Visualization version   GIF version

Theorem poimirlem25 33760
Description: Lemma for poimir 33768 stating that for a given simplex such that no vertex maps to 𝑁, the number of admissible faces is even. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem28.1 (𝑝 = ((1st𝑠) ∘𝑓 + ((((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
Ref Expression
poimirlem25 (𝜑 → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
Distinct variable groups:   𝑖,𝑗,𝑝,𝑠,𝑦,𝜑   𝑗,𝑁,𝑦   𝑇,𝑗,𝑦   𝑈,𝑗,𝑦   𝜑,𝑖,𝑝,𝑠   𝐵,𝑖,𝑗,𝑠   𝑖,𝐾,𝑗,𝑝,𝑠   𝑖,𝑁,𝑝,𝑠   𝑇,𝑖,𝑝   𝑈,𝑖,𝑝   𝑇,𝑠   𝑦,𝐵   𝐶,𝑖,𝑝,𝑦   𝑦,𝐾   𝑈,𝑠
Allowed substitution hints:   𝐵(𝑝)   𝐶(𝑗,𝑠)

Proof of Theorem poimirlem25
Dummy variables 𝑓 𝑡 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neq0 4075 . . 3 (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ ↔ ∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})
2 2z 11610 . . . . . . . 8 2 ∈ ℤ
3 iddvds 15203 . . . . . . . 8 (2 ∈ ℤ → 2 ∥ 2)
42, 3ax-mp 5 . . . . . . 7 2 ∥ 2
5 df-2 11280 . . . . . . 7 2 = (1 + 1)
64, 5breqtri 4809 . . . . . 6 2 ∥ (1 + 1)
7 vex 3352 . . . . . . . . . 10 𝑡 ∈ V
8 fzfi 12978 . . . . . . . . . . . . 13 (0...𝑁) ∈ Fin
9 rabfi 8340 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin → {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin)
108, 9ax-mp 5 . . . . . . . . . . . 12 {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin
11 diffi 8347 . . . . . . . . . . . 12 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin → ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin)
1210, 11ax-mp 5 . . . . . . . . . . 11 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin
13 neldifsn 4456 . . . . . . . . . . 11 ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})
1412, 13pm3.2i 447 . . . . . . . . . 10 (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin ∧ ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
15 hashunsng 13382 . . . . . . . . . 10 (𝑡 ∈ V → ((({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin ∧ ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) → (♯‘(({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡})) = ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1)))
167, 14, 15mp2 9 . . . . . . . . 9 (♯‘(({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡})) = ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1)
17 difsnid 4474 . . . . . . . . . 10 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡}) = {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})
1817fveq2d 6336 . . . . . . . . 9 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → (♯‘(({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡})) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
1916, 18syl5eqr 2818 . . . . . . . 8 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
2019adantl 467 . . . . . . 7 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
21 sneq 4324 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → {𝑦} = {𝑡})
2221difeq2d 3877 . . . . . . . . . . . 12 (𝑦 = 𝑡 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑡}))
2322rexeqdv 3293 . . . . . . . . . . 11 (𝑦 = 𝑡 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
2423ralbidv 3134 . . . . . . . . . 10 (𝑦 = 𝑡 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
2524elrab 3513 . . . . . . . . 9 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ↔ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
26 poimirlem25.5 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑁𝑇, 𝑈⟩ / 𝑠𝐶)
2726ralrimiva 3114 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑗 ∈ (0...𝑁)𝑁𝑇, 𝑈⟩ / 𝑠𝐶)
28 nfcv 2912 . . . . . . . . . . . . . . . . . 18 𝑗𝑁
29 nfcsb1v 3696 . . . . . . . . . . . . . . . . . 18 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
3028, 29nfne 3042 . . . . . . . . . . . . . . . . 17 𝑗 𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
31 csbeq1a 3689 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
3231neeq2d 3002 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑡 → (𝑁𝑇, 𝑈⟩ / 𝑠𝐶𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
3330, 32rspc 3452 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0...𝑁) → (∀𝑗 ∈ (0...𝑁)𝑁𝑇, 𝑈⟩ / 𝑠𝐶𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
3427, 33mpan9 490 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
35 nesym 2998 . . . . . . . . . . . . . . 15 (𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
3634, 35sylib 208 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
37 nfv 1994 . . . . . . . . . . . . . . . . . 18 𝑗(𝜑𝑡 ∈ (0...𝑁))
3829nfel1 2927 . . . . . . . . . . . . . . . . . 18 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)
3937, 38nfim 1976 . . . . . . . . . . . . . . . . 17 𝑗((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
40 eleq1w 2832 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑡 → (𝑗 ∈ (0...𝑁) ↔ 𝑡 ∈ (0...𝑁)))
4140anbi2d 606 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡 → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡 ∈ (0...𝑁))))
4231eleq1d 2834 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
4341, 42imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑡 → (((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)) ↔ ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))))
44 poimirlem25.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
45 ovex 6822 . . . . . . . . . . . . . . . . . . . . . 22 (0..^𝐾) ∈ V
46 ovex 6822 . . . . . . . . . . . . . . . . . . . . . 22 (1...𝑁) ∈ V
4745, 46elmap 8037 . . . . . . . . . . . . . . . . . . . . 21 (𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) ↔ 𝑇:(1...𝑁)⟶(0..^𝐾))
4844, 47sylibr 224 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
49 poimirlem25.4 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
50 fzfi 12978 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑁) ∈ Fin
51 f1oexrnex 7261 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ Fin) → 𝑈 ∈ V)
5250, 51mpan2 663 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ V)
53 f1oeq1 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑈 → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)))
5453elabg 3500 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈 ∈ V → (𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)))
5552, 54syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → (𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)))
5655ibir 257 . . . . . . . . . . . . . . . . . . . . 21 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
5749, 56syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
58 opelxpi 5288 . . . . . . . . . . . . . . . . . . . 20 ((𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) ∧ 𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
5948, 57, 58syl2anc 565 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
6059adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
61 nfcv 2912 . . . . . . . . . . . . . . . . . . 19 𝑠𝑇, 𝑈
62 nfv 1994 . . . . . . . . . . . . . . . . . . . 20 𝑠(𝜑𝑗 ∈ (0...𝑁))
63 nfcsb1v 3696 . . . . . . . . . . . . . . . . . . . . 21 𝑠𝑇, 𝑈⟩ / 𝑠𝐶
6463nfel1 2927 . . . . . . . . . . . . . . . . . . . 20 𝑠𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)
6562, 64nfim 1976 . . . . . . . . . . . . . . . . . . 19 𝑠((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
66 csbeq1a 3689 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ⟨𝑇, 𝑈⟩ → 𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
6766eleq1d 2834 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ⟨𝑇, 𝑈⟩ → (𝐶 ∈ (0...𝑁) ↔ 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
6867imbi2d 329 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ⟨𝑇, 𝑈⟩ → (((𝜑𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁)) ↔ ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))))
69 elun 3902 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 ∈ ({1} ∪ {0}) ↔ (𝑝 ∈ {1} ∨ 𝑝 ∈ {0}))
70 fzofzp1 12772 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝐾) → (𝑖 + 1) ∈ (0...𝐾))
71 elsni 4331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ {1} → 𝑝 = 1)
7271oveq2d 6808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ {1} → (𝑖 + 𝑝) = (𝑖 + 1))
7372eleq1d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ {1} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 1) ∈ (0...𝐾)))
7470, 73syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {1} → (𝑖 + 𝑝) ∈ (0...𝐾)))
75 elfzonn0 12720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℕ0)
7675nn0cnd 11554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℂ)
7776addid1d 10437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) = 𝑖)
78 elfzofz 12692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ (0...𝐾))
7977, 78eqeltrd 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) ∈ (0...𝐾))
80 elsni 4331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ {0} → 𝑝 = 0)
8180oveq2d 6808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ {0} → (𝑖 + 𝑝) = (𝑖 + 0))
8281eleq1d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ {0} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 0) ∈ (0...𝐾)))
8379, 82syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {0} → (𝑖 + 𝑝) ∈ (0...𝐾)))
8474, 83jaod 839 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝐾) → ((𝑝 ∈ {1} ∨ 𝑝 ∈ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾)))
8569, 84syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ ({1} ∪ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾)))
8685imp 393 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0})) → (𝑖 + 𝑝) ∈ (0...𝐾))
8786adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0}))) → (𝑖 + 𝑝) ∈ (0...𝐾))
88 xp1st 7346 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
89 elmapi 8030 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑠) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
9190adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
92 xp2nd 7347 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd𝑠) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
93 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (2nd𝑠) ∈ V
94 f1oeq1 6268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = (2nd𝑠) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁)))
9593, 94elab 3499 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd𝑠) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁))
9692, 95sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁))
97 1ex 10236 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ V
9897fconst 6231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((2nd𝑠) “ (1...𝑗)) × {1}):((2nd𝑠) “ (1...𝑗))⟶{1}
99 c0ex 10235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 ∈ V
10099fconst 6231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd𝑠) “ ((𝑗 + 1)...𝑁))⟶{0}
10198, 100pm3.2i 447 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((2nd𝑠) “ (1...𝑗)) × {1}):((2nd𝑠) “ (1...𝑗))⟶{1} ∧ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd𝑠) “ ((𝑗 + 1)...𝑁))⟶{0})
102 dff1o3 6284 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd𝑠):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd𝑠)))
103 imain 6114 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun (2nd𝑠) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))))
104102, 103simplbiim 487 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))))
105 elfznn0 12639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
106105nn0red 11553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
107106ltp1d 11155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
108 fzdisj 12574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
110109imaeq2d 5607 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd𝑠) “ ∅))
111 ima0 5622 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠) “ ∅) = ∅
112110, 111syl6eq 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
113104, 112sylan9req 2825 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = ∅)
114 fun 6206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((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}))
115101, 113, 114sylancr 567 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
116 nn0p1nn 11533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
117105, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
118 nnuz 11924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℕ = (ℤ‘1)
119117, 118syl6eleq 2859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
120 elfzuz3 12545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
121 fzsplit2 12572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
122119, 120, 121syl2anc 565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
123122imaeq2d 5607 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ (1...𝑁)) = ((2nd𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
124 imaundi 5686 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))
125123, 124syl6req 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = ((2nd𝑠) “ (1...𝑁)))
126 f1ofo 6285 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd𝑠):(1...𝑁)–onto→(1...𝑁))
127 foima 6261 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–onto→(1...𝑁) → ((2nd𝑠) “ (1...𝑁)) = (1...𝑁))
128126, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd𝑠) “ (1...𝑁)) = (1...𝑁))
129125, 128sylan9eqr 2826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
130129feq2d 6171 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((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})))
131115, 130mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
13296, 131sylan 561 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
133 fzfid 12979 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
134 inidm 3969 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
13587, 91, 132, 133, 133, 134off 7058 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
136 ovex 6822 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
137 feq1 6166 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝:(1...𝑁)⟶(0...𝐾) ↔ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
138137anbi2d 606 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) ↔ (𝜑 ∧ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
139 poimirlem28.1 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)
140139eleq1d 2834 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐵 ∈ (0...𝑁) ↔ 𝐶 ∈ (0...𝑁)))
141138, 140imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁)) ↔ ((𝜑 ∧ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → 𝐶 ∈ (0...𝑁))))
142 poimirlem28.2 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))
143136, 141, 142vtocl 3408 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → 𝐶 ∈ (0...𝑁))
144135, 143sylan2 572 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁))
145144an12s 620 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (𝜑𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁))
146145ex 397 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁)))
14761, 65, 68, 146vtoclgaf 3420 . . . . . . . . . . . . . . . . . 18 (⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
14860, 147mpcom 38 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
14939, 43, 148chvar 2423 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
150 poimir.0 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℕ)
151150nnnn0d 11552 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
152 nn0uz 11923 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
153151, 152syl6eleq 2859 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘0))
154 fzm1 12626 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘0) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
155153, 154syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
156155adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
157149, 156mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
158157ord 844 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → (¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
15936, 158mt3d 142 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
160159adantrr 688 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
161 fzfi 12978 . . . . . . . . . . . . . . 15 (0...(𝑁 − 1)) ∈ Fin
162150nncnd 11237 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
163 1cnd 10257 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 1 ∈ ℂ)
164162, 163, 163addsubd 10614 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 + 1) − 1) = ((𝑁 − 1) + 1))
165 hashfz0 13420 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (♯‘(0...𝑁)) = (𝑁 + 1))
166151, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1))
167166oveq1d 6807 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((♯‘(0...𝑁)) − 1) = ((𝑁 + 1) − 1))
168 nnm1nn0 11535 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
169 hashfz0 13420 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ ℕ0 → (♯‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1))
170150, 168, 1693syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1))
171164, 167, 1703eqtr4rd 2815 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(0...(𝑁 − 1))) = ((♯‘(0...𝑁)) − 1))
172 hashdifsn 13403 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) ∈ Fin ∧ 𝑡 ∈ (0...𝑁)) → (♯‘((0...𝑁) ∖ {𝑡})) = ((♯‘(0...𝑁)) − 1))
1738, 172mpan 662 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0...𝑁) → (♯‘((0...𝑁) ∖ {𝑡})) = ((♯‘(0...𝑁)) − 1))
174173eqcomd 2776 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0...𝑁) → ((♯‘(0...𝑁)) − 1) = (♯‘((0...𝑁) ∖ {𝑡})))
175171, 174sylan9eq 2824 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → (♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})))
176 diffi 8347 . . . . . . . . . . . . . . . . . 18 ((0...𝑁) ∈ Fin → ((0...𝑁) ∖ {𝑡}) ∈ Fin)
1778, 176ax-mp 5 . . . . . . . . . . . . . . . . 17 ((0...𝑁) ∖ {𝑡}) ∈ Fin
178 hashen 13338 . . . . . . . . . . . . . . . . 17 (((0...(𝑁 − 1)) ∈ Fin ∧ ((0...𝑁) ∖ {𝑡}) ∈ Fin) → ((♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})))
179161, 177, 178mp2an 664 . . . . . . . . . . . . . . . 16 ((♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))
180175, 179sylib 208 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))
181 phpreu 33719 . . . . . . . . . . . . . . 15 (((0...(𝑁 − 1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
182161, 180, 181sylancr 567 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
183182biimpd 219 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
184183impr 442 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
185 nfv 1994 . . . . . . . . . . . . . . 15 𝑧 𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶
186 nfcsb1v 3696 . . . . . . . . . . . . . . . 16 𝑗𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
187186nfeq2 2928 . . . . . . . . . . . . . . 15 𝑗 𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
188 csbeq1a 3689 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑧𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
189188eqeq2d 2780 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
190185, 187, 189cbvreu 3317 . . . . . . . . . . . . . 14 (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
191 eqeq1 2774 . . . . . . . . . . . . . . 15 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
192191reubidv 3274 . . . . . . . . . . . . . 14 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
193190, 192syl5bb 272 . . . . . . . . . . . . 13 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
194193rspcv 3454 . . . . . . . . . . . 12 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
195160, 184, 194sylc 65 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
196 an32 617 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
197196biimpi 206 . . . . . . . . . . . . . . 15 (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
198197adantll 685 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
199 eqeq2 2781 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
200 rexsns 4353 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
20129nfeq2 2928 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗 𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
20231eqeq2d 2780 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑡 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
203201, 202sbciegf 3617 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ V → ([𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
2047, 203ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
205200, 204bitri 264 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
206 rexsns 4353 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
207 vex 3352 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
208187, 189sbciegf 3617 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ V → ([𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
209207, 208ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
210206, 209bitri 264 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
211199, 205, 2103bitr4g 303 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
212211orbi1d 881 . . . . . . . . . . . . . . . . . . . 20 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ((∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
213 rexun 3942 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
214 rexun 3942 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
215212, 213, 2143bitr4g 303 . . . . . . . . . . . . . . . . . . 19 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
216215adantl 467 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
217 eldifsni 4455 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧𝑡)
218217necomd 2997 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑡𝑧)
219 dif32 4037 . . . . . . . . . . . . . . . . . . . . . . 23 (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) = (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})
220219uneq2i 3913 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}))
221 snssi 4472 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → {𝑡} ⊆ ((0...𝑁) ∖ {𝑧}))
222 eldifsn 4451 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) ↔ (𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧))
223 undif 4189 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑡} ⊆ ((0...𝑁) ∖ {𝑧}) ↔ ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧}))
224221, 222, 2233imtr3i 280 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧}))
225220, 224syl5eq 2816 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧}))
226218, 225sylan2 572 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧}))
227226rexeqdv 3293 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
228227adantr 466 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
229 snssi 4472 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → {𝑧} ⊆ ((0...𝑁) ∖ {𝑡}))
230 undif 4189 . . . . . . . . . . . . . . . . . . . . 21 ({𝑧} ⊆ ((0...𝑁) ∖ {𝑡}) ↔ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡}))
231229, 230sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡}))
232231rexeqdv 3293 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
233232ad2antlr 698 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
234216, 228, 2333bitr3d 298 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
235234ralbidv 3134 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
236235biimpar 463 . . . . . . . . . . . . . . 15 ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
237236an32s 623 . . . . . . . . . . . . . 14 ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
238198, 237sylan 561 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
239 simpl 468 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 ∈ (0...𝑁))
240239anim2i 595 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (𝜑𝑡 ∈ (0...𝑁)))
241 necom 2995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑡𝑡𝑧)
242241biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝑡𝑡𝑧)
243242adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) → 𝑡𝑧)
244243anim2i 595 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡)) → (𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧))
245 eldifsn 4451 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ↔ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡))
246245anbi2i 601 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ (𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡)))
247244, 246, 2223imtr4i 281 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
248247adantll 685 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
249248adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
25029nfel1 2927 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))
25137, 250nfim 1976 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
25231eleq1d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑡 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))))
25341, 252imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑡 → (((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))) ↔ ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))))
25426necomd 2997 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶𝑁)
255254neneqd 2947 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → ¬ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
256 fzm1 12626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘0) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
257153, 256syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
258257adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
259148, 258mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
260259ord 844 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (¬ 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
261255, 260mt3d 142 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
262251, 253, 261chvar 2423 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
263262ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
264 eldifi 3881 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧 ∈ (0...𝑁))
265 eleq1w 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑧 → (𝑡 ∈ (0...𝑁) ↔ 𝑧 ∈ (0...𝑁)))
266265anbi2d 606 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑧 → ((𝜑𝑡 ∈ (0...𝑁)) ↔ (𝜑𝑧 ∈ (0...𝑁))))
267 sneq 4324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 𝑧 → {𝑡} = {𝑧})
268267difeq2d 3877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑧 → ((0...𝑁) ∖ {𝑡}) = ((0...𝑁) ∖ {𝑧}))
269268breq2d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑧 → ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})))
270266, 269imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑧 → (((𝜑𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝜑𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))))
271270, 180chvarv 2424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
272264, 271sylan2 572 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
273272adantlr 686 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
274 phpreu 33719 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0...(𝑁 − 1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
275161, 274mpan 662 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
276275biimpa 462 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
277273, 276sylan 561 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
278 eqeq1 2774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
279278adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑗 ∈ ((0...𝑁) ∖ {𝑧})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
280201, 279reubida 3272 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
281280rspcv 3454 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
282263, 277, 281sylc 65 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
283 reurmo 3309 . . . . . . . . . . . . . . . . . . . . . 22 (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
284282, 283syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
285 nfv 1994 . . . . . . . . . . . . . . . . . . . . . 22 𝑖𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶
286285rmo3 3675 . . . . . . . . . . . . . . . . . . . . 21 (∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖))
287284, 286sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖))
288 equcomi 2101 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑡𝑡 = 𝑖)
289288csbeq1d 3687 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑡𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
290 sbsbc 3589 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
291 vex 3352 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑖 ∈ V
292 sbceqg 4126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ V → ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
29329csbconstgf 3692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ V → 𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
294293eqeq1d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ V → (𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
295292, 294bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ V → ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
296291, 295ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
297290, 296bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
298289, 297sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑡 → [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
299298biantrud 515 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑡 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
300299bicomd 213 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑡 → ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
301 eqeq2 2781 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑡 → (𝑗 = 𝑖𝑗 = 𝑡))
302300, 301imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑡 → (((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
303302rspcv 3454 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
304303ralimdv 3111 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
305249, 287, 304sylc 65 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡))
306 dif32 4037 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) = (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})
307306eleq2i 2841 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ 𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))
308 eldifsn 4451 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡))
309 eldifsn 4451 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧))
310307, 308, 3093bitr3ri 291 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡))
311310imbi1i 338 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
312 impexp 437 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
313 impexp 437 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
314311, 312, 3133bitr3ri 291 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
315314albii 1894 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
316 con34b 305 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ (¬ 𝑗 = 𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
317 df-ne 2943 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑡 ↔ ¬ 𝑗 = 𝑡)
318317imbi1i 338 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (¬ 𝑗 = 𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
319316, 318bitr4i 267 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
320319ralbii 3128 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
321 df-ral 3065 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
322320, 321bitri 264 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
323 df-ral 3065 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
324315, 322, 3233bitr4i 292 . . . . . . . . . . . . . . . . . . 19 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
325305, 324sylib 208 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
326 df-ne 2943 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗𝑧 ↔ ¬ 𝑗 = 𝑧)
327326imbi1i 338 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (¬ 𝑗 = 𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
328 con34b 305 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧) ↔ (¬ 𝑗 = 𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
329327, 328bitr4i 267 . . . . . . . . . . . . . . . . . . . 20 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧))
330 ancr 528 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
331329, 330sylbi 207 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
332331ralimi 3100 . . . . . . . . . . . . . . . . . 18 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
333325, 332syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
334240, 333sylanl1 651 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
335201, 278rexbid 3198 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
336335rspcva 3456 . . . . . . . . . . . . . . . . . . 19 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
337262, 336sylan 561 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡 ∈ (0...𝑁)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
338337anasss 457 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
339338ad2antrr 697 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
340 rexim 3155 . . . . . . . . . . . . . . . 16 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
341334, 339, 340sylc 65 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
342 rexex 3149 . . . . . . . . . . . . . . 15 (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
343341, 342syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
34429, 186nfeq 2924 . . . . . . . . . . . . . . 15 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
345188eqeq2d 2780 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
346344, 345equsexv 2264 . . . . . . . . . . . . . 14 (∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
347343, 346sylib 208 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
348238, 347impbida 794 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
349348reubidva 3273 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
350195, 349mpbid 222 . . . . . . . . . 10 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
351 an32 617 . . . . . . . . . . . . . 14 (((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧𝑡))
352245anbi1i 602 . . . . . . . . . . . . . 14 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
353 sneq 4324 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → {𝑦} = {𝑧})
354353difeq2d 3877 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑧}))
355354rexeqdv 3293 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
356355ralbidv 3134 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
357356elrab 3513 . . . . . . . . . . . . . . 15 (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ↔ (𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
358357anbi1i 602 . . . . . . . . . . . . . 14 ((𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧𝑡))
359351, 352, 3583bitr4i 292 . . . . . . . . . . . . 13 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡))
360 eldifsn 4451 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡))
361359, 360bitr4i 267 . . . . . . . . . . . 12 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
362361eubii 2639 . . . . . . . . . . 11 (∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
363 df-reu 3067 . . . . . . . . . . 11 (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
364 euhash1 13409 . . . . . . . . . . . 12 (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1 ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})))
36512, 364ax-mp 5 . . . . . . . . . . 11 ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1 ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
366362, 363, 3653bitr4i 292 . . . . . . . . . 10 (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
367350, 366sylib 208 . . . . . . . . 9 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
36825, 367sylan2b 573 . . . . . . . 8 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
369368oveq1d 6807 . . . . . . 7 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (1 + 1))
37020, 369eqtr3d 2806 . . . . . 6 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) = (1 + 1))
3716, 370syl5breqr 4822 . . . . 5 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
372371ex 397 . . . 4 (𝜑 → (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
373372exlimdv 2012 . . 3 (𝜑 → (∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
3741, 373syl5bi 232 . 2 (𝜑 → (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
375 dvds0 15205 . . . . 5 (2 ∈ ℤ → 2 ∥ 0)
3762, 375ax-mp 5 . . . 4 2 ∥ 0
377 hash0 13359 . . . 4 (♯‘∅) = 0
378376, 377breqtrri 4811 . . 3 2 ∥ (♯‘∅)
379 fveq2 6332 . . 3 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) = (♯‘∅))
380378, 379syl5breqr 4822 . 2 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
381374, 380pm2.61d2 173 1 (𝜑 → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 826  wal 1628   = wceq 1630  wex 1851  [wsb 2048  wcel 2144  ∃!weu 2617  {cab 2756  wne 2942  wral 3060  wrex 3061  ∃!wreu 3062  ∃*wrmo 3063  {crab 3064  Vcvv 3349  [wsbc 3585  csb 3680  cdif 3718  cun 3719  cin 3720  wss 3721  c0 4061  {csn 4314  cop 4320   class class class wbr 4784   × cxp 5247  ccnv 5248  cima 5252  Fun wfun 6025  wf 6027  ontowfo 6029  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6792  𝑓 cof 7041  1st c1st 7312  2nd c2nd 7313  𝑚 cmap 8008  cen 8105  Fincfn 8108  0cc0 10137  1c1 10138   + caddc 10140   < clt 10275  cmin 10467  cn 11221  2c2 11271  0cn0 11493  cz 11578  cuz 11887  ...cfz 12532  ..^cfzo 12672  chash 13320  cdvds 15188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-cnex 10193  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-mulcom 10201  ax-addass 10202  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1ne0 10206  ax-1rid 10207  ax-rnegex 10208  ax-rrecex 10209  ax-cnre 10210  ax-pre-lttri 10211  ax-pre-lttrn 10212  ax-pre-ltadd 10213  ax-pre-mulgt0 10214
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-nel 3046  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-of 7043  df-om 7212  df-1st 7314  df-2nd 7315  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-1o 7712  df-oadd 7716  df-er 7895  df-map 8010  df-en 8109  df-dom 8110  df-sdom 8111  df-fin 8112  df-card 8964  df-cda 9191  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-sub 10469  df-neg 10470  df-nn 11222  df-2 11280  df-n0 11494  df-z 11579  df-uz 11888  df-fz 12533  df-fzo 12673  df-hash 13321  df-dvds 15189
This theorem is referenced by:  poimirlem26  33761
  Copyright terms: Public domain W3C validator