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 ‘ 𝐺 ) ( ♯ ‘ 𝑦 ) = 𝑁 )