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 42185
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 5110 . . . . . . . 8 (𝑑 = 𝑐 → (𝑑 ∥ (♯‘𝐵) ↔ 𝑐 ∥ (♯‘𝐵)))
2 eqeq2 2741 . . . . . . . . . 10 (𝑑 = 𝑐 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
32rabbidv 3413 . . . . . . . . 9 (𝑑 = 𝑐 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐})
43neeq1d 2984 . . . . . . . 8 (𝑑 = 𝑐 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅))
51, 4anbi12d 632 . . . . . . 7 (𝑑 = 𝑐 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅)))
63fveq2d 6862 . . . . . . . 8 (𝑑 = 𝑐 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}))
7 fveq2 6858 . . . . . . . 8 (𝑑 = 𝑐 → (ϕ‘𝑑) = (ϕ‘𝑐))
86, 7eqeq12d 2745 . . . . . . 7 (𝑑 = 𝑐 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
95, 8imbi12d 344 . . . . . 6 (𝑑 = 𝑐 → (((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)) ↔ ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
109imbi2d 340 . . . . 5 (𝑑 = 𝑐 → ((𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))) ↔ (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
11 simplr 768 . . . . . . . . . . . . 13 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → 𝜑)
12 simplll 774 . . . . . . . . . . . . 13 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → 𝑑 ∈ ℕ)
1311, 12jca 511 . . . . . . . . . . . 12 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → (𝜑 ∧ 𝑑 ∈ ℕ))
14 breq1 5110 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → (𝑐 < 𝑑 ↔ 𝑒 < 𝑑))
15 breq1 5110 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (𝑐 ∥ (♯‘𝐵) ↔ 𝑒 ∥ (♯‘𝐵)))
16 eqeq2 2741 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑒 → (((od‘𝐺)‘𝑥) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑒))
1716rabbidv 3413 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑒 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒})
1817neeq1d 2984 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅))
1915, 18anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅)))
2017fveq2d 6862 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}))
21 fveq2 6858 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (ϕ‘𝑐) = (ϕ‘𝑒))
2220, 21eqeq12d 2745 . . . . . . . . . . . . . . . . . . 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 3589 . . . . . . . . . . . . . . 15 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))))
32 simp-5r 785 . . . . . . . . . . . . . . . . . 18 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → 𝜑)
33 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → 𝑒 < 𝑑)
34 simplr 768 . . . . . . . . . . . . . . . . . . 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 3125 . . . . . . . . . . . . 13 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ∀𝑒 ∈ ℕ (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
41 nfv 1914 . . . . . . . . . . . . . . 15 Ⅎ𝑐(𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))
42 nfv 1914 . . . . . . . . . . . . . . 15 Ⅎ𝑒(𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
43 breq1 5110 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑐 → (𝑒 < 𝑑 ↔ 𝑐 < 𝑑))
44 breq1 5110 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (𝑒 ∥ (♯‘𝐵) ↔ 𝑐 ∥ (♯‘𝐵)))
45 eqeq2 2741 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑐 → (((od‘𝐺)‘𝑥) = 𝑒 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
4645rabbidv 3413 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑐 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐})
4746neeq1d 2984 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅))
4844, 47anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑐 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅)))
4946fveq2d 6862 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}))
50 fveq2 6858 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (ϕ‘𝑒) = (ϕ‘𝑐))
5149, 50eqeq12d 2745 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑐 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
5248, 51imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑐 → (((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)) ↔ ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
5343, 52imbi12d 344 . . . . . . . . . . . . . . 15 (𝑒 = 𝑐 → ((𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))) ↔ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
5441, 42, 53cbvralw 3280 . . . . . . . . . . . . . 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 770 . . . . . . . . . . 11 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → 𝑑 ∥ (♯‘𝐵))
5957, 58jca 511 . . . . . . . . . 10 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → (((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)))
60 simprr 772 . . . . . . . . . 10 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)
6159, 60jca 511 . . . . . . . . 9 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅))
62 rabn0 4352 . . . . . . . . . . . 12 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑)
6362biimpi 216 . . . . . . . . . . 11 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅ → ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑)
6463adantl 481 . . . . . . . . . 10 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑)
65 simp-4l 782 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
66 simp-4r 783 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑑 ∥ (♯‘𝐵))
67 simplr 768 . . . . . . . . . . . . . . . 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 2891 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑥𝐵
72 nfcv 2891 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑧𝐵
73 nfv 1914 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑧((od‘𝐺)‘𝑥) = 𝑑
74 nfv 1914 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑥((od‘𝐺)‘𝑧) = 𝑑
75 fveqeq2 6867 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑧) = 𝑑))
7671, 72, 73, 74, 75cbvrabw 3441 . . . . . . . . . . . . . . . . 17 {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑}
7776a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑})
7877fveq2d 6862 . . . . . . . . . . . . . . 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 7395 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧 → (𝑛 ↑ 𝑥) = (𝑛 ↑ 𝑧))
8988eqeq1d 2731 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → ((𝑛 ↑ 𝑥) = (0g‘𝐺) ↔ (𝑛 ↑ 𝑧) = (0g‘𝐺)))
9071, 72, 86, 87, 89cbvrabw 3441 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)} = {𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}
9190a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)} = {𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)})
9291fveq2d 6862 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) = (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}))
9392breq1d 5117 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 ↔ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛))
9493ralbidv 3156 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 ↔ ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛))
9594biimpd 229 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 → ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛))
9685, 95mpd 15 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛)
9796ad5antr 734 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛)
98 simp-5r 785 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑑 ∈ ℕ)
99 simpllr 775 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑑 ∥ (♯‘𝐵))
100 simplr 768 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑎 ∈ 𝐵)
101 simpr 484 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ((od‘𝐺)‘𝑎) = 𝑑)
102 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑥((od‘𝐺)‘𝑧) = 𝑐
103 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑧((od‘𝐺)‘𝑥) = 𝑐
104 fveqeq2 6867 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑥 → (((od‘𝐺)‘𝑧) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
10572, 71, 102, 103, 104cbvrabw 3441 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}
106 eqcom 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐})
107105, 106mpbi 230 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}
108107neeq1i 2989 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅)
109108anbi2i 623 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅))
110107fveq2i 6861 . . . . . . . . . . . . . . . . . . . . . . . . 25 (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐})
111110eqeq1i 2734 . . . . . . . . . . . . . . . . . . . . . . . 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 3066 . . . . . . . . . . . . . . . . . . . 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 42184 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑}) = (ϕ‘𝑑))
12178, 120eqtrd 2764 . . . . . . . . . . . . . 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 6867 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑎) = 𝑑))
126123, 124, 125cbvrexw 3281 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 ↔ ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
127126biimpi 216 . . . . . . . . . . . . . 14 (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 → ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
128127adantl 481 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) → ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
129122, 128r19.29a 3141 . . . . . . . . . . . 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 12875 . . . 4 (𝑑 ∈ ℕ → (𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))))
138137com12 32 . . 3 (𝜑 → (𝑑 ∈ ℕ → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))))
139138imp 406 . 2 ((𝜑 ∧ 𝑑 ∈ ℕ) → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
140139ralrimiva 3125 1 (𝜑 → ∀𝑑 ∈ ℕ ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3405  ∅c0 4296   class class class wbr 5107  ‘cfv 6511  (class class class)co 7387  Fincfn 8918   < clt 11208   ≤ cle 11209  ℕcn 12186  ♯chash 14295   ∥ cdvds 16222  ϕcphi 16734  Basecbs 17179  0gc0g 17402  Grpcgrp 18865  .gcmg 18999  odcod 19454
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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-inf2 9594  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145  ax-pre-sup 11146
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-disj 5075  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-oadd 8438  df-omul 8439  df-er 8671  df-map 8801  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-sup 9393  df-inf 9394  df-oi 9463  df-card 9892  df-acn 9895  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-div 11836  df-nn 12187  df-2 12249  df-3 12250  df-n0 12443  df-xnn0 12516  df-z 12530  df-uz 12794  df-rp 12952  df-fz 13469  df-fzo 13616  df-fl 13754  df-mod 13832  df-seq 13967  df-exp 14027  df-hash 14296  df-cj 15065  df-re 15066  df-im 15067  df-sqrt 15201  df-abs 15202  df-clim 15454  df-sum 15653  df-dvds 16223  df-gcd 16465  df-phi 16736  df-0g 17404  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-grp 18868  df-minusg 18869  df-sbg 18870  df-mulg 19000  df-od 19458
This theorem is referenced by:  unitscyglem4  42186
  Copyright terms: Public domain W3C validator