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

Theorem poimirlem25 32604
 Description: Lemma for poimir 32612 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 3889 . . 3 (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ ↔ ∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})
2 2z 11286 . . . . . . . 8 2 ∈ ℤ
3 iddvds 14833 . . . . . . . 8 (2 ∈ ℤ → 2 ∥ 2)
42, 3ax-mp 5 . . . . . . 7 2 ∥ 2
5 df-2 10956 . . . . . . 7 2 = (1 + 1)
64, 5breqtri 4608 . . . . . 6 2 ∥ (1 + 1)
7 vex 3176 . . . . . . . . . 10 𝑡 ∈ V
8 fzfi 12633 . . . . . . . . . . . . 13 (0...𝑁) ∈ Fin
9 rabfi 8070 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin → {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin)
108, 9ax-mp 5 . . . . . . . . . . . 12 {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin
11 diffi 8077 . . . . . . . . . . . 12 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∈ Fin → ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin)
1210, 11ax-mp 5 . . . . . . . . . . 11 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin
13 neldifsn 4262 . . . . . . . . . . 11 ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})
1412, 13pm3.2i 470 . . . . . . . . . 10 (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∈ Fin ∧ ¬ 𝑡 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
15 hashunsng 13042 . . . . . . . . . 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 4282 . . . . . . . . . 10 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → (({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡}) = {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})
1817fveq2d 6107 . . . . . . . . 9 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → (#‘(({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ∪ {𝑡})) = (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
1916, 18syl5eqr 2658 . . . . . . . 8 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → ((#‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
2019adantl 481 . . . . . . 7 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → ((#‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
21 sneq 4135 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → {𝑦} = {𝑡})
2221difeq2d 3690 . . . . . . . . . . . 12 (𝑦 = 𝑡 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑡}))
2322rexeqdv 3122 . . . . . . . . . . 11 (𝑦 = 𝑡 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
2423ralbidv 2969 . . . . . . . . . 10 (𝑦 = 𝑡 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
2524elrab 3331 . . . . . . . . 9 (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ↔ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
26 poimirlem25.5 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑁𝑇, 𝑈⟩ / 𝑠𝐶)
2726ralrimiva 2949 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑗 ∈ (0...𝑁)𝑁𝑇, 𝑈⟩ / 𝑠𝐶)
28 nfcv 2751 . . . . . . . . . . . . . . . . . 18 𝑗𝑁
29 nfcsb1v 3515 . . . . . . . . . . . . . . . . . 18 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
3028, 29nfne 2882 . . . . . . . . . . . . . . . . 17 𝑗 𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
31 csbeq1a 3508 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
3231neeq2d 2842 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑡 → (𝑁𝑇, 𝑈⟩ / 𝑠𝐶𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
3330, 32rspc 3276 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0...𝑁) → (∀𝑗 ∈ (0...𝑁)𝑁𝑇, 𝑈⟩ / 𝑠𝐶𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
3427, 33mpan9 485 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
35 nesym 2838 . . . . . . . . . . . . . . 15 (𝑁𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
3634, 35sylib 207 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
37 nfv 1830 . . . . . . . . . . . . . . . . . 18 𝑗(𝜑𝑡 ∈ (0...𝑁))
3829nfel1 2765 . . . . . . . . . . . . . . . . . 18 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)
3937, 38nfim 1813 . . . . . . . . . . . . . . . . 17 𝑗((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
40 eleq1 2676 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑡 → (𝑗 ∈ (0...𝑁) ↔ 𝑡 ∈ (0...𝑁)))
4140anbi2d 736 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡 → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡 ∈ (0...𝑁))))
4231eleq1d 2672 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑡 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
4341, 42imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑡 → (((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)) ↔ ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))))
44 poimirlem25.3 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
45 ovex 6577 . . . . . . . . . . . . . . . . . . . . . 22 (0..^𝐾) ∈ V
46 ovex 6577 . . . . . . . . . . . . . . . . . . . . . 22 (1...𝑁) ∈ V
4745, 46elmap 7772 . . . . . . . . . . . . . . . . . . . . 21 (𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) ↔ 𝑇:(1...𝑁)⟶(0..^𝐾))
4844, 47sylibr 223 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
49 poimirlem25.4 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
50 fzfi 12633 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑁) ∈ Fin
51 f1oexrnex 7008 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ Fin) → 𝑈 ∈ V)
5250, 51mpan2 703 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ V)
53 f1oeq1 6040 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑈 → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)))
5453elabg 3320 . . . . . . . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . . . . . . . 21 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
5749, 56syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
58 opelxpi 5072 . . . . . . . . . . . . . . . . . . . 20 ((𝑇 ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) ∧ 𝑈 ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
5948, 57, 58syl2anc 691 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
6059adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → ⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
61 nfcv 2751 . . . . . . . . . . . . . . . . . . 19 𝑠𝑇, 𝑈
62 nfv 1830 . . . . . . . . . . . . . . . . . . . 20 𝑠(𝜑𝑗 ∈ (0...𝑁))
63 nfcsb1v 3515 . . . . . . . . . . . . . . . . . . . . 21 𝑠𝑇, 𝑈⟩ / 𝑠𝐶
6463nfel1 2765 . . . . . . . . . . . . . . . . . . . 20 𝑠𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)
6562, 64nfim 1813 . . . . . . . . . . . . . . . . . . 19 𝑠((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
66 csbeq1a 3508 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = ⟨𝑇, 𝑈⟩ → 𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
6766eleq1d 2672 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = ⟨𝑇, 𝑈⟩ → (𝐶 ∈ (0...𝑁) ↔ 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
6867imbi2d 329 . . . . . . . . . . . . . . . . . . 19 (𝑠 = ⟨𝑇, 𝑈⟩ → (((𝜑𝑗 ∈ (0...𝑁)) → 𝐶 ∈ (0...𝑁)) ↔ ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))))
69 elun 3715 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 ∈ ({1} ∪ {0}) ↔ (𝑝 ∈ {1} ∨ 𝑝 ∈ {0}))
70 fzofzp1 12431 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝐾) → (𝑖 + 1) ∈ (0...𝐾))
71 elsni 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ {1} → 𝑝 = 1)
7271oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ {1} → (𝑖 + 𝑝) = (𝑖 + 1))
7372eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ {1} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 1) ∈ (0...𝐾)))
7470, 73syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {1} → (𝑖 + 𝑝) ∈ (0...𝐾)))
75 elfzonn0 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℕ0)
7675nn0cnd 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ ℂ)
7776addid1d 10115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) = 𝑖)
78 elfzofz 12354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝐾) → 𝑖 ∈ (0...𝐾))
7977, 78eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (0..^𝐾) → (𝑖 + 0) ∈ (0...𝐾))
80 elsni 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑝 ∈ {0} → 𝑝 = 0)
8180oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ {0} → (𝑖 + 𝑝) = (𝑖 + 0))
8281eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ {0} → ((𝑖 + 𝑝) ∈ (0...𝐾) ↔ (𝑖 + 0) ∈ (0...𝐾)))
8379, 82syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ {0} → (𝑖 + 𝑝) ∈ (0...𝐾)))
8474, 83jaod 394 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝐾) → ((𝑝 ∈ {1} ∨ 𝑝 ∈ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾)))
8569, 84syl5bi 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0..^𝐾) → (𝑝 ∈ ({1} ∪ {0}) → (𝑖 + 𝑝) ∈ (0...𝐾)))
8685imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0})) → (𝑖 + 𝑝) ∈ (0...𝐾))
8786adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑖 ∈ (0..^𝐾) ∧ 𝑝 ∈ ({1} ∪ {0}))) → (𝑖 + 𝑝) ∈ (0...𝐾))
88 xp1st 7089 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
89 elmapi 7765 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1st𝑠) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
9088, 89syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
9190adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝐾))
92 xp2nd 7090 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd𝑠) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
93 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (2nd𝑠) ∈ V
94 f1oeq1 6040 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = (2nd𝑠) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁)))
9593, 94elab 3319 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd𝑠) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁))
9692, 95sylib 207 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁))
97 1ex 9914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ V
9897fconst 6004 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((2nd𝑠) “ (1...𝑗)) × {1}):((2nd𝑠) “ (1...𝑗))⟶{1}
99 c0ex 9913 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 ∈ V
10099fconst 6004 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6056 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd𝑠):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd𝑠)))
103 imain 5888 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun (2nd𝑠) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))))
104102, 103simplbiim 657 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))))
105 elfznn0 12302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
106105nn0red 11229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
107106ltp1d 10833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
108 fzdisj 12239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
110109imaeq2d 5385 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd𝑠) “ ∅))
111 ima0 5400 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠) “ ∅) = ∅
112110, 111syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
113104, 112sylan9req 2665 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd𝑠) “ (1...𝑗)) ∩ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = ∅)
114 fun 5979 . . . . . . . . . . . . . . . . . . . . . . . . . 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 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
116 nn0p1nn 11209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
117105, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
118 nnuz 11599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℕ = (ℤ‘1)
119117, 118syl6eleq 2698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
120 elfzuz3 12210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
121 fzsplit2 12237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
122119, 120, 121syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
123122imaeq2d 5385 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → ((2nd𝑠) “ (1...𝑁)) = ((2nd𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
124 imaundi 5464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁)))
125123, 124syl6req 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = ((2nd𝑠) “ (1...𝑁)))
126 f1ofo 6057 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd𝑠):(1...𝑁)–onto→(1...𝑁))
127 foima 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2nd𝑠):(1...𝑁)–onto→(1...𝑁) → ((2nd𝑠) “ (1...𝑁)) = (1...𝑁))
128126, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd𝑠) “ (1...𝑁)) = (1...𝑁))
129125, 128sylan9eqr 2666 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd𝑠) “ (1...𝑗)) ∪ ((2nd𝑠) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
130129feq2d 5944 . . . . . . . . . . . . . . . . . . . . . . . . 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 221 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑠):(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
13296, 131sylan 487 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
133 fzfid 12634 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
134 inidm 3784 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
13587, 91, 132, 133, 133, 134off 6810 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁)) → ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
136 ovex 6577 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
137 feq1 5939 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝:(1...𝑁)⟶(0...𝐾) ↔ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
138137anbi2d 736 . . . . . . . . . . . . . . . . . . . . . . . 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 2672 . . . . . . . . . . . . . . . . . . . . . . . 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 3232 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → 𝐶 ∈ (0...𝑁))
144135, 143sylan2 490 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠 ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑗 ∈ (0...𝑁))) → 𝐶 ∈ (0...𝑁))
145144an12s 839 . . . . . . . . . . . . . . . . . . . 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 3244 . . . . . . . . . . . . . . . . . 18 (⟨𝑇, 𝑈⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁)))
14860, 147mpcom 37 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
14939, 43, 148chvar 2250 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁))
150 poimir.0 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℕ)
151150nnnn0d 11228 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
152 nn0uz 11598 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
153151, 152syl6eleq 2698 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘0))
154 fzm1 12289 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘0) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
155153, 154syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
156155adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
157149, 156mpbid 221 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
158157ord 391 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → (¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
15936, 158mt3d 139 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
160159adantrr 749 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
161 fzfi 12633 . . . . . . . . . . . . . . 15 (0...(𝑁 − 1)) ∈ Fin
162150nncnd 10913 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
163 1cnd 9935 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 1 ∈ ℂ)
164162, 163, 163addsubd 10292 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 + 1) − 1) = ((𝑁 − 1) + 1))
165 hashfz0 13079 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (#‘(0...𝑁)) = (𝑁 + 1))
166151, 165syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (#‘(0...𝑁)) = (𝑁 + 1))
167166oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((#‘(0...𝑁)) − 1) = ((𝑁 + 1) − 1))
168 nnm1nn0 11211 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
169 hashfz0 13079 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ ℕ0 → (#‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1))
170150, 168, 1693syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (#‘(0...(𝑁 − 1))) = ((𝑁 − 1) + 1))
171164, 167, 1703eqtr4rd 2655 . . . . . . . . . . . . . . . . 17 (𝜑 → (#‘(0...(𝑁 − 1))) = ((#‘(0...𝑁)) − 1))
172 hashdifsn 13063 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) ∈ Fin ∧ 𝑡 ∈ (0...𝑁)) → (#‘((0...𝑁) ∖ {𝑡})) = ((#‘(0...𝑁)) − 1))
1738, 172mpan 702 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0...𝑁) → (#‘((0...𝑁) ∖ {𝑡})) = ((#‘(0...𝑁)) − 1))
174173eqcomd 2616 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0...𝑁) → ((#‘(0...𝑁)) − 1) = (#‘((0...𝑁) ∖ {𝑡})))
175171, 174sylan9eq 2664 . . . . . . . . . . . . . . . 16 ((𝜑𝑡 ∈ (0...𝑁)) → (#‘(0...(𝑁 − 1))) = (#‘((0...𝑁) ∖ {𝑡})))
176 diffi 8077 . . . . . . . . . . . . . . . . . 18 ((0...𝑁) ∈ Fin → ((0...𝑁) ∖ {𝑡}) ∈ Fin)
1778, 176ax-mp 5 . . . . . . . . . . . . . . . . 17 ((0...𝑁) ∖ {𝑡}) ∈ Fin
178 hashen 12997 . . . . . . . . . . . . . . . . 17 (((0...(𝑁 − 1)) ∈ Fin ∧ ((0...𝑁) ∖ {𝑡}) ∈ Fin) → ((#‘(0...(𝑁 − 1))) = (#‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})))
179161, 177, 178mp2an 704 . . . . . . . . . . . . . . . 16 ((#‘(0...(𝑁 − 1))) = (#‘((0...𝑁) ∖ {𝑡})) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))
180175, 179sylib 207 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}))
181 phpreu 32563 . . . . . . . . . . . . . . 15 (((0...(𝑁 − 1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
182161, 180, 181sylancr 694 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
183182biimpd 218 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (0...𝑁)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
184183impr 647 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
185 nfv 1830 . . . . . . . . . . . . . . 15 𝑧 𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶
186 nfcsb1v 3515 . . . . . . . . . . . . . . . 16 𝑗𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
187186nfeq2 2766 . . . . . . . . . . . . . . 15 𝑗 𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
188 csbeq1a 3508 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑧𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
189188eqeq2d 2620 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
190185, 187, 189cbvreu 3145 . . . . . . . . . . . . . 14 (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
191 eqeq1 2614 . . . . . . . . . . . . . . 15 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
192191reubidv 3103 . . . . . . . . . . . . . 14 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
193190, 192syl5bb 271 . . . . . . . . . . . . 13 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
194193rspcv 3278 . . . . . . . . . . . 12 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
195160, 184, 194sylc 63 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
196 an32 835 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
197196biimpi 205 . . . . . . . . . . . . . . 15 (((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
198197adantll 746 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
199 eqeq2 2621 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
200 rexsns 4164 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
20129nfeq2 2766 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗 𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
20231eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑡 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
203201, 202sbciegf 3434 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ V → ([𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
2047, 203ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑡 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
205200, 204bitri 263 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
206 rexsns 4164 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
207 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧 ∈ V
208187, 189sbciegf 3434 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ V → ([𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
209207, 208ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑧 / 𝑗]𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
210206, 209bitri 263 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
211199, 205, 2103bitr4g 302 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
212211orbi1d 735 . . . . . . . . . . . . . . . . . . . 20 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ((∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
213 rexun 3755 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (∃𝑗 ∈ {𝑡}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
214 rexun 3755 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (∃𝑗 ∈ {𝑧}𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∨ ∃𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
215212, 213, 2143bitr4g 302 . . . . . . . . . . . . . . . . . . 19 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
216215adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
217 eldifsni 4261 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧𝑡)
218217necomd 2837 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑡𝑧)
219 dif32 3850 . . . . . . . . . . . . . . . . . . . . . . 23 (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) = (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})
220219uneq2i 3726 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}))
221 snssi 4280 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → {𝑡} ⊆ ((0...𝑁) ∖ {𝑧}))
222 eldifsn 4260 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) ↔ (𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧))
223 undif 4001 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑡} ⊆ ((0...𝑁) ∖ {𝑧}) ↔ ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧}))
224221, 222, 2233imtr3i 279 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡})) = ((0...𝑁) ∖ {𝑧}))
225220, 224syl5eq 2656 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧}))
226218, 225sylan2 490 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑧}))
227226rexeqdv 3122 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
228227adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑡} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
229 snssi 4280 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → {𝑧} ⊆ ((0...𝑁) ∖ {𝑡}))
230 undif 4001 . . . . . . . . . . . . . . . . . . . . 21 ({𝑧} ⊆ ((0...𝑁) ∖ {𝑡}) ↔ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡}))
231229, 230sylib 207 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})) = ((0...𝑁) ∖ {𝑡}))
232231rexeqdv 3122 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
233232ad2antlr 759 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ({𝑧} ∪ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
234216, 228, 2333bitr3d 297 . . . . . . . . . . . . . . . . 17 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
235234ralbidv 2969 . . . . . . . . . . . . . . . 16 (((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
236235biimpar 501 . . . . . . . . . . . . . . 15 ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
237236an32s 842 . . . . . . . . . . . . . 14 ((((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
238198, 237sylan 487 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
239 simpl 472 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 ∈ (0...𝑁))
240239anim2i 591 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (𝜑𝑡 ∈ (0...𝑁)))
241 necom 2835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑡𝑡𝑧)
242241biimpi 205 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝑡𝑡𝑧)
243242adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) → 𝑡𝑧)
244243anim2i 591 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡)) → (𝑡 ∈ (0...𝑁) ∧ 𝑡𝑧))
245 eldifsn 4260 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ↔ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡))
246245anbi2i 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ↔ (𝑡 ∈ (0...𝑁) ∧ (𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡)))
247244, 246, 2223imtr4i 280 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ (0...𝑁) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
248247adantll 746 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
249248adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 ∈ ((0...𝑁) ∖ {𝑧}))
25029nfel1 2765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))
25137, 250nfim 1813 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
25231eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑡 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))))
25341, 252imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑡 → (((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1))) ↔ ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))))
25426necomd 2837 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶𝑁)
255254neneqd 2787 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → ¬ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)
256 fzm1 12289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ (ℤ‘0) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
257153, 256syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
258257adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...𝑁) ↔ (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁)))
259148, 258mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∨ 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
260259ord 391 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (¬ 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑁))
261255, 260mt3d 139 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
262251, 253, 261chvar 2250 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 ∈ (0...𝑁)) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
263262ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)))
264 eldifi 3694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ((0...𝑁) ∖ {𝑡}) → 𝑧 ∈ (0...𝑁))
265 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑧 → (𝑡 ∈ (0...𝑁) ↔ 𝑧 ∈ (0...𝑁)))
266265anbi2d 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑧 → ((𝜑𝑡 ∈ (0...𝑁)) ↔ (𝜑𝑧 ∈ (0...𝑁))))
267 sneq 4135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 𝑧 → {𝑡} = {𝑧})
268267difeq2d 3690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑧 → ((0...𝑁) ∖ {𝑡}) = ((0...𝑁) ∖ {𝑧}))
269268breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = 𝑧 → ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡}) ↔ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})))
270266, 269imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = 𝑧 → (((𝜑𝑡 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑡})) ↔ ((𝜑𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))))
271270, 180chvarv 2251 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (0...𝑁)) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
272264, 271sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
273272adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}))
274 phpreu 32563 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0...(𝑁 − 1)) ∈ Fin ∧ (0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧})) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
275161, 274mpan 702 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
276275biimpa 500 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...(𝑁 − 1)) ≈ ((0...𝑁) ∖ {𝑧}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
277273, 276sylan 487 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
278 eqeq1 2614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
279278adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑗 ∈ ((0...𝑁) ∖ {𝑧})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
280201, 279reubida 3101 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
281280rspcv 3278 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) → (∀𝑖 ∈ (0...(𝑁 − 1))∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
282263, 277, 281sylc 63 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
283 reurmo 3138 . . . . . . . . . . . . . . . . . . . . . 22 (∃!𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
284282, 283syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
285 nfv 1830 . . . . . . . . . . . . . . . . . . . . . 22 𝑖𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶
286285rmo3 3494 . . . . . . . . . . . . . . . . . . . . 21 (∃*𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖))
287284, 286sylib 207 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖))
288 equcomi 1931 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑡𝑡 = 𝑖)
289288csbeq1d 3506 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑡𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
290 sbsbc 3406 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶[𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
291 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑖 ∈ V
292 sbceqg 3936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ V → ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
29329csbconstgf 3511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ V → 𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
294293eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ V → (𝑖 / 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
295292, 294bitrd 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ V → ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
296291, 295ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
297290, 296bitri 263 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑖 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
298289, 297sylibr 223 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑡 → [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
299298biantrud 527 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑡 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
300299bicomd 212 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑡 → ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
301 eqeq2 2621 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑡 → (𝑗 = 𝑖𝑗 = 𝑡))
302300, 301imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑡 → (((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
303302rspcv 3278 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
304303ralimdv 2946 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ((0...𝑁) ∖ {𝑧}) → (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})∀𝑖 ∈ ((0...𝑁) ∖ {𝑧})((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ [𝑖 / 𝑗]𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑗 = 𝑖) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡)))
305249, 287, 304sylc 63 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡))
306 dif32 3850 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) = (((0...𝑁) ∖ {𝑡}) ∖ {𝑧})
307306eleq2i 2680 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ 𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}))
308 eldifsn 4260 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑧}) ∖ {𝑡}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡))
309 eldifsn 4260 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (((0...𝑁) ∖ {𝑡}) ∖ {𝑧}) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧))
310307, 308, 3093bitr3ri 290 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡))
311310imbi1i 338 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
312 impexp 461 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑡}) ∧ 𝑗𝑧) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
313 impexp 461 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) ∧ 𝑗𝑡) → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
314311, 312, 3133bitr3ri 290 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ↔ (𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
315314albii 1737 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
316 con34b 305 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ (¬ 𝑗 = 𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
317 df-ne 2782 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑡 ↔ ¬ 𝑗 = 𝑡)
318317imbi1i 338 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (¬ 𝑗 = 𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
319316, 318bitr4i 266 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
320319ralbii 2963 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
321 df-ral 2901 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
322320, 321bitri 263 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑧}) → (𝑗𝑡 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
323 df-ral 2901 . . . . . . . . . . . . . . . . . . . 20 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∀𝑗(𝑗 ∈ ((0...𝑁) ∖ {𝑡}) → (𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
324315, 322, 3233bitr4i 291 . . . . . . . . . . . . . . . . . . 19 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑧})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑡) ↔ ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
325305, 324sylib 207 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
326 df-ne 2782 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗𝑧 ↔ ¬ 𝑗 = 𝑧)
327326imbi1i 338 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (¬ 𝑗 = 𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
328 con34b 305 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧) ↔ (¬ 𝑗 = 𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
329327, 328bitr4i 266 . . . . . . . . . . . . . . . . . . . 20 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧))
330 ancr 570 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑗 = 𝑧) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
331329, 330sylbi 206 . . . . . . . . . . . . . . . . . . 19 ((𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
332331ralimi 2936 . . . . . . . . . . . . . . . . . 18 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗𝑧 → ¬ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
333325, 332syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡 ∈ (0...𝑁)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
334240, 333sylanl1 680 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
335201, 278rexbid 3033 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
336335rspcva 3280 . . . . . . . . . . . . . . . . . . 19 ((𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ∈ (0...(𝑁 − 1)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
337262, 336sylan 487 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡 ∈ (0...𝑁)) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
338337anasss 677 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
339338ad2antrr 758 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)
340 rexim 2991 . . . . . . . . . . . . . . . 16 (∀𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → (𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶)))
341334, 339, 340sylc 63 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
342 rexex 2985 . . . . . . . . . . . . . . 15 (∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
343341, 342syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶))
34429, 186nfeq 2762 . . . . . . . . . . . . . . 15 𝑗𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
345188eqeq2d 2620 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
346344, 345equsexv 2095 . . . . . . . . . . . . . 14 (∃𝑗(𝑗 = 𝑧𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
347343, 346sylib 207 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) → 𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
348238, 347impbida 873 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) ∧ 𝑧 ∈ ((0...𝑁) ∖ {𝑡})) → (𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
349348reubidva 3102 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})𝑡 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = 𝑧 / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
350195, 349mpbid 221 . . . . . . . . . 10 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → ∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
351 an32 835 . . . . . . . . . . . . . 14 (((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧𝑡))
352245anbi1i 727 . . . . . . . . . . . . . 14 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ((𝑧 ∈ (0...𝑁) ∧ 𝑧𝑡) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
353 sneq 4135 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → {𝑦} = {𝑧})
354353difeq2d 3690 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((0...𝑁) ∖ {𝑦}) = ((0...𝑁) ∖ {𝑧}))
355354rexeqdv 3122 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
356355ralbidv 2969 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
357356elrab 3331 . . . . . . . . . . . . . . 15 (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ↔ (𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
358357anbi1i 727 . . . . . . . . . . . . . 14 ((𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡) ↔ ((𝑧 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ∧ 𝑧𝑡))
359351, 352, 3583bitr4i 291 . . . . . . . . . . . . 13 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡))
360 eldifsn 4260 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}) ↔ (𝑧 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∧ 𝑧𝑡))
361359, 360bitr4i 266 . . . . . . . . . . . 12 ((𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
362361eubii 2480 . . . . . . . . . . 11 (∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶) ↔ ∃!𝑧 𝑧 ∈ ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡}))
363 df-reu 2903 . . . . . . . . . . 11 (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃!𝑧(𝑧 ∈ ((0...𝑁) ∖ {𝑡}) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
364 euhash1 13069 . . . . . . . . . . . 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 291 . . . . . . . . . 10 (∃!𝑧 ∈ ((0...𝑁) ∖ {𝑡})∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑧})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ↔ (#‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
367350, 366sylib 207 . . . . . . . . 9 ((𝜑 ∧ (𝑡 ∈ (0...𝑁) ∧ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑡})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)) → (#‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
36825, 367sylan2b 491 . . . . . . . 8 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → (#‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) = 1)
369368oveq1d 6564 . . . . . . 7 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → ((#‘({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} ∖ {𝑡})) + 1) = (1 + 1))
37020, 369eqtr3d 2646 . . . . . 6 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) = (1 + 1))
3716, 370syl5breqr 4621 . . . . 5 ((𝜑𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) → 2 ∥ (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
372371ex 449 . . . 4 (𝜑 → (𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → 2 ∥ (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
373372exlimdv 1848 . . 3 (𝜑 → (∃𝑡 𝑡 ∈ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} → 2 ∥ (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
3741, 373syl5bi 231 . 2 (𝜑 → (¬ {𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → 2 ∥ (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶})))
375 dvds0 14835 . . . . 5 (2 ∈ ℤ → 2 ∥ 0)
3762, 375ax-mp 5 . . . 4 2 ∥ 0
377 hash0 13019 . . . 4 (#‘∅) = 0
378376, 377breqtrri 4610 . . 3 2 ∥ (#‘∅)
379 fveq2 6103 . . 3 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}) = (#‘∅))
380378, 379syl5breqr 4621 . 2 ({𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶} = ∅ → 2 ∥ (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
381374, 380pm2.61d2 171 1 (𝜑 → 2 ∥ (#‘{𝑦 ∈ (0...𝑁) ∣ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑦})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695  [wsb 1867   ∈ wcel 1977  ∃!weu 2458  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  ∃*wrmo 2899  {crab 2900  Vcvv 3173  [wsbc 3402  ⦋csb 3499   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125  ⟨cop 4131   class class class wbr 4583   × cxp 5036  ◡ccnv 5037   “ cima 5041  Fun wfun 5798  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ∘𝑓 cof 6793  1st c1st 7057  2nd c2nd 7058   ↑𝑚 cmap 7744   ≈ cen 7838  Fincfn 7841  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   − cmin 10145  ℕcn 10897  2c2 10947  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ...cfz 12197  ..^cfzo 12334  #chash 12979   ∥ cdvds 14821 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-hash 12980  df-dvds 14822 This theorem is referenced by:  poimirlem26  32605
 Copyright terms: Public domain W3C validator