Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  unitscyglem3 Structured version   Visualization version   GIF version
Theorem unitscyglem3 42198
Description: Lemma for unitscyg. (Contributed by metakunt, 14-Jul-2025.)
Hypotheses
Ref Expression
unitscyglem1.1 𝐵 = (Base‘𝐺)
unitscyglem1.2 ↑ = (.g‘𝐺)
unitscyglem1.3 (𝜑 → 𝐺 ∈ Grp)
unitscyglem1.4 (𝜑 → 𝐵 ∈ Fin)
unitscyglem1.5 (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)
Assertion
Ref Expression
unitscyglem3 (𝜑 → ∀𝑑 ∈ ℕ ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
Distinct variable groups:   𝐵,𝑑,𝑥   𝐺,𝑑,𝑥   𝜑,𝑑   ↑ ,𝑛,𝑥   𝐵,𝑛   𝑛,𝐺   𝜑,𝑛
Allowed substitution hints:   𝜑(𝑥)   ↑ (𝑑)
Proof of Theorem unitscyglem3
Dummy variables 𝑎 𝑐 𝑒 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 5146 . . . . . . . 8 (𝑑 = 𝑐 → (𝑑 ∥ (♯‘𝐵) ↔ 𝑐 ∥ (♯‘𝐵)))
2 eqeq2 2749 . . . . . . . . . 10 (𝑑 = 𝑐 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
32rabbidv 3444 . . . . . . . . 9 (𝑑 = 𝑐 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐})
43neeq1d 3000 . . . . . . . 8 (𝑑 = 𝑐 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅))
51, 4anbi12d 632 . . . . . . 7 (𝑑 = 𝑐 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅)))
63fveq2d 6910 . . . . . . . 8 (𝑑 = 𝑐 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}))
7 fveq2 6906 . . . . . . . 8 (𝑑 = 𝑐 → (ϕ‘𝑑) = (ϕ‘𝑐))
86, 7eqeq12d 2753 . . . . . . 7 (𝑑 = 𝑐 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
95, 8imbi12d 344 . . . . . 6 (𝑑 = 𝑐 → (((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)) ↔ ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
109imbi2d 340 . . . . 5 (𝑑 = 𝑐 → ((𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))) ↔ (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
11 simplr 769 . . . . . . . . . . . . 13 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → 𝜑)
12 simplll 775 . . . . . . . . . . . . 13 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → 𝑑 ∈ ℕ)
1311, 12jca 511 . . . . . . . . . . . 12 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → (𝜑 ∧ 𝑑 ∈ ℕ))
14 breq1 5146 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → (𝑐 < 𝑑 ↔ 𝑒 < 𝑑))
15 breq1 5146 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (𝑐 ∥ (♯‘𝐵) ↔ 𝑒 ∥ (♯‘𝐵)))
16 eqeq2 2749 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑒 → (((od‘𝐺)‘𝑥) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑒))
1716rabbidv 3444 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑒 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒})
1817neeq1d 3000 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅))
1915, 18anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅)))
2017fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}))
21 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (ϕ‘𝑐) = (ϕ‘𝑒))
2220, 21eqeq12d 2753 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))
2319, 22imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑒 → (((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)) ↔ ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
2423imbi2d 340 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → ((𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) ↔ (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))))
2514, 24imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑒 → ((𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ↔ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))))
26 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
2726adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
2827adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
2928adantr 480 . . . . . . . . . . . . . . . 16 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
30 simpr 484 . . . . . . . . . . . . . . . 16 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → 𝑒 ∈ ℕ)
3125, 29, 30rspcdva 3623 . . . . . . . . . . . . . . 15 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))))
32 simp-5r 786 . . . . . . . . . . . . . . . . . 18 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → 𝜑)
33 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → 𝑒 < 𝑑)
34 simplr 769 . . . . . . . . . . . . . . . . . . 19 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))))
3533, 34mpd 15 . . . . . . . . . . . . . . . . . 18 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
3632, 35mpd 15 . . . . . . . . . . . . . . . . 17 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))
3736ex 412 . . . . . . . . . . . . . . . 16 ((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) → (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
3837ex 412 . . . . . . . . . . . . . . 15 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → ((𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))) → (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))))
3931, 38mpd 15 . . . . . . . . . . . . . 14 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
4039ralrimiva 3146 . . . . . . . . . . . . 13 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ∀𝑒 ∈ ℕ (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
41 nfv 1914 . . . . . . . . . . . . . . 15 Ⅎ𝑐(𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))
42 nfv 1914 . . . . . . . . . . . . . . 15 Ⅎ𝑒(𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
43 breq1 5146 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑐 → (𝑒 < 𝑑 ↔ 𝑐 < 𝑑))
44 breq1 5146 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (𝑒 ∥ (♯‘𝐵) ↔ 𝑐 ∥ (♯‘𝐵)))
45 eqeq2 2749 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑐 → (((od‘𝐺)‘𝑥) = 𝑒 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
4645rabbidv 3444 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑐 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐})
4746neeq1d 3000 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅))
4844, 47anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑐 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅)))
4946fveq2d 6910 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}))
50 fveq2 6906 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (ϕ‘𝑒) = (ϕ‘𝑐))
5149, 50eqeq12d 2753 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑐 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
5248, 51imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑐 → (((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)) ↔ ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
5343, 52imbi12d 344 . . . . . . . . . . . . . . 15 (𝑒 = 𝑐 → ((𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))) ↔ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
5441, 42, 53cbvralw 3306 . . . . . . . . . . . . . 14 (∀𝑒 ∈ ℕ (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))) ↔ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
5554biimpi 216 . . . . . . . . . . . . 13 (∀𝑒 ∈ ℕ (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
5640, 55syl 17 . . . . . . . . . . . 12 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
5713, 56jca 511 . . . . . . . . . . 11 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
58 simprl 771 . . . . . . . . . . 11 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → 𝑑 ∥ (♯‘𝐵))
5957, 58jca 511 . . . . . . . . . 10 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → (((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)))
60 simprr 773 . . . . . . . . . 10 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)
6159, 60jca 511 . . . . . . . . 9 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅))
62 rabn0 4389 . . . . . . . . . . . 12 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑)
6362biimpi 216 . . . . . . . . . . 11 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅ → ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑)
6463adantl 481 . . . . . . . . . 10 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑)
65 simp-4l 783 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
66 simp-4r 784 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑑 ∥ (♯‘𝐵))
67 simplr 769 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑎 ∈ 𝐵)
6865, 66, 67jca31 514 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵))
69 simpr 484 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ((od‘𝐺)‘𝑎) = 𝑑)
7068, 69jca 511 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑))
71 nfcv 2905 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑥𝐵
72 nfcv 2905 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑧𝐵
73 nfv 1914 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑧((od‘𝐺)‘𝑥) = 𝑑
74 nfv 1914 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑥((od‘𝐺)‘𝑧) = 𝑑
75 fveqeq2 6915 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑧) = 𝑑))
7671, 72, 73, 74, 75cbvrabw 3473 . . . . . . . . . . . . . . . . 17 {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑}
7776a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑})
7877fveq2d 6910 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑}))
79 unitscyglem1.1 . . . . . . . . . . . . . . . 16 𝐵 = (Base‘𝐺)
80 unitscyglem1.2 . . . . . . . . . . . . . . . 16 ↑ = (.g‘𝐺)
81 unitscyglem1.3 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝐺 ∈ Grp)
8281ad5antr 734 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝐺 ∈ Grp)
83 unitscyglem1.4 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝐵 ∈ Fin)
8483ad5antr 734 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝐵 ∈ Fin)
85 unitscyglem1.5 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)
86 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑧(𝑛 ↑ 𝑥) = (0g‘𝐺)
87 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑥(𝑛 ↑ 𝑧) = (0g‘𝐺)
88 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧 → (𝑛 ↑ 𝑥) = (𝑛 ↑ 𝑧))
8988eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → ((𝑛 ↑ 𝑥) = (0g‘𝐺) ↔ (𝑛 ↑ 𝑧) = (0g‘𝐺)))
9071, 72, 86, 87, 89cbvrabw 3473 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)} = {𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}
9190a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)} = {𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)})
9291fveq2d 6910 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) = (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}))
9392breq1d 5153 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 ↔ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛))
9493ralbidv 3178 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 ↔ ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛))
9594biimpd 229 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 → ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛))
9685, 95mpd 15 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛)
9796ad5antr 734 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛)
98 simp-5r 786 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑑 ∈ ℕ)
99 simpllr 776 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑑 ∥ (♯‘𝐵))
100 simplr 769 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑎 ∈ 𝐵)
101 simpr 484 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ((od‘𝐺)‘𝑎) = 𝑑)
102 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑥((od‘𝐺)‘𝑧) = 𝑐
103 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑧((od‘𝐺)‘𝑥) = 𝑐
104 fveqeq2 6915 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑥 → (((od‘𝐺)‘𝑧) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
10572, 71, 102, 103, 104cbvrabw 3473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}
106 eqcom 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐})
107105, 106mpbi 230 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}
108107neeq1i 3005 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅)
109108anbi2i 623 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅))
110107fveq2i 6909 . . . . . . . . . . . . . . . . . . . . . . . . 25 (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐})
111110eqeq1i 2742 . . . . . . . . . . . . . . . . . . . . . . . 24 ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐) ↔ (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))
112109, 111imbi12i 350 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)) ↔ ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐)))
113112imbi2i 336 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) ↔ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
114113biimpi 216 . . . . . . . . . . . . . . . . . . . . 21 ((𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) → (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
115114ralimi 3083 . . . . . . . . . . . . . . . . . . . 20 (∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
116115adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
117116adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
118117adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
119118adantr 480 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
12079, 80, 82, 84, 97, 98, 99, 100, 101, 119unitscyglem2 42197 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑}) = (ϕ‘𝑑))
12178, 120eqtrd 2777 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
12270, 121syl 17 . . . . . . . . . . . . 13 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
123 nfv 1914 . . . . . . . . . . . . . . . 16 Ⅎ𝑎((od‘𝐺)‘𝑥) = 𝑑
124 nfv 1914 . . . . . . . . . . . . . . . 16 Ⅎ𝑥((od‘𝐺)‘𝑎) = 𝑑
125 fveqeq2 6915 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑎) = 𝑑))
126123, 124, 125cbvrexw 3307 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 ↔ ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
127126biimpi 216 . . . . . . . . . . . . . 14 (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 → ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
128127adantl 481 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) → ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
129122, 128r19.29a 3162 . . . . . . . . . . . 12 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
130129ex 412 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) → (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
131130adantr 480 . . . . . . . . . 10 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
13264, 131mpd 15 . . . . . . . . 9 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
13361, 132syl 17 . . . . . . . 8 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
134133ex 412 . . . . . . 7 (((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
135134ex 412 . . . . . 6 ((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) → (𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))))
136135ex 412 . . . . 5 (𝑑 ∈ ℕ → (∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) → (𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))))
13710, 136indstr 12958 . . . 4 (𝑑 ∈ ℕ → (𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))))
138137com12 32 . . 3 (𝜑 → (𝑑 ∈ ℕ → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))))
139138imp 406 . 2 ((𝜑 ∧ 𝑑 ∈ ℕ) → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
140139ralrimiva 3146 1 (𝜑 → ∀𝑑 ∈ ℕ ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  {crab 3436  ∅c0 4333   class class class wbr 5143  ‘cfv 6561  (class class class)co 7431  Fincfn 8985   < clt 11295   ≤ cle 11296  ℕcn 12266  ♯chash 14369   ∥ cdvds 16290  ϕcphi 16801  Basecbs 17247  0gc0g 17484  Grpcgrp 18951  .gcmg 19085  odcod 19542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-omul 8511  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-acn 9982  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-dvds 16291  df-gcd 16532  df-phi 16803  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-grp 18954  df-minusg 18955  df-sbg 18956  df-mulg 19086  df-od 19546
This theorem is referenced by:  unitscyglem4  42199
  Copyright terms: Public domain W3C validator