Metamath Proof Explorer

Theorem idomsubgmo

Description: The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015) (Revised by NM, 17-Jun-2017)

Ref Expression
Hypothesis idomsubgmo.g ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
Assertion idomsubgmo ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ∃* 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑦 ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 idomsubgmo.g ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
2 fvex ⊢ ( Base ‘ 𝐺 ) ∈ V
3 2 rabex ⊢ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ∈ V
4 simp2l ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑦 ∈ ( SubGrp ‘ 𝐺 ) )
5 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 5 subgss ⊢ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) → 𝑦 ⊆ ( Base ‘ 𝐺 ) )
7 4 6 syl ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑦 ⊆ ( Base ‘ 𝐺 ) )
8 simpl2l ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑦 ) → 𝑦 ∈ ( SubGrp ‘ 𝐺 ) )
9 simp3l ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( ♯ ‘ 𝑦 ) = 𝑁 )
10 simp1r ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑁 ∈ ℕ )
11 10 nnnn0d ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑁 ∈ ℕ0 )
12 9 11 eqeltrd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
13 vex ⊢ 𝑦 ∈ V
14 hashclb ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ Fin ↔ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ) )
15 13 14 ax-mp ⊢ ( 𝑦 ∈ Fin ↔ ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
16 12 15 sylibr ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑦 ∈ Fin )
17 16 adantr ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑦 ) → 𝑦 ∈ Fin )
18 simpr ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝑦 )
19 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
20 19 odsubdvds ⊢ ( ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑦 ∈ Fin ∧ 𝑧 ∈ 𝑦 ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ ( ♯ ‘ 𝑦 ) )
21 8 17 18 20 syl3anc ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑦 ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ ( ♯ ‘ 𝑦 ) )
22 9 adantr ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ 𝑦 ) = 𝑁 )
23 21 22 breqtrd ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑦 ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 )
24 7 23 ssrabdv ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑦 ⊆ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } )
25 simp2r ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) )
26 5 subgss ⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥 ⊆ ( Base ‘ 𝐺 ) )
27 25 26 syl ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑥 ⊆ ( Base ‘ 𝐺 ) )
28 simpl2r ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑥 ) → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) )
29 simp3r ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( ♯ ‘ 𝑥 ) = 𝑁 )
30 29 11 eqeltrd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
31 vex ⊢ 𝑥 ∈ V
32 hashclb ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ Fin ↔ ( ♯ ‘ 𝑥 ) ∈ ℕ0 ) )
33 31 32 ax-mp ⊢ ( 𝑥 ∈ Fin ↔ ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
34 30 33 sylibr ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑥 ∈ Fin )
35 34 adantr ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑥 ) → 𝑥 ∈ Fin )
36 simpr ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 )
37 19 odsubdvds ⊢ ( ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ Fin ∧ 𝑧 ∈ 𝑥 ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ ( ♯ ‘ 𝑥 ) )
38 28 35 36 37 syl3anc ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑥 ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ ( ♯ ‘ 𝑥 ) )
39 29 adantr ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑥 ) → ( ♯ ‘ 𝑥 ) = 𝑁 )
40 38 39 breqtrd ⊢ ( ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) ∧ 𝑧 ∈ 𝑥 ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 )
41 27 40 ssrabdv ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑥 ⊆ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } )
42 24 41 unssd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( 𝑦 ∪ 𝑥 ) ⊆ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } )
43 ssdomg ⊢ ( { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ∈ V → ( ( 𝑦 ∪ 𝑥 ) ⊆ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } → ( 𝑦 ∪ 𝑥 ) ≼ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ) )
44 3 42 43 mpsyl ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( 𝑦 ∪ 𝑥 ) ≼ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } )
45 1 5 19 idomodle ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ) ≤ 𝑁 )
46 45 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ) ≤ 𝑁 )
47 46 9 breqtrrd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ) ≤ ( ♯ ‘ 𝑦 ) )
48 3 a1i ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ∈ V )
49 hashbnd ⊢ ( ( { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ∈ V ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ∧ ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ) ≤ ( ♯ ‘ 𝑦 ) ) → { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ∈ Fin )
50 48 12 47 49 syl3anc ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ∈ Fin )
51 hashdom ⊢ ( ( { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ∈ Fin ∧ 𝑦 ∈ V ) → ( ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ) ≤ ( ♯ ‘ 𝑦 ) ↔ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ≼ 𝑦 ) )
52 50 13 51 sylancl ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ) ≤ ( ♯ ‘ 𝑦 ) ↔ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ≼ 𝑦 ) )
53 47 52 mpbid ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ≼ 𝑦 )
54 domtr ⊢ ( ( ( 𝑦 ∪ 𝑥 ) ≼ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ∧ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∥ 𝑁 } ≼ 𝑦 ) → ( 𝑦 ∪ 𝑥 ) ≼ 𝑦 )
55 44 53 54 syl2anc ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( 𝑦 ∪ 𝑥 ) ≼ 𝑦 )
56 13 31 unex ⊢ ( 𝑦 ∪ 𝑥 ) ∈ V
57 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ 𝑥 )
58 ssdomg ⊢ ( ( 𝑦 ∪ 𝑥 ) ∈ V → ( 𝑦 ⊆ ( 𝑦 ∪ 𝑥 ) → 𝑦 ≼ ( 𝑦 ∪ 𝑥 ) ) )
59 56 57 58 mp2 ⊢ 𝑦 ≼ ( 𝑦 ∪ 𝑥 )
60 sbth ⊢ ( ( ( 𝑦 ∪ 𝑥 ) ≼ 𝑦 ∧ 𝑦 ≼ ( 𝑦 ∪ 𝑥 ) ) → ( 𝑦 ∪ 𝑥 ) ≈ 𝑦 )
61 55 59 60 sylancl ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( 𝑦 ∪ 𝑥 ) ≈ 𝑦 )
62 9 29 eqtr4d ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑥 ) )
63 hashen ⊢ ( ( 𝑦 ∈ Fin ∧ 𝑥 ∈ Fin ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑥 ) ↔ 𝑦 ≈ 𝑥 ) )
64 16 34 63 syl2anc ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑥 ) ↔ 𝑦 ≈ 𝑥 ) )
65 62 64 mpbid ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑦 ≈ 𝑥 )
66 fiuneneq ⊢ ( ( 𝑦 ≈ 𝑥 ∧ 𝑦 ∈ Fin ) → ( ( 𝑦 ∪ 𝑥 ) ≈ 𝑦 ↔ 𝑦 = 𝑥 ) )
67 65 16 66 syl2anc ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → ( ( 𝑦 ∪ 𝑥 ) ≈ 𝑦 ↔ 𝑦 = 𝑥 ) )
68 61 67 mpbid ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ) → 𝑦 = 𝑥 )
69 68 3expia ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ( ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → 𝑦 = 𝑥 ) )
70 69 ralrimivva ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → 𝑦 = 𝑥 ) )
71 fveqeq2 ⊢ ( 𝑦 = 𝑥 → ( ( ♯ ‘ 𝑦 ) = 𝑁 ↔ ( ♯ ‘ 𝑥 ) = 𝑁 ) )
72 71 rmo4 ⊢ ( ∃* 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑦 ) = 𝑁 ↔ ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ( ( ♯ ‘ 𝑦 ) = 𝑁 ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → 𝑦 = 𝑥 ) )
73 70 72 sylibr ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ∃* 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑦 ) = 𝑁 )