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 4073 . . 3 (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ ↔ ∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})
2 2z 11601 . . . . . . . 8 2 ∈ ℤ
3 iddvds 15197 . . . . . . . 8 (2 ∈ ℤ → 2 ∥ 2)
42, 3ax-mp 5 . . . . . . 7 2 ∥ 2
5 df-2 11271 . . . . . . 7 2 = (1 + 1)
64, 5breqtri 4829 . . . . . 6 2 ∥ (1 + 1)
7 vex 3343 . . . . . . . . . 10 𝑡 ∈ V
8 fzfi 12965 . . . . . . . . . . . . 13 (0...𝑁) ∈ Fin
9 rabfi 8350 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin → {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin)
108, 9ax-mp 5 . . . . . . . . . . . 12 {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin
11 diffi 8357 . . . . . . . . . . . 12 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin → ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin)
1210, 11ax-mp 5 . . . . . . . . . . 11 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin
13 neldifsn 4467 . . . . . . . . . . 11 ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})
1412, 13pm3.2i 470 . . . . . . . . . 10 (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin ∧ ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
15 hashunsng 13373 . . . . . . . . . 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 4486 . . . . . . . . . 10 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡}) = {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})
1817fveq2d 6356 . . . . . . . . 9 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → (♯‘(({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡})) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
1916, 18syl5eqr 2808 . . . . . . . 8 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
2019adantl 473 . . . . . . 7 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
21 sneq 4331 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → {𝑦} = {𝑡})
2221difeq2d 3871 . . . . . . . . . . . 12 (𝑦 = 𝑡 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑡}))
2322rexeqdv 3284 . . . . . . . . . . 11 (𝑦 = 𝑡 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
2423ralbidv 3124 . . . . . . . . . 10 (𝑦 = 𝑡 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
2524elrab 3504 . . . . . . . . 9 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ↔ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
26 poimirlem25.5 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑁𝑇, 𝑈⟩ / 𝑠𝐶)
2726ralrimiva 3104 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑗 ∈ (0...𝑁)𝑁𝑇, 𝑈⟩ / 𝑠𝐶)
28 nfcv 2902 . . . . . . . . . . . . . . . . . 18 𝑗𝑁
29 nfcsb1v 3690 . . . . . . . . . . . . . . . . . 18 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
3028, 29nfne 3032 . . . . . . . . . . . . . . . . 17 𝑗 𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
31 csbeq1a 3683 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
3231neeq2d 2992 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑡 → (𝑁𝑇, 𝑈⟩ / 𝑠𝐶𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
3330, 32rspc 3443 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0...𝑁) → (∀𝑗 ∈ (0...𝑁)𝑁𝑇, 𝑈⟩ / 𝑠𝐶𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
3427, 33mpan9 487 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
35 nesym 2988 . . . . . . . . . . . . . . 15 (𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
3634, 35sylib 208 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
37 nfv 1992 . . . . . . . . . . . . . . . . . 18 𝑗(𝜑𝑡 ∈ (0...𝑁))
3829nfel1 2917 . . . . . . . . . . . . . . . . . 18 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)
3937, 38nfim 1974 . . . . . . . . . . . . . . . . 17 𝑗((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
40 eleq1w 2822 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑡 → (𝑗 ∈ (0...𝑁) ↔ 𝑡 ∈ (0...𝑁)))
4140anbi2d 742 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡 → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡 ∈ (0...𝑁))))
4231eleq1d 2824 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
4341, 42imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑡 → (((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)) ↔ ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))))
44 poimirlem25.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
45 ovex 6841 . . . . . . . . . . . . . . . . . . . . . 22 (0..^𝐾) ∈ V
46 ovex 6841 . . . . . . . . . . . . . . . . . . . . . 22 (1...𝑁) ∈ V
4745, 46elmap 8052 . . . . . . . . . . . . . . . . . . . . 21 (𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) ↔ 𝑇:(1...𝑁)⟶(0..^𝐾))
4844, 47sylibr 224 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
49 poimirlem25.4 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
50 fzfi 12965 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑁) ∈ Fin
51 f1oexrnex 7280 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ Fin) → 𝑈 ∈ V)
5250, 51mpan2 709 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ V)
53 f1oeq1 6288 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑈 → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)))
5453elabg 3491 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈 ∈ V → (𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)))
5552, 54syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → (𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)))
5655ibir 257 . . . . . . . . . . . . . . . . . . . . 21 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
5749, 56syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
58 opelxpi 5305 . . . . . . . . . . . . . . . . . . . 20 ((𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) ∧ 𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
5948, 57, 58syl2anc 696 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
6059adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
61 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑠𝑇, 𝑈
62 nfv 1992 . . . . . . . . . . . . . . . . . . . 20 𝑠(𝜑𝑗 ∈ (0...𝑁))
63 nfcsb1v 3690 . . . . . . . . . . . . . . . . . . . . 21 𝑠𝑇, 𝑈⟩ / 𝑠𝐶
6463nfel1 2917 . . . . . . . . . . . . . . . . . . . 20 𝑠𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)
6562, 64nfim 1974 . . . . . . . . . . . . . . . . . . 19 𝑠((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
66 csbeq1a 3683 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ⟨𝑇, 𝑈⟩ → 𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
6766eleq1d 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ⟨𝑇, 𝑈⟩ → (𝐶 ∈ (0...𝑁) ↔ 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
6867imbi2d 329 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ⟨𝑇, 𝑈⟩ → (((𝜑𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁)) ↔ ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))))
69 elun 3896 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 ∈ ({1} ∪ {0}) ↔ (𝑝 ∈ {1} ∨ 𝑝 ∈ {0}))
70 fzofzp1 12759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝐾) → (𝑖 + 1) ∈ (0...𝐾))
71 elsni 4338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ {1} → 𝑝 = 1)
7271oveq2d 6829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ {1} → (𝑖 + 𝑝) = (𝑖 + 1))
7372eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ {1} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 1) ∈ (0...𝐾)))
7470, 73syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {1} → (𝑖 + 𝑝) ∈ (0...𝐾)))
75 elfzonn0 12707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℕ0)
7675nn0cnd 11545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℂ)
7776addid1d 10428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) = 𝑖)
78 elfzofz 12679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ (0...𝐾))
7977, 78eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) ∈ (0...𝐾))
80 elsni 4338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ {0} → 𝑝 = 0)
8180oveq2d 6829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ {0} → (𝑖 + 𝑝) = (𝑖 + 0))
8281eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ {0} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 0) ∈ (0...𝐾)))
8379, 82syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {0} → (𝑖 + 𝑝) ∈ (0...𝐾)))
8474, 83jaod 394 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝐾) → ((𝑝 ∈ {1} ∨ 𝑝 ∈ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾)))
8569, 84syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ ({1} ∪ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾)))
8685imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0})) → (𝑖 + 𝑝) ∈ (0...𝐾))
8786adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0}))) → (𝑖 + 𝑝) ∈ (0...𝐾))
88 xp1st 7365 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
89 elmapi 8045 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑠) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
9190adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
92 xp2nd 7366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd𝑠) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
93 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (2nd𝑠) ∈ V
94 f1oeq1 6288 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = (2nd𝑠) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁)))
9593, 94elab 3490 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd𝑠) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁))
9692, 95sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁))
97 1ex 10227 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ V
9897fconst 6252 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((2nd𝑠) “ (1...𝑗)) × {1}):((2nd𝑠) “ (1...𝑗))⟶{1}
99 c0ex 10226 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 ∈ V
10099fconst 6252 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd𝑠) “ ((𝑗 + 1)...𝑁))⟶{0}
10198, 100pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((2nd𝑠) “ (1...𝑗)) × {1}):((2nd𝑠) “ (1...𝑗))⟶{1} ∧ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd𝑠) “ ((𝑗 + 1)...𝑁))⟶{0})
102 dff1o3 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd𝑠):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd𝑠)))
103 imain 6135 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun (2nd𝑠) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))))
104102, 103simplbiim 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))))
105 elfznn0 12626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
106105nn0red 11544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
107106ltp1d 11146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
108 fzdisj 12561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
110109imaeq2d 5624 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd𝑠) “ ∅))
111 ima0 5639 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠) “ ∅) = ∅
112110, 111syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
113104, 112sylan9req 2815 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = ∅)
114 fun 6227 . . . . . . . . . . . . . . . . . . . . . . . . . 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 698 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
116 nn0p1nn 11524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
117105, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
118 nnuz 11916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℕ = (ℤ‘1)
119117, 118syl6eleq 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
120 elfzuz3 12532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
121 fzsplit2 12559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
122119, 120, 121syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
123122imaeq2d 5624 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ (1...𝑁)) = ((2nd𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
124 imaundi 5703 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))
125123, 124syl6req 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = ((2nd𝑠) “ (1...𝑁)))
126 f1ofo 6305 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd𝑠):(1...𝑁)–onto→(1...𝑁))
127 foima 6281 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–onto→(1...𝑁) → ((2nd𝑠) “ (1...𝑁)) = (1...𝑁))
128126, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd𝑠) “ (1...𝑁)) = (1...𝑁))
129125, 128sylan9eqr 2816 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
130129feq2d 6192 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
131115, 130mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
13296, 131sylan 489 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
133 fzfid 12966 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
134 inidm 3965 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
13587, 91, 132, 133, 133, 134off 7077 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
136 ovex 6841 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
137 feq1 6187 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝:(1...𝑁)⟶(0...𝐾) ↔ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
138137anbi2d 742 . . . . . . . . . . . . . . . . . . . . . . . 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 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐵 ∈ (0...𝑁) ↔ 𝐶 ∈ (0...𝑁)))
141138, 140imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁)) ↔ ((𝜑 ∧ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → 𝐶 ∈ (0...𝑁))))
142 poimirlem28.2 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))
143136, 141, 142vtocl 3399 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → 𝐶 ∈ (0...𝑁))
144135, 143sylan2 492 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁))
145144an12s 878 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (𝜑𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁))
146145ex 449 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁)))
14761, 65, 68, 146vtoclgaf 3411 . . . . . . . . . . . . . . . . . 18 (⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
14860, 147mpcom 38 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
14939, 43, 148chvar 2407 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
150 poimir.0 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℕ)
151150nnnn0d 11543 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
152 nn0uz 11915 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
153151, 152syl6eleq 2849 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘0))
154 fzm1 12613 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘0) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
155153, 154syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
156155adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
157149, 156mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
158157ord 391 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → (¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
15936, 158mt3d 140 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
160159adantrr 755 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
161 fzfi 12965 . . . . . . . . . . . . . . 15 (0...(𝑁 − 1)) ∈ Fin
162150nncnd 11228 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
163 1cnd 10248 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 1 ∈ ℂ)
164162, 163, 163addsubd 10605 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 + 1) − 1) = ((𝑁 − 1) + 1))
165 hashfz0 13411 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (♯‘(0...𝑁)) = (𝑁 + 1))
166151, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1))
167166oveq1d 6828 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((♯‘(0...𝑁)) − 1) = ((𝑁 + 1) − 1))
168 nnm1nn0 11526 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
169 hashfz0 13411 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ ℕ0 → (♯‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1))
170150, 168, 1693syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1))
171164, 167, 1703eqtr4rd 2805 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(0...(𝑁 − 1))) = ((♯‘(0...𝑁)) − 1))
172 hashdifsn 13394 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) ∈ Fin ∧ 𝑡 ∈ (0...𝑁)) → (♯‘((0...𝑁) ∖ {𝑡})) = ((♯‘(0...𝑁)) − 1))
1738, 172mpan 708 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0...𝑁) → (♯‘((0...𝑁) ∖ {𝑡})) = ((♯‘(0...𝑁)) − 1))
174173eqcomd 2766 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0...𝑁) → ((♯‘(0...𝑁)) − 1) = (♯‘((0...𝑁) ∖ {𝑡})))
175171, 174sylan9eq 2814 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → (♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})))
176 diffi 8357 . . . . . . . . . . . . . . . . . 18 ((0...𝑁) ∈ Fin → ((0...𝑁) ∖ {𝑡}) ∈ Fin)
1778, 176ax-mp 5 . . . . . . . . . . . . . . . . 17 ((0...𝑁) ∖ {𝑡}) ∈ Fin
178 hashen 13329 . . . . . . . . . . . . . . . . 17 (((0...(𝑁 − 1)) ∈ Fin ∧ ((0...𝑁) ∖ {𝑡}) ∈ Fin) → ((♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})))
179161, 177, 178mp2an 710 . . . . . . . . . . . . . . . 16 ((♯‘(0...(𝑁 − 1))) = (♯‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))
180175, 179sylib 208 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))
181 phpreu 33706 . . . . . . . . . . . . . . 15 (((0...(𝑁 − 1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
182161, 180, 181sylancr 698 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
183182biimpd 219 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
184183impr 650 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
185 nfv 1992 . . . . . . . . . . . . . . 15 𝑧 𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶
186 nfcsb1v 3690 . . . . . . . . . . . . . . . 16 𝑗𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
187186nfeq2 2918 . . . . . . . . . . . . . . 15 𝑗 𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
188 csbeq1a 3683 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑧𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
189188eqeq2d 2770 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
190185, 187, 189cbvreu 3308 . . . . . . . . . . . . . 14 (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
191 eqeq1 2764 . . . . . . . . . . . . . . 15 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
192191reubidv 3265 . . . . . . . . . . . . . 14 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
193190, 192syl5bb 272 . . . . . . . . . . . . 13 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
194193rspcv 3445 . . . . . . . . . . . 12 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
195160, 184, 194sylc 65 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
196 an32 874 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
197196biimpi 206 . . . . . . . . . . . . . . 15 (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
198197adantll 752 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
199 eqeq2 2771 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
200 rexsns 4361 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
20129nfeq2 2918 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗 𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
20231eqeq2d 2770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑡 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
203201, 202sbciegf 3608 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ V → ([𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
2047, 203ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
205200, 204bitri 264 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
206 rexsns 4361 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
207 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
208187, 189sbciegf 3608 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ V → ([𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
209207, 208ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
210206, 209bitri 264 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
211199, 205, 2103bitr4g 303 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
212211orbi1d 741 . . . . . . . . . . . . . . . . . . . 20 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ((∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
213 rexun 3936 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
214 rexun 3936 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
215212, 213, 2143bitr4g 303 . . . . . . . . . . . . . . . . . . 19 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
216215adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
217 eldifsni 4466 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧𝑡)
218217necomd 2987 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑡𝑧)
219 dif32 4034 . . . . . . . . . . . . . . . . . . . . . . 23 (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) = (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})
220219uneq2i 3907 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}))
221 snssi 4484 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → {𝑡} ⊆ ((0...𝑁) ∖ {𝑧}))
222 eldifsn 4462 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) ↔ (𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧))
223 undif 4193 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑡} ⊆ ((0...𝑁) ∖ {𝑧}) ↔ ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧}))
224221, 222, 2233imtr3i 280 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧}))
225220, 224syl5eq 2806 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧}))
226218, 225sylan2 492 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧}))
227226rexeqdv 3284 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
228227adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
229 snssi 4484 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → {𝑧} ⊆ ((0...𝑁) ∖ {𝑡}))
230 undif 4193 . . . . . . . . . . . . . . . . . . . . 21 ({𝑧} ⊆ ((0...𝑁) ∖ {𝑡}) ↔ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡}))
231229, 230sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡}))
232231rexeqdv 3284 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
233232ad2antlr 765 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
234216, 228, 2333bitr3d 298 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
235234ralbidv 3124 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
236235biimpar 503 . . . . . . . . . . . . . . 15 ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
237236an32s 881 . . . . . . . . . . . . . 14 ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
238198, 237sylan 489 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
239 simpl 474 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 ∈ (0...𝑁))
240239anim2i 594 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (𝜑𝑡 ∈ (0...𝑁)))
241 necom 2985 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑡𝑡𝑧)
242241biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝑡𝑡𝑧)
243242adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) → 𝑡𝑧)
244243anim2i 594 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡)) → (𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧))
245 eldifsn 4462 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ↔ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡))
246245anbi2i 732 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ (𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡)))
247244, 246, 2223imtr4i 281 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
248247adantll 752 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
249248adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
25029nfel1 2917 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))
25137, 250nfim 1974 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
25231eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑡 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))))
25341, 252imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑡 → (((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))) ↔ ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))))
25426necomd 2987 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶𝑁)
255254neneqd 2937 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → ¬ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
256 fzm1 12613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘0) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
257153, 256syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
258257adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
259148, 258mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
260259ord 391 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (¬ 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
261255, 260mt3d 140 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
262251, 253, 261chvar 2407 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
263262ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
264 eldifi 3875 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧 ∈ (0...𝑁))
265 eleq1w 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑧 → (𝑡 ∈ (0...𝑁) ↔ 𝑧 ∈ (0...𝑁)))
266265anbi2d 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑧 → ((𝜑𝑡 ∈ (0...𝑁)) ↔ (𝜑𝑧 ∈ (0...𝑁))))
267 sneq 4331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 𝑧 → {𝑡} = {𝑧})
268267difeq2d 3871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑧 → ((0...𝑁) ∖ {𝑡}) = ((0...𝑁) ∖ {𝑧}))
269268breq2d 4816 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑧 → ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})))
270266, 269imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑧 → (((𝜑𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝜑𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))))
271270, 180chvarv 2408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
272264, 271sylan2 492 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
273272adantlr 753 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
274 phpreu 33706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0...(𝑁 − 1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
275161, 274mpan 708 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
276275biimpa 502 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
277273, 276sylan 489 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
278 eqeq1 2764 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
279278adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑗 ∈ ((0...𝑁) ∖ {𝑧})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
280201, 279reubida 3263 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
281280rspcv 3445 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
282263, 277, 281sylc 65 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
283 reurmo 3300 . . . . . . . . . . . . . . . . . . . . . 22 (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
284282, 283syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
285 nfv 1992 . . . . . . . . . . . . . . . . . . . . . 22 𝑖𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶
286285rmo3 3669 . . . . . . . . . . . . . . . . . . . . 21 (∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖))
287284, 286sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖))
288 equcomi 2099 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑡𝑡 = 𝑖)
289288csbeq1d 3681 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑡𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
290 sbsbc 3580 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
291 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑖 ∈ V
292 sbceqg 4127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ V → ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
29329csbconstgf 3686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ V → 𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
294293eqeq1d 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ V → (𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
295292, 294bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ V → ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
296291, 295ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
297290, 296bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
298289, 297sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑡 → [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
299298biantrud 529 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑡 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
300299bicomd 213 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑡 → ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
301 eqeq2 2771 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑡 → (𝑗 = 𝑖𝑗 = 𝑡))
302300, 301imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑡 → (((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
303302rspcv 3445 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
304303ralimdv 3101 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
305249, 287, 304sylc 65 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡))
306 dif32 4034 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) = (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})
307306eleq2i 2831 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ 𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))
308 eldifsn 4462 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡))
309 eldifsn 4462 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧))
310307, 308, 3093bitr3ri 291 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡))
311310imbi1i 338 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
312 impexp 461 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
313 impexp 461 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
314311, 312, 3133bitr3ri 291 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
315314albii 1896 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
316 con34b 305 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ (¬ 𝑗 = 𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
317 df-ne 2933 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑡 ↔ ¬ 𝑗 = 𝑡)
318317imbi1i 338 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (¬ 𝑗 = 𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
319316, 318bitr4i 267 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
320319ralbii 3118 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
321 df-ral 3055 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
322320, 321bitri 264 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
323 df-ral 3055 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
324315, 322, 3233bitr4i 292 . . . . . . . . . . . . . . . . . . 19 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
325305, 324sylib 208 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
326 df-ne 2933 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗𝑧 ↔ ¬ 𝑗 = 𝑧)
327326imbi1i 338 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (¬ 𝑗 = 𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
328 con34b 305 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧) ↔ (¬ 𝑗 = 𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
329327, 328bitr4i 267 . . . . . . . . . . . . . . . . . . . 20 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧))
330 ancr 573 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
331329, 330sylbi 207 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
332331ralimi 3090 . . . . . . . . . . . . . . . . . 18 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
333325, 332syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
334240, 333sylanl1 685 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
335201, 278rexbid 3189 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
336335rspcva 3447 . . . . . . . . . . . . . . . . . . 19 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
337262, 336sylan 489 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡 ∈ (0...𝑁)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
338337anasss 682 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
339338ad2antrr 764 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
340 rexim 3146 . . . . . . . . . . . . . . . 16 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
341334, 339, 340sylc 65 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
342 rexex 3140 . . . . . . . . . . . . . . 15 (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
343341, 342syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
34429, 186nfeq 2914 . . . . . . . . . . . . . . 15 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
345188eqeq2d 2770 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
346344, 345equsexv 2256 . . . . . . . . . . . . . 14 (∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
347343, 346sylib 208 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
348238, 347impbida 913 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
349348reubidva 3264 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
350195, 349mpbid 222 . . . . . . . . . 10 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
351 an32 874 . . . . . . . . . . . . . 14 (((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧𝑡))
352245anbi1i 733 . . . . . . . . . . . . . 14 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
353 sneq 4331 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → {𝑦} = {𝑧})
354353difeq2d 3871 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑧}))
355354rexeqdv 3284 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
356355ralbidv 3124 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
357356elrab 3504 . . . . . . . . . . . . . . 15 (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ↔ (𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
358357anbi1i 733 . . . . . . . . . . . . . 14 ((𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧𝑡))
359351, 352, 3583bitr4i 292 . . . . . . . . . . . . 13 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡))
360 eldifsn 4462 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡))
361359, 360bitr4i 267 . . . . . . . . . . . 12 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
362361eubii 2629 . . . . . . . . . . 11 (∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
363 df-reu 3057 . . . . . . . . . . 11 (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
364 euhash1 13400 . . . . . . . . . . . 12 (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1 ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})))
36512, 364ax-mp 5 . . . . . . . . . . 11 ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1 ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
366362, 363, 3653bitr4i 292 . . . . . . . . . 10 (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
367350, 366sylib 208 . . . . . . . . 9 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
36825, 367sylan2b 493 . . . . . . . 8 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → (♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
369368oveq1d 6828 . . . . . . 7 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → ((♯‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (1 + 1))
37020, 369eqtr3d 2796 . . . . . 6 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) = (1 + 1))
3716, 370syl5breqr 4842 . . . . 5 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
372371ex 449 . . . 4 (𝜑 → (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
373372exlimdv 2010 . . 3 (𝜑 → (∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
3741, 373syl5bi 232 . 2 (𝜑 → (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
375 dvds0 15199 . . . . 5 (2 ∈ ℤ → 2 ∥ 0)
3762, 375ax-mp 5 . . . 4 2 ∥ 0
377 hash0 13350 . . . 4 (♯‘∅) = 0
378376, 377breqtrri 4831 . . 3 2 ∥ (♯‘∅)
379 fveq2 6352 . . 3 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) = (♯‘∅))
380378, 379syl5breqr 4842 . 2 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
381374, 380pm2.61d2 172 1 (𝜑 → 2 ∥ (♯‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383  ∀wal 1630   = wceq 1632  ∃wex 1853  [wsb 2046   ∈ wcel 2139  ∃!weu 2607  {cab 2746   ≠ wne 2932  ∀wral 3050  ∃wrex 3051  ∃!wreu 3052  ∃*wrmo 3053  {crab 3054  Vcvv 3340  [wsbc 3576  ⦋csb 3674   ∖ cdif 3712   ∪ cun 3713   ∩ cin 3714   ⊆ wss 3715  ∅c0 4058  {csn 4321  ⟨cop 4327   class class class wbr 4804   × cxp 5264  ◡ccnv 5265   “ cima 5269  Fun wfun 6043  ⟶wf 6045  –onto→wfo 6047  –1-1-onto→wf1o 6048  ‘cfv 6049  (class class class)co 6813   ∘𝑓 cof 7060  1st c1st 7331  2nd c2nd 7332   ↑𝑚 cmap 8023   ≈ cen 8118  Fincfn 8121  0cc0 10128  1c1 10129   + caddc 10131   < clt 10266   − cmin 10458  ℕcn 11212  2c2 11262  ℕ0cn0 11484  ℤcz 11569  ℤ≥cuz 11879  ...cfz 12519  ..^cfzo 12659  ♯chash 13311   ∥ cdvds 15182 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-2 11271  df-n0 11485  df-z 11570  df-uz 11880  df-fz 12520  df-fzo 12660  df-hash 13312  df-dvds 15183 This theorem is referenced by:  poimirlem26  33748
 Copyright terms: Public domain W3C validator