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 biimpi ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ → ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 )
69 68 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 )
70 simp-4l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) )
71 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝑑 ∥ ( ♯ ‘ 𝐵 ) )
72 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝑎 ∈ 𝐵 )
73 70 71 72 jca31 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) )
74 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 )
75 73 74 jca ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) )
76 nfcv ⊢ Ⅎ 𝑥 𝐵
77 nfcv ⊢ Ⅎ 𝑧 𝐵
78 nfv ⊢ Ⅎ 𝑧 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑
79 nfv ⊢ Ⅎ 𝑥 ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑
80 fveqeq2 ⊢ ( 𝑥 = 𝑧 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑 ) )
81 76 77 78 79 80 cbvrabw ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } = { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑 }
82 81 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } = { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑 } )
83 82 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑 } ) )
84 3 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝐺 ∈ Grp )
85 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝐵 ∈ Fin )
86 nfv ⊢ Ⅎ 𝑧 ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 )
87 nfv ⊢ Ⅎ 𝑥 ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 )
88 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑛 ↑ 𝑥 ) = ( 𝑛 ↑ 𝑧 ) )
89 88 eqeq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) ↔ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) ) )
90 76 77 86 87 89 cbvrabw ⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) }
91 90 a1i ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } )
92 91 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) )
93 92 breq1d ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ↔ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ) )
94 93 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ↔ ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ) )
95 94 biimpd ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ) )
96 5 95 mpd ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 )
97 96 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 )
98 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝑑 ∈ ℕ )
99 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝑑 ∥ ( ♯ ‘ 𝐵 ) )
100 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → 𝑎 ∈ 𝐵 )
101 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 )
102 nfv ⊢ Ⅎ 𝑥 ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐
103 nfv ⊢ Ⅎ 𝑧 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐
104 fveqeq2 ⊢ ( 𝑧 = 𝑥 → ( ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 ) )
105 77 76 102 103 104 cbvrabw ⊢ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 }
106 eqcom ⊢ ( { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ↔ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } = { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } )
107 105 106 mpbi ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } = { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 }
108 107 neeq1i ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ↔ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ )
109 108 anbi2i ⊢ ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) ↔ ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) )
110 107 fveq2i ⊢ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } )
111 110 eqeq1i ⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ↔ ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) )
112 109 111 imbi12i ⊢ ( ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ↔ ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) )
113 112 imbi2i ⊢ ( ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ↔ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
114 113 biimpi ⊢ ( ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) → ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
115 114 ralimi ⊢ ( ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
116 115 adantl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
117 116 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
118 117 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
119 118 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
120 1 2 84 85 97 98 99 100 101 119 unitscyglem2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ♯ ‘ { 𝑧 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
121 83 120 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
122 75 121 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
123 nfv ⊢ Ⅎ 𝑎 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑
124 nfv ⊢ Ⅎ 𝑥 ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑
125 fveqeq2 ⊢ ( 𝑥 = 𝑎 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 ) )
126 123 124 125 cbvrexw ⊢ ( ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ↔ ∃ 𝑎 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 )
127 126 biimpi ⊢ ( ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 → ∃ 𝑎 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 )
128 127 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) → ∃ 𝑎 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑎 ) = 𝑑 )
129 122 128 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
130 129 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )
131 130 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )
132 69 131 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ∧ 𝑑 ∥ ( ♯ ‘ 𝐵 ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
133 66 132 syl ⊢ ( ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) ∧ ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) )
134 133 ex ⊢ ( ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) ∧ 𝜑 ) → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )
135 134 ex ⊢ ( ( 𝑑 ∈ ℕ ∧ ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) ) → ( 𝜑 → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) ) )
136 135 ex ⊢ ( 𝑑 ∈ ℕ → ( ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝑑 → ( 𝜑 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ) → ( 𝜑 → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) ) ) )
137 15 136 indstr ⊢ ( 𝑑 ∈ ℕ → ( 𝜑 → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) ) )
138 137 com12 ⊢ ( 𝜑 → ( 𝑑 ∈ ℕ → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) ) )
139 138 imp ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℕ ) → ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )
140 139 ralrimiva ⊢ ( 𝜑 → ∀ 𝑑 ∈ ℕ ( ( 𝑑 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑑 } ) = ( ϕ ‘ 𝑑 ) ) )