Metamath Proof Explorer

Theorem unitscyglem1

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

Ref Expression
Hypotheses unitscyglem1.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
unitscyglem1.2 ⊢ ↑ = ( .g ‘ 𝐺 )
unitscyglem1.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
unitscyglem1.4 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
unitscyglem1.5 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 )
unitscyglem1.6 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion unitscyglem1 ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ( 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 unitscyglem1.6 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7 oveq1 ⊢ ( 𝑛 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) → ( 𝑛 ↑ 𝑥 ) = ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) )
8 7 eqeq1d ⊢ ( 𝑛 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) → ( ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) ↔ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
9 8 rabbidv ⊢ ( 𝑛 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } = { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
10 9 fveq2d ⊢ ( 𝑛 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
11 id ⊢ ( 𝑛 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) → 𝑛 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) )
12 10 11 breq12d ⊢ ( 𝑛 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 ↔ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) )
13 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
14 1 13 odcl2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℕ )
15 3 4 6 14 syl3anc ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℕ )
16 12 5 15 rspcdva ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) )
17 eqid ⊢ ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) = ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) )
18 1 13 2 17 dfod2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = if ( ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ∈ Fin , ( ♯ ‘ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ) , 0 ) )
19 3 6 18 syl2anc ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = if ( ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ∈ Fin , ( ♯ ‘ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ) , 0 ) )
20 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℤ ) → 𝐺 ∈ Grp )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℤ )
22 6 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℤ ) → 𝐴 ∈ 𝐵 )
23 1 2 20 21 22 mulgcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ↑ 𝐴 ) ∈ 𝐵 )
24 23 fmpttd ⊢ ( 𝜑 → ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) : ℤ ⟶ 𝐵 )
25 frn ⊢ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) : ℤ ⟶ 𝐵 → ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ⊆ 𝐵 )
26 24 25 syl ⊢ ( 𝜑 → ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ⊆ 𝐵 )
27 4 26 ssfid ⊢ ( 𝜑 → ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ∈ Fin )
28 27 iftrued ⊢ ( 𝜑 → if ( ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ∈ Fin , ( ♯ ‘ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ) , 0 ) = ( ♯ ‘ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ) )
29 19 28 eqtrd ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( ♯ ‘ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ) )
30 eqid ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } = { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) }
31 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) ∈ V )
32 1 31 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ V )
33 30 32 rabexd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ∈ V )
34 ovexd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ↑ 𝐴 ) ∈ V )
35 34 fmpttd ⊢ ( 𝜑 → ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) : ℤ ⟶ V )
36 35 ffnd ⊢ ( 𝜑 → ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) Fn ℤ )
37 fvelrnb ⊢ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) Fn ℤ → ( 𝑦 ∈ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ↔ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) )
38 36 37 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ↔ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) )
39 38 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ) → ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 )
40 id ⊢ ( ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦 → ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦 )
41 40 eqcomd ⊢ ( ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦 → 𝑦 = ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) )
42 41 adantl ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦 ) → 𝑦 = ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) )
43 simpll ⊢ ( ( ( 𝜑 ∧ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) ∧ 𝑤 ∈ ℤ ) → 𝜑 )
44 simpr ⊢ ( ( ( 𝜑 ∧ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) ∧ 𝑤 ∈ ℤ ) → 𝑤 ∈ ℤ )
45 43 44 jca ⊢ ( ( ( 𝜑 ∧ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) ∧ 𝑤 ∈ ℤ ) → ( 𝜑 ∧ 𝑤 ∈ ℤ ) )
46 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) = ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) )
47 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) ∧ 𝑖 = 𝑤 ) → 𝑖 = 𝑤 )
48 47 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) ∧ 𝑖 = 𝑤 ) → ( 𝑖 ↑ 𝐴 ) = ( 𝑤 ↑ 𝐴 ) )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → 𝑤 ∈ ℤ )
50 ovexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( 𝑤 ↑ 𝐴 ) ∈ V )
51 46 48 49 50 fvmptd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = ( 𝑤 ↑ 𝐴 ) )
52 oveq2 ⊢ ( 𝑥 = ( 𝑤 ↑ 𝐴 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ ( 𝑤 ↑ 𝐴 ) ) )
53 52 eqeq1d ⊢ ( 𝑥 = ( 𝑤 ↑ 𝐴 ) → ( ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) ↔ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ ( 𝑤 ↑ 𝐴 ) ) = ( 0g ‘ 𝐺 ) ) )
54 3 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → 𝐺 ∈ Grp )
55 6 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → 𝐴 ∈ 𝐵 )
56 1 2 54 49 55 mulgcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( 𝑤 ↑ 𝐴 ) ∈ 𝐵 )
57 15 nnzd ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ )
59 49 58 55 3jca ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( 𝑤 ∈ ℤ ∧ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ ∧ 𝐴 ∈ 𝐵 ) )
60 1 2 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑤 ∈ ℤ ∧ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 𝑤 · ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 𝐴 ) = ( 𝑤 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝐴 ) ) )
61 54 59 60 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( ( 𝑤 · ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 𝐴 ) = ( 𝑤 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝐴 ) ) )
62 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
63 1 13 2 62 odid ⊢ ( 𝐴 ∈ 𝐵 → ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝐴 ) = ( 0g ‘ 𝐺 ) )
64 55 63 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝐴 ) = ( 0g ‘ 𝐺 ) )
65 64 oveq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( 𝑤 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝐴 ) ) = ( 𝑤 ↑ ( 0g ‘ 𝐺 ) ) )
66 1 2 62 mulgz ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑤 ∈ ℤ ) → ( 𝑤 ↑ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
67 3 66 sylan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( 𝑤 ↑ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
68 65 67 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( 𝑤 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
69 61 68 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( 0g ‘ 𝐺 ) = ( ( 𝑤 · ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 𝐴 ) )
70 59 simp2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ )
71 70 49 55 3jca ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ 𝐴 ∈ 𝐵 ) )
72 1 2 mulgassr ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 𝑤 · ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 𝐴 ) = ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ ( 𝑤 ↑ 𝐴 ) ) )
73 54 71 72 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( ( 𝑤 · ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 𝐴 ) = ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ ( 𝑤 ↑ 𝐴 ) ) )
74 69 73 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ ( 𝑤 ↑ 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
75 53 56 74 elrabd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( 𝑤 ↑ 𝐴 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
76 51 75 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℤ ) → ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
77 45 76 syl ⊢ ( ( ( 𝜑 ∧ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) ∧ 𝑤 ∈ ℤ ) → ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
78 77 adantr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦 ) → ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
79 42 78 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦 ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
80 nfv ⊢ Ⅎ 𝑤 ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦
81 nfv ⊢ Ⅎ 𝑧 ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦
82 fveqeq2 ⊢ ( 𝑧 = 𝑤 → ( ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ↔ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦 ) )
83 80 81 82 cbvrexw ⊢ ( ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑤 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦 )
84 83 biimpi ⊢ ( ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 → ∃ 𝑤 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦 )
85 84 adantl ⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) → ∃ 𝑤 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑤 ) = 𝑦 )
86 79 85 r19.29a ⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
87 86 ex ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ) → ( ∃ 𝑧 ∈ ℤ ( ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ‘ 𝑧 ) = 𝑦 → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
89 39 88 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
90 89 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
91 90 ssrdv ⊢ ( 𝜑 → ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
92 hashss ⊢ ( ( { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ∈ V ∧ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) → ( ♯ ‘ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
93 33 91 92 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ran ( 𝑖 ∈ ℤ ↦ ( 𝑖 ↑ 𝐴 ) ) ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
94 29 93 eqbrtrd ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
95 16 94 jca ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ) )
96 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ⊆ 𝐵
97 96 a1i ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ⊆ 𝐵 )
98 4 97 ssfid ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ∈ Fin )
99 hashcl ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ∈ ℕ0 )
100 98 99 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ∈ ℕ0 )
101 100 nn0red ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ∈ ℝ )
102 15 nnred ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℝ )
103 101 102 letri3d ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↔ ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ) ) )
104 95 103 mpbird ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) )