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 42997
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 5114 . . . . . . . 8 (𝑑 = 𝑐 → (𝑑 ∥ (♯‘𝐵) ↔ 𝑐 ∥ (♯‘𝐵)))
2 eqeq2 2777 . . . . . . . . . 10 (𝑑 = 𝑐 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
32rabbidv 3425 . . . . . . . . 9 (𝑑 = 𝑐 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐})
43neeq1d 3019 . . . . . . . 8 (𝑑 = 𝑐 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅))
51, 4anbi12d 644 . . . . . . 7 (𝑑 = 𝑐 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅)))
63fveq2d 6889 . . . . . . . 8 (𝑑 = 𝑐 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}))
7 fveq2 6885 . . . . . . . 8 (𝑑 = 𝑐 → (ϕ‘𝑑) = (ϕ‘𝑐))
86, 7eqeq12d 2781 . . . . . . 7 (𝑑 = 𝑐 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
95, 8imbi12d 347 . . . . . 6 (𝑑 = 𝑐 → (((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)) ↔ ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
109imbi2d 343 . . . . 5 (𝑑 = 𝑐 → ((𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))) ↔ (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
11 simplr 781 . . . . . . . . . . . . 13 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → 𝜑)
12 simplll 787 . . . . . . . . . . . . 13 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → 𝑑 ∈ ℕ)
1311, 12jca 521 . . . . . . . . . . . 12 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → (𝜑 ∧ 𝑑 ∈ ℕ))
14 breq1 5114 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → (𝑐 < 𝑑 ↔ 𝑒 < 𝑑))
15 breq1 5114 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (𝑐 ∥ (♯‘𝐵) ↔ 𝑒 ∥ (♯‘𝐵)))
16 eqeq2 2777 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑒 → (((od‘𝐺)‘𝑥) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑒))
1716rabbidv 3425 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑒 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒})
1817neeq1d 3019 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅))
1915, 18anbi12d 644 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅)))
2017fveq2d 6889 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}))
21 fveq2 6885 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (ϕ‘𝑐) = (ϕ‘𝑒))
2220, 21eqeq12d 2781 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))
2319, 22imbi12d 347 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑒 → (((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)) ↔ ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
2423imbi2d 343 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → ((𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) ↔ (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))))
2514, 24imbi12d 347 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑒 → ((𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ↔ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))))
26 simpr 490 . . . . . . . . . . . . . . . . . . 19 ((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
2726adantr 486 . . . . . . . . . . . . . . . . . 18 (((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
2827adantr 486 . . . . . . . . . . . . . . . . 17 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
2928adantr 486 . . . . . . . . . . . . . . . 16 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
30 simpr 490 . . . . . . . . . . . . . . . 16 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → 𝑒 ∈ ℕ)
3125, 29, 30rspcdva 3584 . . . . . . . . . . . . . . 15 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))))
32 simp-5r 798 . . . . . . . . . . . . . . . . . 18 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → 𝜑)
33 simpr 490 . . . . . . . . . . . . . . . . . . 19 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → 𝑒 < 𝑑)
34 simplr 781 . . . . . . . . . . . . . . . . . . 19 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))))
3533, 34mpd 16 . . . . . . . . . . . . . . . . . 18 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
3632, 35mpd 16 . . . . . . . . . . . . . . . . 17 (((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) ∧ 𝑒 < 𝑑) → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))
3736ex 418 . . . . . . . . . . . . . . . 16 ((((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) ∧ (𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))) → (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
3837ex 418 . . . . . . . . . . . . . . 15 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → ((𝑒 < 𝑑 → (𝜑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))) → (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))))
3931, 38mpd 16 . . . . . . . . . . . . . 14 (((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) ∧ 𝑒 ∈ ℕ) → (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
4039ralrimiva 3159 . . . . . . . . . . . . 13 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ∀𝑒 ∈ ℕ (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))))
41 nfv 1947 . . . . . . . . . . . . . . 15 Ⅎ𝑐(𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)))
42 nfv 1947 . . . . . . . . . . . . . . 15 Ⅎ𝑒(𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
43 breq1 5114 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑐 → (𝑒 < 𝑑 ↔ 𝑐 < 𝑑))
44 breq1 5114 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (𝑒 ∥ (♯‘𝐵) ↔ 𝑐 ∥ (♯‘𝐵)))
45 eqeq2 2777 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑐 → (((od‘𝐺)‘𝑥) = 𝑒 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
4645rabbidv 3425 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑐 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐})
4746neeq1d 3019 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅))
4844, 47anbi12d 644 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑐 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅)))
4946fveq2d 6889 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}))
50 fveq2 6885 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑐 → (ϕ‘𝑒) = (ϕ‘𝑐))
5149, 50eqeq12d 2781 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑐 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))
5248, 51imbi12d 347 . . . . . . . . . . . . . . . 16 (𝑒 = 𝑐 → (((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒)) ↔ ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
5343, 52imbi12d 347 . . . . . . . . . . . . . . 15 (𝑒 = 𝑐 → ((𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))) ↔ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
5441, 42, 53cbvralw 3309 . . . . . . . . . . . . . 14 (∀𝑒 ∈ ℕ (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))) ↔ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
5554biimpi 219 . . . . . . . . . . . . 13 (∀𝑒 ∈ ℕ (𝑒 < 𝑑 → ((𝑒 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑒}) = (ϕ‘𝑒))) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
5640, 55syl 18 . . . . . . . . . . . 12 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
5713, 56jca 521 . . . . . . . . . . 11 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
58 simprl 783 . . . . . . . . . . 11 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → 𝑑 ∥ (♯‘𝐵))
5957, 58jca 521 . . . . . . . . . 10 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → (((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)))
60 simprr 785 . . . . . . . . . 10 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)
6159, 60jca 521 . . . . . . . . 9 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → ((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅))
62 rabn0 4346 . . . . . . . . . . 11 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑)
6362bilani 510 . . . . . . . . . 10 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑)
64 simp-4l 795 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))))
65 simp-4r 796 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑑 ∥ (♯‘𝐵))
66 simplr 781 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑎 ∈ 𝐵)
6764, 65, 66jca31 524 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵))
68 simpr 490 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ((od‘𝐺)‘𝑎) = 𝑑)
6967, 68jca 521 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑))
70 nfcv 2927 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑥𝐵
71 nfcv 2927 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑧𝐵
72 nfv 1947 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑧((od‘𝐺)‘𝑥) = 𝑑
73 nfv 1947 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑥((od‘𝐺)‘𝑧) = 𝑑
74 fveqeq2 6894 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑧) = 𝑑))
7570, 71, 72, 73, 74cbvrabw 3453 . . . . . . . . . . . . . . . . 17 {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑}
7675a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑})
7776fveq2d 6889 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑}))
78 unitscyglem1.1 . . . . . . . . . . . . . . . 16 𝐵 = (Base‘𝐺)
79 unitscyglem1.2 . . . . . . . . . . . . . . . 16 ↑ = (.g‘𝐺)
80 unitscyglem1.3 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝐺 ∈ Grp)
8180ad5antr 747 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝐺 ∈ Grp)
82 unitscyglem1.4 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝐵 ∈ Fin)
8382ad5antr 747 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝐵 ∈ Fin)
84 unitscyglem1.5 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)
85 nfv 1947 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑧(𝑛 ↑ 𝑥) = (0g‘𝐺)
86 nfv 1947 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑥(𝑛 ↑ 𝑧) = (0g‘𝐺)
87 oveq2 7424 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑧 → (𝑛 ↑ 𝑥) = (𝑛 ↑ 𝑧))
8887eqeq1d 2767 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑧 → ((𝑛 ↑ 𝑥) = (0g‘𝐺) ↔ (𝑛 ↑ 𝑧) = (0g‘𝐺)))
8970, 71, 85, 86, 88cbvrabw 3453 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)} = {𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}
9089a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)} = {𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)})
9190fveq2d 6889 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) = (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}))
9291breq1d 5121 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 ↔ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛))
9392ralbidv 3190 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 ↔ ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛))
9493biimpd 232 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛 → ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛))
9584, 94mpd 16 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛)
9695ad5antr 747 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ∀𝑛 ∈ ℕ (♯‘{𝑧 ∈ 𝐵 ∣ (𝑛 ↑ 𝑧) = (0g‘𝐺)}) ≤ 𝑛)
97 simp-5r 798 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑑 ∈ ℕ)
98 simpllr 788 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑑 ∥ (♯‘𝐵))
99 simplr 781 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → 𝑎 ∈ 𝐵)
100 simpr 490 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ((od‘𝐺)‘𝑎) = 𝑑)
101 nfv 1947 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑥((od‘𝐺)‘𝑧) = 𝑐
102 nfv 1947 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑧((od‘𝐺)‘𝑥) = 𝑐
103 fveqeq2 6894 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑥 → (((od‘𝐺)‘𝑧) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑐))
10471, 70, 101, 102, 103cbvrabw 3453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}
105 eqcom 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐})
106104, 105mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}
107106neeq1i 3024 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅)
108107anbi2i 635 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅))
109106fveq2i 6888 . . . . . . . . . . . . . . . . . . . . . . . . 25 (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐})
110109eqeq1i 2770 . . . . . . . . . . . . . . . . . . . . . . . 24 ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐) ↔ (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))
111108, 110imbi12i 353 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)) ↔ ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐)))
112111imbi2i 339 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) ↔ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
113112biimpi 219 . . . . . . . . . . . . . . . . . . . . 21 ((𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) → (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
114113ralimi 3104 . . . . . . . . . . . . . . . . . . . 20 (∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
115114adantl 487 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
116115adantr 486 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
117116adantr 486 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
118117adantr 486 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐} ≠ ∅) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑐}) = (ϕ‘𝑐))))
11978, 79, 81, 83, 96, 97, 98, 99, 100, 118unitscyglem2 42996 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑧 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑧) = 𝑑}) = (ϕ‘𝑑))
12077, 119eqtrd 2800 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
12169, 120syl 18 . . . . . . . . . . . . 13 (((((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) ∧ 𝑎 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑎) = 𝑑) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
122 nfv 1947 . . . . . . . . . . . . . . 15 Ⅎ𝑎((od‘𝐺)‘𝑥) = 𝑑
123 nfv 1947 . . . . . . . . . . . . . . 15 Ⅎ𝑥((od‘𝐺)‘𝑎) = 𝑑
124 fveqeq2 6894 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (((od‘𝐺)‘𝑥) = 𝑑 ↔ ((od‘𝐺)‘𝑎) = 𝑑))
125122, 123, 124cbvrexw 3310 . . . . . . . . . . . . . 14 (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 ↔ ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
126125bilani 510 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) → ∃𝑎 ∈ 𝐵 ((od‘𝐺)‘𝑎) = 𝑑)
127121, 126r19.29a 3175 . . . . . . . . . . . 12 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
128127ex 418 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) → (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
129128adantr 486 . . . . . . . . . 10 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = 𝑑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
13063, 129mpd 16 . . . . . . . . 9 (((((𝜑 ∧ 𝑑 ∈ ℕ) ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) ∧ 𝑑 ∥ (♯‘𝐵)) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
13161, 130syl 18 . . . . . . . 8 ((((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) ∧ (𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))
132131ex 418 . . . . . . 7 (((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) ∧ 𝜑) → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
133132ex 418 . . . . . 6 ((𝑑 ∈ ℕ ∧ ∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))) → (𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))))
134133ex 418 . . . . 5 (𝑑 ∈ ℕ → (∀𝑐 ∈ ℕ (𝑐 < 𝑑 → (𝜑 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) → (𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))))
13510, 134indstr 12951 . . . 4 (𝑑 ∈ ℕ → (𝜑 → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))))
136135com12 33 . . 3 (𝜑 → (𝑑 ∈ ℕ → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑))))
137136imp 412 . 2 ((𝜑 ∧ 𝑑 ∈ ℕ) → ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
138137ralrimiva 3159 1 (𝜑 → ∀𝑑 ∈ ℕ ((𝑑 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑑}) = (ϕ‘𝑑)))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  {crab 3418  ∅c0 4286   class class class wbr 5111  ‘cfv 6540  (class class class)co 7416  Fincfn 8945   < clt 11254   ≤ cle 11255  ℕcn 12244  ♯chash 14379   ∥ cdvds 16327  ϕcphi 16840  Basecbs 17286  0gc0g 17509  Grpcgrp 19023  .gcmg 19156  odcod 19617
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-inf2 9613  ax-cnex 11167  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188  ax-pre-sup 11189
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-disj 5079  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-oadd 8459  df-omul 8460  df-er 8696  df-map 8828  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-sup 9405  df-inf 9406  df-oi 9475  df-card 9937  df-acn 9940  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455  df-div 11883  df-nn 12245  df-2 12314  df-3 12315  df-n0 12516  df-xnn0 12589  df-z 12603  df-uz 12874  df-rp 13028  df-fz 13547  df-fzo 13695  df-fl 13838  df-mod 13916  df-seq 14051  df-exp 14111  df-hash 14380  df-cj 15169  df-re 15170  df-im 15171  df-sqrt 15305  df-abs 15306  df-clim 15558  df-sum 15757  df-dvds 16328  df-gcd 16570  df-phi 16842  df-0g 17511  df-mgm 18715  df-sgrp 18798  df-mnd 18814  df-grp 19026  df-minusg 19027  df-sbg 19028  df-mulg 19157  df-od 19621
This theorem is used by:  unitscyglem4  42998
  Copyright terms: Public domain W3C validator