Metamath Proof Explorer

Theorem unitscyglem3

Description: Lemma for unitscyg . (Contributed by metakunt, 14-Jul-2025)

Ref Expression
Hypotheses unitscyglem1.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
unitscyglem1.2 ⊢ ↑ = ( .g ‘ 𝐺 )
unitscyglem1.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
unitscyglem1.4 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
unitscyglem1.5 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 )
Assertion unitscyglem3 ( 𝜑 → ∀ 𝑑 ∈ ℕ ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )

Proof

Step Hyp Ref Expression
1 unitscyglem1.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 unitscyglem1.2 ⊢ ↑ = ( .g ‘ 𝐺 )
3 unitscyglem1.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
4 unitscyglem1.4 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
5 unitscyglem1.5 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 )
6 breq1 ⊢ ( 𝑑 = 𝑐 → ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑐 ∥ ( ♯ ‘ 𝐵 ) ) )
7 eqeq2 ⊢ ( 𝑑 = 𝑐 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 ) )
8 7 rabbidv ⊢ ( 𝑑 = 𝑐 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } )
9 8 neeq1d ⊢ ( 𝑑 = 𝑐 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ↔ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) )
10 6 9 anbi12d ⊢ ( 𝑑 = 𝑐 → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ↔ ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) ) )
11 8 fveq2d ⊢ ( 𝑑 = 𝑐 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) )
12 fveq2 ⊢ ( 𝑑 = 𝑐 → ( ϕ ‘ 𝑑 ) = ( ϕ ‘ 𝑐 ) )
13 11 12 eqeq12d ⊢ ( 𝑑 = 𝑐 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ↔ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) )
14 10 13 imbi12d ⊢ ( 𝑑 = 𝑐 → ( ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) ↔ ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
15 14 imbi2d ⊢ ( 𝑑 = 𝑐 → ( ( 𝜑 → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) ) ↔ ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) )
16 simplr ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → 𝜑 )
17 simplll ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → 𝑑 ∈ ℕ )
18 16 17 jca ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → ( 𝜑 ∧ 𝑑 ∈ ℕ ) )
19 breq1 ⊢ ( 𝑐 = 𝑒 → ( 𝑐 < 𝑑 ↔ 𝑒 < 𝑑 ) )
20 breq1 ⊢ ( 𝑐 = 𝑒 → ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑒 ∥ ( ♯ ‘ 𝐵 ) ) )
21 eqeq2 ⊢ ( 𝑐 = 𝑒 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 ) )
22 21 rabbidv ⊢ ( 𝑐 = 𝑒 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } )
23 22 neeq1d ⊢ ( 𝑐 = 𝑒 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ↔ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) )
24 20 23 anbi12d ⊢ ( 𝑐 = 𝑒 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) ↔ ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) ) )
25 22 fveq2d ⊢ ( 𝑐 = 𝑒 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) )
26 fveq2 ⊢ ( 𝑐 = 𝑒 → ( ϕ ‘ 𝑐 ) = ( ϕ ‘ 𝑒 ) )
27 25 26 eqeq12d ⊢ ( 𝑐 = 𝑒 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ↔ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) )
28 24 27 imbi12d ⊢ ( 𝑐 = 𝑒 → ( ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ↔ ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) )
29 28 imbi2d ⊢ ( 𝑐 = 𝑒 → ( ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ↔ ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) )
30 19 29 imbi12d ⊢ ( 𝑐 = 𝑒 → ( ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ↔ ( 𝑒 < 𝑑 → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) ) )
31 simpr ⊢ ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) )
32 31 adantr ⊢ ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) )
33 32 adantr ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) )
34 33 adantr ⊢ ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) )
35 simpr ⊢ ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) → 𝑒 ∈ ℕ )
36 30 34 35 rspcdva ⊢ ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) → ( 𝑒 < 𝑑 → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) )
37 simp-5r ⊢ ( ( ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) ∧ ( 𝑒 < 𝑑 → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) ) ∧ 𝑒 < 𝑑 ) → 𝜑 )
38 simpr ⊢ ( ( ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) ∧ ( 𝑒 < 𝑑 → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) ) ∧ 𝑒 < 𝑑 ) → 𝑒 < 𝑑 )
39 simplr ⊢ ( ( ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) ∧ ( 𝑒 < 𝑑 → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) ) ∧ 𝑒 < 𝑑 ) → ( 𝑒 < 𝑑 → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) )
40 38 39 mpd ⊢ ( ( ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) ∧ ( 𝑒 < 𝑑 → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) ) ∧ 𝑒 < 𝑑 ) → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) )
41 37 40 mpd ⊢ ( ( ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) ∧ ( 𝑒 < 𝑑 → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) ) ∧ 𝑒 < 𝑑 ) → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) )
42 41 ex ⊢ ( ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) ∧ ( 𝑒 < 𝑑 → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) ) → ( 𝑒 < 𝑑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) )
43 42 ex ⊢ ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) → ( ( 𝑒 < 𝑑 → ( 𝜑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) → ( 𝑒 < 𝑑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ) )
44 36 43 mpd ⊢ ( ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) ∧ 𝑒 ∈ ℕ ) → ( 𝑒 < 𝑑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) )
45 44 ralrimiva ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → ∀ 𝑒 ∈ ℕ ( 𝑒 < 𝑑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) )
46 nfv ⊢ Ⅎ 𝑐 ( 𝑒 < 𝑑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) )
47 nfv ⊢ Ⅎ 𝑒 ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) )
48 breq1 ⊢ ( 𝑒 = 𝑐 → ( 𝑒 < 𝑑 ↔ 𝑐 < 𝑑 ) )
49 breq1 ⊢ ( 𝑒 = 𝑐 → ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑐 ∥ ( ♯ ‘ 𝐵 ) ) )
50 eqeq2 ⊢ ( 𝑒 = 𝑐 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 ) )
51 50 rabbidv ⊢ ( 𝑒 = 𝑐 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } )
52 51 neeq1d ⊢ ( 𝑒 = 𝑐 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ↔ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) )
53 49 52 anbi12d ⊢ ( 𝑒 = 𝑐 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) ↔ ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) ) )
54 51 fveq2d ⊢ ( 𝑒 = 𝑐 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) )
55 fveq2 ⊢ ( 𝑒 = 𝑐 → ( ϕ ‘ 𝑒 ) = ( ϕ ‘ 𝑐 ) )
56 54 55 eqeq12d ⊢ ( 𝑒 = 𝑐 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ↔ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) )
57 53 56 imbi12d ⊢ ( 𝑒 = 𝑐 → ( ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ↔ ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
58 48 57 imbi12d ⊢ ( 𝑒 = 𝑐 → ( ( 𝑒 < 𝑑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ↔ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) )
59 46 47 58 cbvralw ⊢ ( ∀ 𝑒 ∈ ℕ ( 𝑒 < 𝑑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) ↔ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
60 59 biimpi ⊢ ( ∀ 𝑒 ∈ ℕ ( 𝑒 < 𝑑 → ( ( 𝑒 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑒 } ) = ( ϕ ‘ 𝑒 ) ) ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
61 45 60 syl ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
62 18 61 jca ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) )
63 simprl ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → 𝑑 ∥ ( ♯ ‘ 𝐵 ) )
64 62 63 jca ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) )
65 simprr ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ )
66 64 65 jca ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) )
67 rabn0 ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 )
68 67 bilani ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 )
69 simp-4l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) )
70 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝑑 ∥ ( ♯ ‘ 𝐵 ) )
71 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝑎 ∈ 𝐵 )
72 69 70 71 jca31 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) )
73 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 )
74 72 73 jca ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) )
75 nfcv ⊢ Ⅎ 𝑥 𝐵
76 nfcv ⊢ Ⅎ 𝑧 𝐵
77 nfv ⊢ Ⅎ 𝑧 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑
78 nfv ⊢ Ⅎ 𝑥 ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑
79 fveqeq2 ⊢ ( 𝑥 = 𝑧 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑 ) )
80 75 76 77 78 79 cbvrabw ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } = { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑 }
81 80 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } = { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑 } )
82 81 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑 } ) )
83 3 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝐺 ∈ Grp )
84 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝐵 ∈ Fin )
85 nfv ⊢ Ⅎ 𝑧 ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 )
86 nfv ⊢ Ⅎ 𝑥 ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 )
87 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑛 ↑ 𝑥 ) = ( 𝑛 ↑ 𝑧 ) )
88 87 eqeq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) ↔ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) ) )
89 75 76 85 86 88 cbvrabw ⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) }
90 89 a1i ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } )
91 90 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) )
92 91 breq1d ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ↔ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ) )
93 92 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ↔ ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ) )
94 93 biimpd ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ) )
95 5 94 mpd ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 )
96 95 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 )
97 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝑑 ∈ ℕ )
98 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝑑 ∥ ( ♯ ‘ 𝐵 ) )
99 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝑎 ∈ 𝐵 )
100 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 )
101 nfv ⊢ Ⅎ 𝑥 ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐
102 nfv ⊢ Ⅎ 𝑧 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐
103 fveqeq2 ⊢ ( 𝑧 = 𝑥 → ( ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 ) )
104 76 75 101 102 103 cbvrabw ⊢ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 }
105 eqcom ⊢ ( { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ↔ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } = { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } )
106 104 105 mpbi ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } = { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 }
107 106 neeq1i ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ↔ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ )
108 107 anbi2i ⊢ ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) ↔ ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) )
109 106 fveq2i ⊢ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } )
110 109 eqeq1i ⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ↔ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) )
111 108 110 imbi12i ⊢ ( ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ↔ ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) )
112 111 imbi2i ⊢ ( ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ↔ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
113 112 biimpi ⊢ ( ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) → ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
114 113 ralimi ⊢ ( ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
115 114 adantl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
116 115 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
117 116 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
118 117 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
119 1 2 83 84 96 97 98 99 100 118 unitscyglem2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
120 82 119 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
121 74 120 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
122 nfv ⊢ Ⅎ 𝑎 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑
123 nfv ⊢ Ⅎ 𝑥 ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑
124 fveqeq2 ⊢ ( 𝑥 = 𝑎 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) )
125 122 123 124 cbvrexw ⊢ ( ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ↔ ∃ 𝑎 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 )
126 125 bilani ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) → ∃ 𝑎 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 )
127 121 126 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
128 127 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )
129 128 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )
130 68 129 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
131 66 130 syl ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
132 131 ex ⊢ ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )
133 132 ex ⊢ ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) → ( 𝜑 → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) ) )
134 133 ex ⊢ ( 𝑑 ∈ ℕ → ( ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) → ( 𝜑 → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) ) ) )
135 15 134 indstr ⊢ ( 𝑑 ∈ ℕ → ( 𝜑 → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) ) )
136 135 com12 ⊢ ( 𝜑 → ( 𝑑 ∈ ℕ → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) ) )
137 136 imp ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )
138 137 ralrimiva ⊢ ( 𝜑 → ∀ 𝑑 ∈ ℕ ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )