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 35811
Description: Lemma for poimir 35819 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𝑠) ∘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
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 4280 . . 3 (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ ↔ ∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})
2 2z 12361 . . . . . . . 8 2 ∈ ℤ
3 iddvds 15988 . . . . . . . 8 (2 ∈ ℤ → 2 ∥ 2)
42, 3ax-mp 5 . . . . . . 7 2 ∥ 2
5 df-2 12045 . . . . . . 7 2 = (1 + 1)
64, 5breqtri 5100 . . . . . 6 2 ∥ (1 + 1)
7 vex 3437 . . . . . . . . . 10 𝑡 ∈ V
8 fzfi 13701 . . . . . . . . . . . . 13 (0...𝑁) ∈ Fin
9 rabfi 9053 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin → {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin)
108, 9ax-mp 5 . . . . . . . . . . . 12 {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin
11 diffi 8971 . . . . . . . . . . . 12 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin → ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin)
1210, 11ax-mp 5 . . . . . . . . . . 11 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin
13 neldifsn 4726 . . . . . . . . . . 11 ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})
1412, 13pm3.2i 471 . . . . . . . . . 10 (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin ∧ ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
15 hashunsng 14116 . . . . . . . . . 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 4744 . . . . . . . . . 10 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡}) = {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})
1817fveq2d 6787 . . . . . . . . 9 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → (♯‘(({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡})) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
1916, 18eqtr3id 2793 . . . . . . . 8 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
2019adantl 482 . . . . . . 7 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
21 sneq 4572 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → {𝑦} = {𝑡})
2221difeq2d 4058 . . . . . . . . . . . 12 (𝑦 = 𝑡 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑡}))
2322rexeqdv 3350 . . . . . . . . . . 11 (𝑦 = 𝑡 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
2423ralbidv 3113 . . . . . . . . . 10 (𝑦 = 𝑡 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
2524elrab 3625 . . . . . . . . 9 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ↔ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
26 poimirlem25.5 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑁𝑇, 𝑈⟩ / 𝑠𝐶)
2726ralrimiva 3104 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑗 ∈ (0...𝑁)𝑁𝑇, 𝑈⟩ / 𝑠𝐶)
28 nfcv 2908 . . . . . . . . . . . . . . . . . 18 𝑗𝑁
29 nfcsb1v 3858 . . . . . . . . . . . . . . . . . 18 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
3028, 29nfne 3046 . . . . . . . . . . . . . . . . 17 𝑗 𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
31 csbeq1a 3847 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
3231neeq2d 3005 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑡 → (𝑁𝑇, 𝑈⟩ / 𝑠𝐶𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
3330, 32rspc 3550 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0...𝑁) → (∀𝑗 ∈ (0...𝑁)𝑁𝑇, 𝑈⟩ / 𝑠𝐶𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
3427, 33mpan9 507 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
35 nesym 3001 . . . . . . . . . . . . . . 15 (𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
3634, 35sylib 217 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
37 nfv 1918 . . . . . . . . . . . . . . . . . 18 𝑗(𝜑𝑡 ∈ (0...𝑁))
3829nfel1 2924 . . . . . . . . . . . . . . . . . 18 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)
3937, 38nfim 1900 . . . . . . . . . . . . . . . . 17 𝑗((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
40 eleq1w 2822 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑡 → (𝑗 ∈ (0...𝑁) ↔ 𝑡 ∈ (0...𝑁)))
4140anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡 → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡 ∈ (0...𝑁))))
4231eleq1d 2824 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
4341, 42imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑡 → (((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)) ↔ ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))))
44 poimirlem25.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
45 ovex 7317 . . . . . . . . . . . . . . . . . . . . . 22 (0..^𝐾) ∈ V
46 ovex 7317 . . . . . . . . . . . . . . . . . . . . . 22 (1...𝑁) ∈ V
4745, 46elmap 8668 . . . . . . . . . . . . . . . . . . . . 21 (𝑇 ∈ ((0..^𝐾) ↑m (1...𝑁)) ↔ 𝑇:(1...𝑁)⟶(0..^𝐾))
4844, 47sylibr 233 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑇 ∈ ((0..^𝐾) ↑m (1...𝑁)))
49 poimirlem25.4 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
50 fzfi 13701 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑁) ∈ Fin
51 f1oexrnex 7783 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ Fin) → 𝑈 ∈ V)
5250, 51mpan2 688 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ V)
53 f1oeq1 6713 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑈 → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)))
5453elabg 3608 . . . . . . . . . . . . . . . . . . . . . . 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 267 . . . . . . . . . . . . . . . . . . . . 21 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
5749, 56syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
58 opelxpi 5627 . . . . . . . . . . . . . . . . . . . 20 ((𝑇 ∈ ((0..^𝐾) ↑m (1...𝑁)) ∧ 𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
5948, 57, 58syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
6059adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
61 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 𝑠𝑇, 𝑈
62 nfv 1918 . . . . . . . . . . . . . . . . . . . 20 𝑠(𝜑𝑗 ∈ (0...𝑁))
63 nfcsb1v 3858 . . . . . . . . . . . . . . . . . . . . 21 𝑠𝑇, 𝑈⟩ / 𝑠𝐶
6463nfel1 2924 . . . . . . . . . . . . . . . . . . . 20 𝑠𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)
6562, 64nfim 1900 . . . . . . . . . . . . . . . . . . 19 𝑠((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
66 csbeq1a 3847 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ⟨𝑇, 𝑈⟩ → 𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
6766eleq1d 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ⟨𝑇, 𝑈⟩ → (𝐶 ∈ (0...𝑁) ↔ 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
6867imbi2d 341 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ⟨𝑇, 𝑈⟩ → (((𝜑𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁)) ↔ ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))))
69 elun 4084 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 ∈ ({1} ∪ {0}) ↔ (𝑝 ∈ {1} ∨ 𝑝 ∈ {0}))
70 fzofzp1 13493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝐾) → (𝑖 + 1) ∈ (0...𝐾))
71 elsni 4579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ {1} → 𝑝 = 1)
7271oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ {1} → (𝑖 + 𝑝) = (𝑖 + 1))
7372eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ {1} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 1) ∈ (0...𝐾)))
7470, 73syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {1} → (𝑖 + 𝑝) ∈ (0...𝐾)))
75 elfzonn0 13441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℕ0)
7675nn0cnd 12304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℂ)
7776addid1d 11184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) = 𝑖)
78 elfzofz 13412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ (0...𝐾))
7977, 78eqeltrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) ∈ (0...𝐾))
80 elsni 4579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ {0} → 𝑝 = 0)
8180oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ {0} → (𝑖 + 𝑝) = (𝑖 + 0))
8281eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ {0} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 0) ∈ (0...𝐾)))
8379, 82syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {0} → (𝑖 + 𝑝) ∈ (0...𝐾)))
8474, 83jaod 856 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝐾) → ((𝑝 ∈ {1} ∨ 𝑝 ∈ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾)))
8569, 84syl5bi 241 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ ({1} ∪ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾)))
8685imp 407 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0})) → (𝑖 + 𝑝) ∈ (0...𝐾))
8786adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0}))) → (𝑖 + 𝑝) ∈ (0...𝐾))
88 xp1st 7872 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠) ∈ ((0..^𝐾) ↑m (1...𝑁)))
89 elmapi 8646 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑠) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
9190adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
92 xp2nd 7873 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd𝑠) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
93 fvex 6796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (2nd𝑠) ∈ V
94 f1oeq1 6713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = (2nd𝑠) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁)))
9593, 94elab 3610 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd𝑠) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁))
9692, 95sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁))
97 1ex 10980 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ V
9897fconst 6669 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((2nd𝑠) “ (1...𝑗)) × {1}):((2nd𝑠) “ (1...𝑗))⟶{1}
99 c0ex 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 ∈ V
10099fconst 6669 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd𝑠) “ ((𝑗 + 1)...𝑁))⟶{0}
10198, 100pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((2nd𝑠) “ (1...𝑗)) × {1}):((2nd𝑠) “ (1...𝑗))⟶{1} ∧ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd𝑠) “ ((𝑗 + 1)...𝑁))⟶{0})
102 dff1o3 6731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd𝑠):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd𝑠)))
103 imain 6526 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun (2nd𝑠) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))))
104102, 103simplbiim 505 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))))
105 elfznn0 13358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
106105nn0red 12303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
107106ltp1d 11914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
108 fzdisj 13292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
110109imaeq2d 5972 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd𝑠) “ ∅))
111 ima0 5988 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠) “ ∅) = ∅
112110, 111eqtrdi 2795 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
113104, 112sylan9req 2800 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = ∅)
114 fun 6645 . . . . . . . . . . . . . . . . . . . . . . . . . 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 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
116 nn0p1nn 12281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
117105, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
118 nnuz 12630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℕ = (ℤ‘1)
119117, 118eleqtrdi 2850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
120 elfzuz3 13262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
121 fzsplit2 13290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
122119, 120, 121syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
123122imaeq2d 5972 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ (1...𝑁)) = ((2nd𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
124 imaundi 6058 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))
125123, 124eqtr2di 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = ((2nd𝑠) “ (1...𝑁)))
126 f1ofo 6732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd𝑠):(1...𝑁)–onto→(1...𝑁))
127 foima 6702 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–onto→(1...𝑁) → ((2nd𝑠) “ (1...𝑁)) = (1...𝑁))
128126, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd𝑠) “ (1...𝑁)) = (1...𝑁))
129125, 128sylan9eqr 2801 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
130129feq2d 6595 . . . . . . . . . . . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
13296, 131sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
133 fzfid 13702 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
134 inidm 4153 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
13587, 91, 132, 133, 133, 134off 7560 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
136 ovex 7317 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
137 feq1 6590 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝:(1...𝑁)⟶(0...𝐾) ↔ ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
138137anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) ↔ (𝜑 ∧ ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
139 poimirlem28.1 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)
140139eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐵 ∈ (0...𝑁) ↔ 𝐶 ∈ (0...𝑁)))
141138, 140imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁)) ↔ ((𝜑 ∧ ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → 𝐶 ∈ (0...𝑁))))
142 poimirlem28.2 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))
143136, 141, 142vtocl 3499 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → 𝐶 ∈ (0...𝑁))
144135, 143sylan2 593 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁))
145144an12s 646 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (𝜑𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁))
146145ex 413 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁)))
14761, 65, 68, 146vtoclgaf 3513 . . . . . . . . . . . . . . . . . 18 (⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
14860, 147mpcom 38 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
14939, 43, 148chvarfv 2234 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
150 poimir.0 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℕ)
151150nnnn0d 12302 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
152 nn0uz 12629 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
153151, 152eleqtrdi 2850 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘0))
154 fzm1 13345 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘0) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
155153, 154syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
156155adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
157149, 156mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
158157ord 861 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → (¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
15936, 158mt3d 148 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
160159adantrr 714 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
161 fzfi 13701 . . . . . . . . . . . . . . 15 (0...(𝑁 − 1)) ∈ Fin
162150nncnd 11998 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
163 1cnd 10979 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 1 ∈ ℂ)
164162, 163, 163addsubd 11362 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 + 1) − 1) = ((𝑁 − 1) + 1))
165 hashfz0 14156 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (♯‘(0...𝑁)) = (𝑁 + 1))
166151, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1))
167166oveq1d 7299 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((♯‘(0...𝑁)) − 1) = ((𝑁 + 1) − 1))
168 nnm1nn0 12283 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
169 hashfz0 14156 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ ℕ0 → (♯‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1))
170150, 168, 1693syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1))
171164, 167, 1703eqtr4rd 2790 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(0...(𝑁 − 1))) = ((♯‘(0...𝑁)) − 1))
172 hashdifsn 14138 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) ∈ Fin ∧ 𝑡 ∈ (0...𝑁)) → (♯‘((0...𝑁) ∖ {𝑡})) = ((♯‘(0...𝑁)) − 1))
1738, 172mpan 687 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0...𝑁) → (♯‘((0...𝑁) ∖ {𝑡})) = ((♯‘(0...𝑁)) − 1))
174173eqcomd 2745 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0...𝑁) → ((♯‘(0...𝑁)) − 1) = (♯‘((0...𝑁) ∖ {𝑡})))
175171, 174sylan9eq 2799 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → (♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})))
176 diffi 8971 . . . . . . . . . . . . . . . . . 18 ((0...𝑁) ∈ Fin → ((0...𝑁) ∖ {𝑡}) ∈ Fin)
1778, 176ax-mp 5 . . . . . . . . . . . . . . . . 17 ((0...𝑁) ∖ {𝑡}) ∈ Fin
178 hashen 14070 . . . . . . . . . . . . . . . . 17 (((0...(𝑁 − 1)) ∈ Fin ∧ ((0...𝑁) ∖ {𝑡}) ∈ Fin) → ((♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})))
179161, 177, 178mp2an 689 . . . . . . . . . . . . . . . 16 ((♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))
180175, 179sylib 217 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))
181 phpreu 35770 . . . . . . . . . . . . . . 15 (((0...(𝑁 − 1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
182161, 180, 181sylancr 587 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
183182biimpd 228 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
184183impr 455 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
185 nfv 1918 . . . . . . . . . . . . . . 15 𝑧 𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶
186 nfcsb1v 3858 . . . . . . . . . . . . . . . 16 𝑗𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
187186nfeq2 2925 . . . . . . . . . . . . . . 15 𝑗 𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
188 csbeq1a 3847 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑧𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
189188eqeq2d 2750 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
190185, 187, 189cbvreuw 3377 . . . . . . . . . . . . . 14 (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
191 eqeq1 2743 . . . . . . . . . . . . . . 15 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
192191reubidv 3324 . . . . . . . . . . . . . 14 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
193190, 192syl5bb 283 . . . . . . . . . . . . 13 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
194193rspcv 3558 . . . . . . . . . . . 12 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
195160, 184, 194sylc 65 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
196 an32 643 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
197196biimpi 215 . . . . . . . . . . . . . . 15 (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
198197adantll 711 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
199 eqeq2 2751 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
200 rexsns 4606 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
20129nfeq2 2925 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗 𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
20231eqeq2d 2750 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑡 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
203201, 202sbciegf 3756 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ V → ([𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
2047, 203ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
205200, 204bitri 274 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
206 rexsns 4606 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
207 vex 3437 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
208187, 189sbciegf 3756 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ V → ([𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
209207, 208ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
210206, 209bitri 274 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
211199, 205, 2103bitr4g 314 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
212211orbi1d 914 . . . . . . . . . . . . . . . . . . . 20 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ((∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
213 rexun 4125 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
214 rexun 4125 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
215212, 213, 2143bitr4g 314 . . . . . . . . . . . . . . . . . . 19 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
216215adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
217 eldifsni 4724 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧𝑡)
218217necomd 3000 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑡𝑧)
219 dif32 4227 . . . . . . . . . . . . . . . . . . . . . . 23 (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) = (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})
220219uneq2i 4095 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}))
221 snssi 4742 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → {𝑡} ⊆ ((0...𝑁) ∖ {𝑧}))
222 eldifsn 4721 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) ↔ (𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧))
223 undif 4416 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑡} ⊆ ((0...𝑁) ∖ {𝑧}) ↔ ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧}))
224221, 222, 2233imtr3i 291 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧}))
225220, 224eqtrid 2791 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧}))
226218, 225sylan2 593 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧}))
227226rexeqdv 3350 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
228227adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
229 snssi 4742 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → {𝑧} ⊆ ((0...𝑁) ∖ {𝑡}))
230 undif 4416 . . . . . . . . . . . . . . . . . . . . 21 ({𝑧} ⊆ ((0...𝑁) ∖ {𝑡}) ↔ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡}))
231229, 230sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡}))
232231rexeqdv 3350 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
233232ad2antlr 724 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
234216, 228, 2333bitr3d 309 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
235234ralbidv 3113 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
236235biimpar 478 . . . . . . . . . . . . . . 15 ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
237236an32s 649 . . . . . . . . . . . . . 14 ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
238198, 237sylan 580 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
239 simpl 483 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 ∈ (0...𝑁))
240239anim2i 617 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (𝜑𝑡 ∈ (0...𝑁)))
241 necom 2998 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑡𝑡𝑧)
242241biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝑡𝑡𝑧)
243242adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) → 𝑡𝑧)
244243anim2i 617 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡)) → (𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧))
245 eldifsn 4721 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ↔ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡))
246245anbi2i 623 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ (𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡)))
247244, 246, 2223imtr4i 292 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
248247adantll 711 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
249248adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
25029nfel1 2924 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))
25137, 250nfim 1900 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
25231eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑡 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))))
25341, 252imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑡 → (((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))) ↔ ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))))
25426necomd 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶𝑁)
255254neneqd 2949 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → ¬ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
256 fzm1 13345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘0) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
257153, 256syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
258257adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
259148, 258mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
260259ord 861 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (¬ 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
261255, 260mt3d 148 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
262251, 253, 261chvarfv 2234 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
263262ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
264 eldifi 4062 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧 ∈ (0...𝑁))
265 eleq1w 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑧 → (𝑡 ∈ (0...𝑁) ↔ 𝑧 ∈ (0...𝑁)))
266265anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑧 → ((𝜑𝑡 ∈ (0...𝑁)) ↔ (𝜑𝑧 ∈ (0...𝑁))))
267 sneq 4572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 𝑧 → {𝑡} = {𝑧})
268267difeq2d 4058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑧 → ((0...𝑁) ∖ {𝑡}) = ((0...𝑁) ∖ {𝑧}))
269268breq2d 5087 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑧 → ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})))
270266, 269imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑧 → (((𝜑𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝜑𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))))
271270, 180chvarvv 2003 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
272264, 271sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
273272adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
274 phpreu 35770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0...(𝑁 − 1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
275161, 274mpan 687 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
276275biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
277273, 276sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
278 eqeq1 2743 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
279278adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑗 ∈ ((0...𝑁) ∖ {𝑧})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
280201, 279reubida 3322 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
281280rspcv 3558 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
282263, 277, 281sylc 65 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
283 reurmo 3365 . . . . . . . . . . . . . . . . . . . . . 22 (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
284282, 283syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
285 nfv 1918 . . . . . . . . . . . . . . . . . . . . . 22 𝑖𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶
286285rmo3 3823 . . . . . . . . . . . . . . . . . . . . 21 (∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖))
287284, 286sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖))
288 equcomi 2021 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑡𝑡 = 𝑖)
289288csbeq1d 3837 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑡𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
290 sbsbc 3721 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
291 vex 3437 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑖 ∈ V
292 sbceqg 4344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ V → ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
29329csbconstgf 3851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ V → 𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
294293eqeq1d 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ V → (𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
295292, 294bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ V → ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
296291, 295ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
297290, 296bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
298289, 297sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑡 → [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
299298biantrud 532 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑡 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
300299bicomd 222 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑡 → ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
301 eqeq2 2751 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑡 → (𝑗 = 𝑖𝑗 = 𝑡))
302300, 301imbi12d 345 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑡 → (((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
303302rspcv 3558 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
304303ralimdv 3110 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
305249, 287, 304sylc 65 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡))
306 dif32 4227 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) = (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})
307306eleq2i 2831 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ 𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))
308 eldifsn 4721 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡))
309 eldifsn 4721 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧))
310307, 308, 3093bitr3ri 302 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡))
311310imbi1i 350 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
312 impexp 451 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
313 impexp 451 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
314311, 312, 3133bitr3ri 302 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
315314albii 1822 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
316 con34b 316 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ (¬ 𝑗 = 𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
317 df-ne 2945 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑡 ↔ ¬ 𝑗 = 𝑡)
318317imbi1i 350 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (¬ 𝑗 = 𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
319316, 318bitr4i 277 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
320319ralbii 3093 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
321 df-ral 3070 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
322320, 321bitri 274 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
323 df-ral 3070 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
324315, 322, 3233bitr4i 303 . . . . . . . . . . . . . . . . . . 19 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
325305, 324sylib 217 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
326 df-ne 2945 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗𝑧 ↔ ¬ 𝑗 = 𝑧)
327326imbi1i 350 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (¬ 𝑗 = 𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
328 con34b 316 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧) ↔ (¬ 𝑗 = 𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
329327, 328bitr4i 277 . . . . . . . . . . . . . . . . . . . 20 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧))
330 ancr 547 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
331329, 330sylbi 216 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
332331ralimi 3088 . . . . . . . . . . . . . . . . . 18 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
333325, 332syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
334240, 333sylanl1 677 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
335201, 278rexbid 3254 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
336335rspcva 3560 . . . . . . . . . . . . . . . . . . 19 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
337262, 336sylan 580 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡 ∈ (0...𝑁)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
338337anasss 467 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
339338ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
340 rexim 3173 . . . . . . . . . . . . . . . 16 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
341334, 339, 340sylc 65 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
342 rexex 3172 . . . . . . . . . . . . . . 15 (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
343341, 342syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
34429, 186nfeq 2921 . . . . . . . . . . . . . . 15 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
345188eqeq2d 2750 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
346344, 345equsexv 2261 . . . . . . . . . . . . . 14 (∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
347343, 346sylib 217 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
348238, 347impbida 798 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
349348reubidva 3323 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
350195, 349mpbid 231 . . . . . . . . . 10 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
351 an32 643 . . . . . . . . . . . . . 14 (((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧𝑡))
352245anbi1i 624 . . . . . . . . . . . . . 14 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
353 sneq 4572 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → {𝑦} = {𝑧})
354353difeq2d 4058 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑧}))
355354rexeqdv 3350 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
356355ralbidv 3113 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
357356elrab 3625 . . . . . . . . . . . . . . 15 (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ↔ (𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
358357anbi1i 624 . . . . . . . . . . . . . 14 ((𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧𝑡))
359351, 352, 3583bitr4i 303 . . . . . . . . . . . . 13 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡))
360 eldifsn 4721 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡))
361359, 360bitr4i 277 . . . . . . . . . . . 12 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
362361eubii 2586 . . . . . . . . . . 11 (∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
363 df-reu 3073 . . . . . . . . . . 11 (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
364 euhash1 14144 . . . . . . . . . . . 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 303 . . . . . . . . . 10 (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
367350, 366sylib 217 . . . . . . . . 9 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
36825, 367sylan2b 594 . . . . . . . 8 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
369368oveq1d 7299 . . . . . . 7 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (1 + 1))
37020, 369eqtr3d 2781 . . . . . 6 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) = (1 + 1))
3716, 370breqtrrid 5113 . . . . 5 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
372371ex 413 . . . 4 (𝜑 → (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
373372exlimdv 1937 . . 3 (𝜑 → (∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
3741, 373syl5bi 241 . 2 (𝜑 → (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
375 dvds0 15990 . . . . 5 (2 ∈ ℤ → 2 ∥ 0)
3762, 375ax-mp 5 . . . 4 2 ∥ 0
377 hash0 14091 . . . 4 (♯‘∅) = 0
378376, 377breqtrri 5102 . . 3 2 ∥ (♯‘∅)
379 fveq2 6783 . . 3 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) = (♯‘∅))
380378, 379breqtrrid 5113 . 2 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
381374, 380pm2.61d2 181 1 (𝜑 → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  wal 1537   = wceq 1539  wex 1782  [wsb 2068  wcel 2107  ∃!weu 2569  {cab 2716  wne 2944  wral 3065  wrex 3066  ∃!wreu 3067  ∃*wrmo 3068  {crab 3069  Vcvv 3433  [wsbc 3717  csb 3833  cdif 3885  cun 3886  cin 3887  wss 3888  c0 4257  {csn 4562  cop 4568   class class class wbr 5075   × cxp 5588  ccnv 5589  cima 5593  Fun wfun 6431  wf 6433  ontowfo 6435  1-1-ontowf1o 6436  cfv 6437  (class class class)co 7284  f cof 7540  1st c1st 7838  2nd c2nd 7839  m cmap 8624  cen 8739  Fincfn 8742  0cc0 10880  1c1 10881   + caddc 10883   < clt 11018  cmin 11214  cn 11982  2c2 12037  0cn0 12242  cz 12328  cuz 12591  ...cfz 13248  ..^cfzo 13391  chash 14053  cdvds 15972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-oadd 8310  df-er 8507  df-map 8626  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-dju 9668  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-nn 11983  df-2 12045  df-n0 12243  df-z 12329  df-uz 12592  df-fz 13249  df-fzo 13392  df-hash 14054  df-dvds 15973
This theorem is referenced by:  poimirlem26  35812
  Copyright terms: Public domain W3C validator