Step |
Hyp |
Ref |
Expression |
1 |
|
symgpssefmnd.m |
⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 ) |
2 |
|
symgpssefmnd.g |
⊢ 𝐺 = ( SymGrp ‘ 𝐴 ) |
3 |
|
hashgt12el |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ) |
4 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
5 |
2 4
|
symgbasmap |
⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) → 𝑥 ∈ ( 𝐴 ↑m 𝐴 ) ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) |
7 |
1 6
|
efmndbas |
⊢ ( Base ‘ 𝑀 ) = ( 𝐴 ↑m 𝐴 ) |
8 |
5 7
|
eleqtrrdi |
⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) → 𝑥 ∈ ( Base ‘ 𝑀 ) ) |
9 |
8
|
ssriv |
⊢ ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝑀 ) |
10 |
9
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝑀 ) ) |
11 |
|
fconst6g |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐴 ) |
12 |
11
|
adantr |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐴 ) |
13 |
12
|
3ad2ant2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐴 ) |
14 |
1 6
|
elefmndbas |
⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝑀 ) ↔ ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐴 ) ) |
15 |
14
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝑀 ) ↔ ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐴 ) ) |
16 |
13 15
|
mpbird |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝑀 ) ) |
17 |
|
fconstg |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } ) |
18 |
17
|
adantr |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } ) |
19 |
18
|
3ad2ant2 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } ) |
20 |
|
id |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) ) |
21 |
20
|
3expa |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) ) |
22 |
21
|
3adant1 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) ) |
23 |
|
nf1oconst |
⊢ ( ( ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) ) → ¬ ( 𝐴 × { 𝑥 } ) : 𝐴 –1-1-onto→ 𝐴 ) |
24 |
19 22 23
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ¬ ( 𝐴 × { 𝑥 } ) : 𝐴 –1-1-onto→ 𝐴 ) |
25 |
2 4
|
elsymgbas |
⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝐺 ) ↔ ( 𝐴 × { 𝑥 } ) : 𝐴 –1-1-onto→ 𝐴 ) ) |
26 |
25
|
notbid |
⊢ ( 𝐴 ∈ 𝑉 → ( ¬ ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝐺 ) ↔ ¬ ( 𝐴 × { 𝑥 } ) : 𝐴 –1-1-onto→ 𝐴 ) ) |
27 |
26
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( ¬ ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝐺 ) ↔ ¬ ( 𝐴 × { 𝑥 } ) : 𝐴 –1-1-onto→ 𝐴 ) ) |
28 |
24 27
|
mpbird |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ¬ ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝐺 ) ) |
29 |
10 16 28
|
ssnelpssd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) ) |
30 |
29
|
3exp |
⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≠ 𝑦 → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) ) ) ) |
31 |
30
|
rexlimdvv |
⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) ) ) |
32 |
31
|
adantr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) ) ) |
33 |
3 32
|
mpd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) ) |