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 33747
Description: Lemma for poimir 33755 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 4131 . . 3 (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ ↔ ∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})
2 2z 11675 . . . . . . . 8 2 ∈ ℤ
3 iddvds 15218 . . . . . . . 8 (2 ∈ ℤ → 2 ∥ 2)
42, 3ax-mp 5 . . . . . . 7 2 ∥ 2
5 df-2 11364 . . . . . . 7 2 = (1 + 1)
64, 5breqtri 4869 . . . . . 6 2 ∥ (1 + 1)
7 vex 3394 . . . . . . . . . 10 𝑡 ∈ V
8 fzfi 12995 . . . . . . . . . . . . 13 (0...𝑁) ∈ Fin
9 rabfi 8424 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin → {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin)
108, 9ax-mp 5 . . . . . . . . . . . 12 {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin
11 diffi 8431 . . . . . . . . . . . 12 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin → ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin)
1210, 11ax-mp 5 . . . . . . . . . . 11 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin
13 neldifsn 4513 . . . . . . . . . . 11 ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})
1412, 13pm3.2i 458 . . . . . . . . . 10 (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin ∧ ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
15 hashunsng 13399 . . . . . . . . . 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 4531 . . . . . . . . . 10 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡}) = {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})
1817fveq2d 6412 . . . . . . . . 9 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → (♯‘(({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡})) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
1916, 18syl5eqr 2854 . . . . . . . 8 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
2019adantl 469 . . . . . . 7 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
21 sneq 4380 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → {𝑦} = {𝑡})
2221difeq2d 3927 . . . . . . . . . . . 12 (𝑦 = 𝑡 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑡}))
2322rexeqdv 3334 . . . . . . . . . . 11 (𝑦 = 𝑡 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
2423ralbidv 3174 . . . . . . . . . 10 (𝑦 = 𝑡 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
2524elrab 3559 . . . . . . . . 9 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ↔ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
26 poimirlem25.5 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑁𝑇, 𝑈⟩ / 𝑠𝐶)
2726ralrimiva 3154 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑗 ∈ (0...𝑁)𝑁𝑇, 𝑈⟩ / 𝑠𝐶)
28 nfcv 2948 . . . . . . . . . . . . . . . . . 18 𝑗𝑁
29 nfcsb1v 3744 . . . . . . . . . . . . . . . . . 18 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
3028, 29nfne 3078 . . . . . . . . . . . . . . . . 17 𝑗 𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
31 csbeq1a 3737 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
3231neeq2d 3038 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑡 → (𝑁𝑇, 𝑈⟩ / 𝑠𝐶𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
3330, 32rspc 3496 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0...𝑁) → (∀𝑗 ∈ (0...𝑁)𝑁𝑇, 𝑈⟩ / 𝑠𝐶𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
3427, 33mpan9 498 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
35 nesym 3034 . . . . . . . . . . . . . . 15 (𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
3634, 35sylib 209 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
37 nfv 2005 . . . . . . . . . . . . . . . . . 18 𝑗(𝜑𝑡 ∈ (0...𝑁))
3829nfel1 2963 . . . . . . . . . . . . . . . . . 18 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)
3937, 38nfim 1987 . . . . . . . . . . . . . . . . 17 𝑗((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
40 eleq1w 2868 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑡 → (𝑗 ∈ (0...𝑁) ↔ 𝑡 ∈ (0...𝑁)))
4140anbi2d 616 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡 → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡 ∈ (0...𝑁))))
4231eleq1d 2870 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
4341, 42imbi12d 335 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑡 → (((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)) ↔ ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))))
44 poimirlem25.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
45 ovex 6906 . . . . . . . . . . . . . . . . . . . . . 22 (0..^𝐾) ∈ V
46 ovex 6906 . . . . . . . . . . . . . . . . . . . . . 22 (1...𝑁) ∈ V
4745, 46elmap 8121 . . . . . . . . . . . . . . . . . . . . 21 (𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) ↔ 𝑇:(1...𝑁)⟶(0..^𝐾))
4844, 47sylibr 225 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
49 poimirlem25.4 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
50 fzfi 12995 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑁) ∈ Fin
51 f1oexrnex 7345 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ Fin) → 𝑈 ∈ V)
5250, 51mpan2 674 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ V)
53 f1oeq1 6343 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑈 → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)))
5453elabg 3546 . . . . . . . . . . . . . . . . . . . . . . 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 259 . . . . . . . . . . . . . . . . . . . . 21 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
5749, 56syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
58 opelxpi 5348 . . . . . . . . . . . . . . . . . . . 20 ((𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) ∧ 𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
5948, 57, 58syl2anc 575 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
6059adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
61 nfcv 2948 . . . . . . . . . . . . . . . . . . 19 𝑠𝑇, 𝑈
62 nfv 2005 . . . . . . . . . . . . . . . . . . . 20 𝑠(𝜑𝑗 ∈ (0...𝑁))
63 nfcsb1v 3744 . . . . . . . . . . . . . . . . . . . . 21 𝑠𝑇, 𝑈⟩ / 𝑠𝐶
6463nfel1 2963 . . . . . . . . . . . . . . . . . . . 20 𝑠𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)
6562, 64nfim 1987 . . . . . . . . . . . . . . . . . . 19 𝑠((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
66 csbeq1a 3737 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ⟨𝑇, 𝑈⟩ → 𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
6766eleq1d 2870 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ⟨𝑇, 𝑈⟩ → (𝐶 ∈ (0...𝑁) ↔ 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
6867imbi2d 331 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ⟨𝑇, 𝑈⟩ → (((𝜑𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁)) ↔ ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))))
69 elun 3952 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 ∈ ({1} ∪ {0}) ↔ (𝑝 ∈ {1} ∨ 𝑝 ∈ {0}))
70 fzofzp1 12789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝐾) → (𝑖 + 1) ∈ (0...𝐾))
71 elsni 4387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ {1} → 𝑝 = 1)
7271oveq2d 6890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ {1} → (𝑖 + 𝑝) = (𝑖 + 1))
7372eleq1d 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ {1} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 1) ∈ (0...𝐾)))
7470, 73syl5ibrcom 238 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {1} → (𝑖 + 𝑝) ∈ (0...𝐾)))
75 elfzonn0 12737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℕ0)
7675nn0cnd 11619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℂ)
7776addid1d 10521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) = 𝑖)
78 elfzofz 12709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ (0...𝐾))
7977, 78eqeltrd 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) ∈ (0...𝐾))
80 elsni 4387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ {0} → 𝑝 = 0)
8180oveq2d 6890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ {0} → (𝑖 + 𝑝) = (𝑖 + 0))
8281eleq1d 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ {0} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 0) ∈ (0...𝐾)))
8379, 82syl5ibrcom 238 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {0} → (𝑖 + 𝑝) ∈ (0...𝐾)))
8474, 83jaod 877 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝐾) → ((𝑝 ∈ {1} ∨ 𝑝 ∈ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾)))
8569, 84syl5bi 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ ({1} ∪ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾)))
8685imp 395 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0})) → (𝑖 + 𝑝) ∈ (0...𝐾))
8786adantl 469 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0}))) → (𝑖 + 𝑝) ∈ (0...𝐾))
88 xp1st 7430 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
89 elmapi 8114 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑠) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
9190adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
92 xp2nd 7431 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd𝑠) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
93 fvex 6421 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (2nd𝑠) ∈ V
94 f1oeq1 6343 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = (2nd𝑠) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁)))
9593, 94elab 3545 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd𝑠) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁))
9692, 95sylib 209 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁))
97 1ex 10321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ V
9897fconst 6306 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((2nd𝑠) “ (1...𝑗)) × {1}):((2nd𝑠) “ (1...𝑗))⟶{1}
99 c0ex 10319 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 ∈ V
10099fconst 6306 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd𝑠) “ ((𝑗 + 1)...𝑁))⟶{0}
10198, 100pm3.2i 458 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((2nd𝑠) “ (1...𝑗)) × {1}):((2nd𝑠) “ (1...𝑗))⟶{1} ∧ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd𝑠) “ ((𝑗 + 1)...𝑁))⟶{0})
102 dff1o3 6359 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd𝑠):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd𝑠)))
103 imain 6185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun (2nd𝑠) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))))
104102, 103simplbiim 495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))))
105 elfznn0 12656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
106105nn0red 11618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
107106ltp1d 11239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
108 fzdisj 12591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
110109imaeq2d 5676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd𝑠) “ ∅))
111 ima0 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠) “ ∅) = ∅
112110, 111syl6eq 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
113104, 112sylan9req 2861 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = ∅)
114 fun 6281 . . . . . . . . . . . . . . . . . . . . . . . . . 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 577 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
116 nn0p1nn 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
117105, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
118 nnuz 11941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℕ = (ℤ‘1)
119117, 118syl6eleq 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
120 elfzuz3 12562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
121 fzsplit2 12589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
122119, 120, 121syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
123122imaeq2d 5676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ (1...𝑁)) = ((2nd𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
124 imaundi 5756 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))
125123, 124syl6req 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = ((2nd𝑠) “ (1...𝑁)))
126 f1ofo 6360 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd𝑠):(1...𝑁)–onto→(1...𝑁))
127 foima 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–onto→(1...𝑁) → ((2nd𝑠) “ (1...𝑁)) = (1...𝑁))
128126, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd𝑠) “ (1...𝑁)) = (1...𝑁))
129125, 128sylan9eqr 2862 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
130129feq2d 6242 . . . . . . . . . . . . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
13296, 131sylan 571 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
133 fzfid 12996 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
134 inidm 4019 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
13587, 91, 132, 133, 133, 134off 7142 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
136 ovex 6906 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
137 feq1 6237 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝:(1...𝑁)⟶(0...𝐾) ↔ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
138137anbi2d 616 . . . . . . . . . . . . . . . . . . . . . . . 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 2870 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐵 ∈ (0...𝑁) ↔ 𝐶 ∈ (0...𝑁)))
141138, 140imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . 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 3452 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → 𝐶 ∈ (0...𝑁))
144135, 143sylan2 582 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁))
145144an12s 631 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (𝜑𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁))
146145ex 399 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁)))
14761, 65, 68, 146vtoclgaf 3464 . . . . . . . . . . . . . . . . . 18 (⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
14860, 147mpcom 38 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
14939, 43, 148chvar 2436 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
150 poimir.0 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℕ)
151150nnnn0d 11617 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
152 nn0uz 11940 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
153151, 152syl6eleq 2895 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘0))
154 fzm1 12643 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘0) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
155153, 154syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
156155adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
157149, 156mpbid 223 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
158157ord 882 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → (¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
15936, 158mt3d 142 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
160159adantrr 699 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
161 fzfi 12995 . . . . . . . . . . . . . . 15 (0...(𝑁 − 1)) ∈ Fin
162150nncnd 11321 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
163 1cnd 10320 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 1 ∈ ℂ)
164162, 163, 163addsubd 10698 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 + 1) − 1) = ((𝑁 − 1) + 1))
165 hashfz0 13436 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (♯‘(0...𝑁)) = (𝑁 + 1))
166151, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1))
167166oveq1d 6889 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((♯‘(0...𝑁)) − 1) = ((𝑁 + 1) − 1))
168 nnm1nn0 11600 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
169 hashfz0 13436 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ ℕ0 → (♯‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1))
170150, 168, 1693syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1))
171164, 167, 1703eqtr4rd 2851 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(0...(𝑁 − 1))) = ((♯‘(0...𝑁)) − 1))
172 hashdifsn 13419 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) ∈ Fin ∧ 𝑡 ∈ (0...𝑁)) → (♯‘((0...𝑁) ∖ {𝑡})) = ((♯‘(0...𝑁)) − 1))
1738, 172mpan 673 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0...𝑁) → (♯‘((0...𝑁) ∖ {𝑡})) = ((♯‘(0...𝑁)) − 1))
174173eqcomd 2812 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0...𝑁) → ((♯‘(0...𝑁)) − 1) = (♯‘((0...𝑁) ∖ {𝑡})))
175171, 174sylan9eq 2860 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → (♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})))
176 diffi 8431 . . . . . . . . . . . . . . . . . 18 ((0...𝑁) ∈ Fin → ((0...𝑁) ∖ {𝑡}) ∈ Fin)
1778, 176ax-mp 5 . . . . . . . . . . . . . . . . 17 ((0...𝑁) ∖ {𝑡}) ∈ Fin
178 hashen 13355 . . . . . . . . . . . . . . . . 17 (((0...(𝑁 − 1)) ∈ Fin ∧ ((0...𝑁) ∖ {𝑡}) ∈ Fin) → ((♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})))
179161, 177, 178mp2an 675 . . . . . . . . . . . . . . . 16 ((♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))
180175, 179sylib 209 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))
181 phpreu 33706 . . . . . . . . . . . . . . 15 (((0...(𝑁 − 1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
182161, 180, 181sylancr 577 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
183182biimpd 220 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
184183impr 444 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
185 nfv 2005 . . . . . . . . . . . . . . 15 𝑧 𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶
186 nfcsb1v 3744 . . . . . . . . . . . . . . . 16 𝑗𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
187186nfeq2 2964 . . . . . . . . . . . . . . 15 𝑗 𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
188 csbeq1a 3737 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑧𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
189188eqeq2d 2816 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
190185, 187, 189cbvreu 3358 . . . . . . . . . . . . . 14 (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
191 eqeq1 2810 . . . . . . . . . . . . . . 15 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
192191reubidv 3315 . . . . . . . . . . . . . 14 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
193190, 192syl5bb 274 . . . . . . . . . . . . 13 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
194193rspcv 3498 . . . . . . . . . . . 12 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
195160, 184, 194sylc 65 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
196 an32 628 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
197196biimpi 207 . . . . . . . . . . . . . . 15 (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
198197adantll 696 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
199 eqeq2 2817 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
200 rexsns 4410 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
20129nfeq2 2964 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗 𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
20231eqeq2d 2816 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑡 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
203201, 202sbciegf 3665 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ V → ([𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
2047, 203ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
205200, 204bitri 266 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
206 rexsns 4410 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
207 vex 3394 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
208187, 189sbciegf 3665 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ V → ([𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
209207, 208ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
210206, 209bitri 266 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
211199, 205, 2103bitr4g 305 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
212211orbi1d 931 . . . . . . . . . . . . . . . . . . . 20 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ((∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
213 rexun 3992 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
214 rexun 3992 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
215212, 213, 2143bitr4g 305 . . . . . . . . . . . . . . . . . . 19 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
216215adantl 469 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
217 eldifsni 4512 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧𝑡)
218217necomd 3033 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑡𝑧)
219 dif32 4092 . . . . . . . . . . . . . . . . . . . . . . 23 (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) = (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})
220219uneq2i 3963 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}))
221 snssi 4529 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → {𝑡} ⊆ ((0...𝑁) ∖ {𝑧}))
222 eldifsn 4508 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) ↔ (𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧))
223 undif 4245 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑡} ⊆ ((0...𝑁) ∖ {𝑧}) ↔ ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧}))
224221, 222, 2233imtr3i 282 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧}))
225220, 224syl5eq 2852 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧}))
226218, 225sylan2 582 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧}))
227226rexeqdv 3334 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
228227adantr 468 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
229 snssi 4529 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → {𝑧} ⊆ ((0...𝑁) ∖ {𝑡}))
230 undif 4245 . . . . . . . . . . . . . . . . . . . . 21 ({𝑧} ⊆ ((0...𝑁) ∖ {𝑡}) ↔ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡}))
231229, 230sylib 209 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡}))
232231rexeqdv 3334 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
233232ad2antlr 709 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
234216, 228, 2333bitr3d 300 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
235234ralbidv 3174 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
236235biimpar 465 . . . . . . . . . . . . . . 15 ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
237236an32s 634 . . . . . . . . . . . . . 14 ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
238198, 237sylan 571 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
239 simpl 470 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 ∈ (0...𝑁))
240239anim2i 605 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (𝜑𝑡 ∈ (0...𝑁)))
241 necom 3031 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑡𝑡𝑧)
242241biimpi 207 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝑡𝑡𝑧)
243242adantl 469 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) → 𝑡𝑧)
244243anim2i 605 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡)) → (𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧))
245 eldifsn 4508 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ↔ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡))
246245anbi2i 611 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ (𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡)))
247244, 246, 2223imtr4i 283 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
248247adantll 696 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
249248adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
25029nfel1 2963 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))
25137, 250nfim 1987 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
25231eleq1d 2870 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑡 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))))
25341, 252imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑡 → (((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))) ↔ ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))))
25426necomd 3033 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶𝑁)
255254neneqd 2983 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → ¬ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
256 fzm1 12643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘0) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
257153, 256syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
258257adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
259148, 258mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
260259ord 882 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (¬ 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
261255, 260mt3d 142 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
262251, 253, 261chvar 2436 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
263262ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
264 eldifi 3931 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧 ∈ (0...𝑁))
265 eleq1w 2868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑧 → (𝑡 ∈ (0...𝑁) ↔ 𝑧 ∈ (0...𝑁)))
266265anbi2d 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑧 → ((𝜑𝑡 ∈ (0...𝑁)) ↔ (𝜑𝑧 ∈ (0...𝑁))))
267 sneq 4380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 𝑧 → {𝑡} = {𝑧})
268267difeq2d 3927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑧 → ((0...𝑁) ∖ {𝑡}) = ((0...𝑁) ∖ {𝑧}))
269268breq2d 4856 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑧 → ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})))
270266, 269imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑧 → (((𝜑𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝜑𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))))
271270, 180chvarv 2437 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
272264, 271sylan2 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
273272adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
274 phpreu 33706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0...(𝑁 − 1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
275161, 274mpan 673 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
276275biimpa 464 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
277273, 276sylan 571 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
278 eqeq1 2810 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
279278adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑗 ∈ ((0...𝑁) ∖ {𝑧})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
280201, 279reubida 3313 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
281280rspcv 3498 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
282263, 277, 281sylc 65 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
283 reurmo 3350 . . . . . . . . . . . . . . . . . . . . . 22 (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
284282, 283syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
285 nfv 2005 . . . . . . . . . . . . . . . . . . . . . 22 𝑖𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶
286285rmo3 3723 . . . . . . . . . . . . . . . . . . . . 21 (∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖))
287284, 286sylib 209 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖))
288 equcomi 2113 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑡𝑡 = 𝑖)
289288csbeq1d 3735 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑡𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
290 sbsbc 3637 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
291 vex 3394 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑖 ∈ V
292 sbceqg 4181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ V → ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
29329csbconstgf 3740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ V → 𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
294293eqeq1d 2808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ V → (𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
295292, 294bitrd 270 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ V → ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
296291, 295ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
297290, 296bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
298289, 297sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑡 → [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
299298biantrud 523 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑡 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
300299bicomd 214 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑡 → ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
301 eqeq2 2817 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑡 → (𝑗 = 𝑖𝑗 = 𝑡))
302300, 301imbi12d 335 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑡 → (((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
303302rspcv 3498 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
304303ralimdv 3151 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
305249, 287, 304sylc 65 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡))
306 dif32 4092 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) = (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})
307306eleq2i 2877 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ 𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))
308 eldifsn 4508 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡))
309 eldifsn 4508 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧))
310307, 308, 3093bitr3ri 293 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡))
311310imbi1i 340 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
312 impexp 439 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
313 impexp 439 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
314311, 312, 3133bitr3ri 293 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
315314albii 1904 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
316 con34b 307 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ (¬ 𝑗 = 𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
317 df-ne 2979 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑡 ↔ ¬ 𝑗 = 𝑡)
318317imbi1i 340 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (¬ 𝑗 = 𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
319316, 318bitr4i 269 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
320319ralbii 3168 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
321 df-ral 3101 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
322320, 321bitri 266 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
323 df-ral 3101 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
324315, 322, 3233bitr4i 294 . . . . . . . . . . . . . . . . . . 19 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
325305, 324sylib 209 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
326 df-ne 2979 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗𝑧 ↔ ¬ 𝑗 = 𝑧)
327326imbi1i 340 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (¬ 𝑗 = 𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
328 con34b 307 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧) ↔ (¬ 𝑗 = 𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
329327, 328bitr4i 269 . . . . . . . . . . . . . . . . . . . 20 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧))
330 ancr 538 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
331329, 330sylbi 208 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
332331ralimi 3140 . . . . . . . . . . . . . . . . . 18 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
333325, 332syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
334240, 333sylanl1 662 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
335201, 278rexbid 3239 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
336335rspcva 3500 . . . . . . . . . . . . . . . . . . 19 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
337262, 336sylan 571 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡 ∈ (0...𝑁)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
338337anasss 454 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
339338ad2antrr 708 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
340 rexim 3195 . . . . . . . . . . . . . . . 16 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
341334, 339, 340sylc 65 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
342 rexex 3189 . . . . . . . . . . . . . . 15 (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
343341, 342syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
34429, 186nfeq 2960 . . . . . . . . . . . . . . 15 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
345188eqeq2d 2816 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
346344, 345equsexv 2277 . . . . . . . . . . . . . 14 (∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
347343, 346sylib 209 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
348238, 347impbida 826 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
349348reubidva 3314 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
350195, 349mpbid 223 . . . . . . . . . 10 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
351 an32 628 . . . . . . . . . . . . . 14 (((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧𝑡))
352245anbi1i 612 . . . . . . . . . . . . . 14 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
353 sneq 4380 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → {𝑦} = {𝑧})
354353difeq2d 3927 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑧}))
355354rexeqdv 3334 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
356355ralbidv 3174 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
357356elrab 3559 . . . . . . . . . . . . . . 15 (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ↔ (𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
358357anbi1i 612 . . . . . . . . . . . . . 14 ((𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧𝑡))
359351, 352, 3583bitr4i 294 . . . . . . . . . . . . 13 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡))
360 eldifsn 4508 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡))
361359, 360bitr4i 269 . . . . . . . . . . . 12 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
362361eubii 2654 . . . . . . . . . . 11 (∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
363 df-reu 3103 . . . . . . . . . . 11 (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
364 euhash1 13425 . . . . . . . . . . . 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 294 . . . . . . . . . 10 (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
367350, 366sylib 209 . . . . . . . . 9 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
36825, 367sylan2b 583 . . . . . . . 8 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
369368oveq1d 6889 . . . . . . 7 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (1 + 1))
37020, 369eqtr3d 2842 . . . . . 6 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) = (1 + 1))
3716, 370syl5breqr 4882 . . . . 5 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
372371ex 399 . . . 4 (𝜑 → (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
373372exlimdv 2024 . . 3 (𝜑 → (∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
3741, 373syl5bi 233 . 2 (𝜑 → (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
375 dvds0 15220 . . . . 5 (2 ∈ ℤ → 2 ∥ 0)
3762, 375ax-mp 5 . . . 4 2 ∥ 0
377 hash0 13376 . . . 4 (♯‘∅) = 0
378376, 377breqtrri 4871 . . 3 2 ∥ (♯‘∅)
379 fveq2 6408 . . 3 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) = (♯‘∅))
380378, 379syl5breqr 4882 . 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 197  wa 384  wo 865  wal 1635   = wceq 1637  wex 1859  [wsb 2060  wcel 2156  ∃!weu 2630  {cab 2792  wne 2978  wral 3096  wrex 3097  ∃!wreu 3098  ∃*wrmo 3099  {crab 3100  Vcvv 3391  [wsbc 3633  csb 3728  cdif 3766  cun 3767  cin 3768  wss 3769  c0 4116  {csn 4370  cop 4376   class class class wbr 4844   × cxp 5309  ccnv 5310  cima 5314  Fun wfun 6095  wf 6097  ontowfo 6099  1-1-ontowf1o 6100  cfv 6101  (class class class)co 6874  𝑓 cof 7125  1st c1st 7396  2nd c2nd 7397  𝑚 cmap 8092  cen 8189  Fincfn 8192  0cc0 10221  1c1 10222   + caddc 10224   < clt 10359  cmin 10551  cn 11305  2c2 11356  0cn0 11559  cz 11643  cuz 11904  ...cfz 12549  ..^cfzo 12689  chash 13337  cdvds 15203
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-of 7127  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-oadd 7800  df-er 7979  df-map 8094  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-card 9048  df-cda 9275  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-nn 11306  df-2 11364  df-n0 11560  df-z 11644  df-uz 11905  df-fz 12550  df-fzo 12690  df-hash 13338  df-dvds 15204
This theorem is referenced by:  poimirlem26  33748
  Copyright terms: Public domain W3C validator