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 42179
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 5151 . . . . . . . 8 (𝑑 = 𝑐 → (𝑑 ∥ (♯‘𝐵) ↔ 𝑐 ∥ (♯‘𝐵)))
2 eqeq2 2747 . . . . . . . . . 10 (𝑑 = 𝑐 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
32rabbidv 3441 . . . . . . . . 9 (𝑑 = 𝑐 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐})
43neeq1d 2998 . . . . . . . 8 (𝑑 = 𝑐 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅))
51, 4anbi12d 632 . . . . . . 7 (𝑑 = 𝑐 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅)))
63fveq2d 6911 . . . . . . . 8 (𝑑 = 𝑐 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}))
7 fveq2 6907 . . . . . . . 8 (𝑑 = 𝑐 → (ϕ‘𝑑) = (ϕ‘𝑐))
86, 7eqeq12d 2751 . . . . . . 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 5151 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → (𝑐 < 𝑑 ↔ 𝑒 < 𝑑))
15 breq1 5151 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (𝑐 ∥ (♯‘𝐵) ↔ 𝑒 ∥ (♯‘𝐵)))
16 eqeq2 2747 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑒 → (((od‘𝐺)‘𝑥) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑒))
1716rabbidv 3441 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑒 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒})
1817neeq1d 2998 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅))
1915, 18anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅)))
2017fveq2d 6911 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}))
21 fveq2 6907 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (ϕ‘𝑐) = (ϕ‘𝑒))
2220, 21eqeq12d 2751 . . . . . . . . . . . . . . . . . . 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 3144 . . . . . . . . . . . . 13 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ∀𝑒 ∈ ℕ (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
41 nfv 1912 . . . . . . . . . . . . . . 15 Ⅎ𝑐(𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))
42 nfv 1912 . . . . . . . . . . . . . . 15 Ⅎ𝑒(𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
43 breq1 5151 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑐 → (𝑒 < 𝑑 ↔ 𝑐 < 𝑑))
44 breq1 5151 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (𝑒 ∥ (♯‘𝐵) ↔ 𝑐 ∥ (♯‘𝐵)))
45 eqeq2 2747 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑐 → (((od‘𝐺)‘𝑥) = 𝑒 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
4645rabbidv 3441 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑐 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐})
4746neeq1d 2998 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅))
4844, 47anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑐 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅)))
4946fveq2d 6911 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}))
50 fveq2 6907 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (ϕ‘𝑒) = (ϕ‘𝑐))
5149, 50eqeq12d 2751 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑐 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
5248, 51imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑐 → (((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)) ↔ ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
5343, 52imbi12d 344 . . . . . . . . . . . . . . 15 (𝑒 = 𝑐 → ((𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))) ↔ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
5441, 42, 53cbvralw 3304 . . . . . . . . . . . . . 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 4395 . . . . . . . . . . . 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 2903 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑥𝐵
72 nfcv 2903 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑧𝐵
73 nfv 1912 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑧((od‘𝐺)‘𝑥) = 𝑑
74 nfv 1912 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑥((od‘𝐺)‘𝑧) = 𝑑
75 fveqeq2 6916 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑧) = 𝑑))
7671, 72, 73, 74, 75cbvrabw 3471 . . . . . . . . . . . . . . . . 17 {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑}
7776a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑})
7877fveq2d 6911 . . . . . . . . . . . . . . 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 1912 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑧(𝑛 ↑ 𝑥) = (0g‘𝐺)
87 nfv 1912 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑥(𝑛 ↑ 𝑧) = (0g‘𝐺)
88 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧 → (𝑛 ↑ 𝑥) = (𝑛 ↑ 𝑧))
8988eqeq1d 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → ((𝑛 ↑ 𝑥) = (0g‘𝐺) ↔ (𝑛 ↑ 𝑧) = (0g‘𝐺)))
9071, 72, 86, 87, 89cbvrabw 3471 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)} = {𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}
9190a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)} = {𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)})
9291fveq2d 6911 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) = (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}))
9392breq1d 5158 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 ↔ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛))
9493ralbidv 3176 . . . . . . . . . . . . . . . . . . 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 1912 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑥((od‘𝐺)‘𝑧) = 𝑐
103 nfv 1912 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑧((od‘𝐺)‘𝑥) = 𝑐
104 fveqeq2 6916 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑥 → (((od‘𝐺)‘𝑧) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
10572, 71, 102, 103, 104cbvrabw 3471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}
106 eqcom 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐})
107105, 106mpbi 230 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}
108107neeq1i 3003 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅)
109108anbi2i 623 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅))
110107fveq2i 6910 . . . . . . . . . . . . . . . . . . . . . . . . 25 (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐})
111110eqeq1i 2740 . . . . . . . . . . . . . . . . . . . . . . . 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 3081 . . . . . . . . . . . . . . . . . . . 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 42178 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑}) = (ϕ‘𝑑))
12178, 120eqtrd 2775 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
12270, 121syl 17 . . . . . . . . . . . . 13 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
123 nfv 1912 . . . . . . . . . . . . . . . 16 Ⅎ𝑎((od‘𝐺)‘𝑥) = 𝑑
124 nfv 1912 . . . . . . . . . . . . . . . 16 Ⅎ𝑥((od‘𝐺)‘𝑎) = 𝑑
125 fveqeq2 6916 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑎) = 𝑑))
126123, 124, 125cbvrexw 3305 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 ↔ ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
127126biimpi 216 . . . . . . . . . . . . . 14 (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 → ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
128127adantl 481 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) → ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
129122, 128r19.29a 3160 . . . . . . . . . . . 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 12956 . . . 4 (𝑑 ∈ ℕ → (𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))))
138137com12 32 . . 3 (𝜑 → (𝑑 ∈ ℕ → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))))
139138imp 406 . 2 ((𝜑 ∧ 𝑑 ∈ ℕ) → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
140139ralrimiva 3144 1 (𝜑 → ∀𝑑 ∈ ℕ ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  {crab 3433  ∅c0 4339   class class class wbr 5148  ‘cfv 6563  (class class class)co 7431  Fincfn 8984   < clt 11293   ≤ cle 11294  ℕcn 12264  ♯chash 14366   ∥ cdvds 16287  ϕcphi 16798  Basecbs 17245  0gc0g 17486  Grpcgrp 18964  .gcmg 19098  odcod 19557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-disj 5116  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-oadd 8509  df-omul 8510  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-sup 9480  df-inf 9481  df-oi 9548  df-card 9977  df-acn 9980  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-xnn0 12598  df-z 12612  df-uz 12877  df-rp 13033  df-fz 13545  df-fzo 13692  df-fl 13829  df-mod 13907  df-seq 14040  df-exp 14100  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-clim 15521  df-sum 15720  df-dvds 16288  df-gcd 16529  df-phi 16800  df-0g 17488  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-grp 18967  df-minusg 18968  df-sbg 18969  df-mulg 19099  df-od 19561
This theorem is referenced by:  unitscyglem4  42180
  Copyright terms: Public domain W3C validator