This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem symgsubmefmnd

Description: The symmetric group on a set A is a submonoid of the monoid of endofunctions on A . (Contributed by AV, 18-Feb-2024)

Ref Expression
Hypotheses symgsubmefmnd.m ⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
symgsubmefmnd.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
symgsubmefmnd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion symgsubmefmnd ( 𝐴 ∈ 𝑉 → 𝐵 ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 symgsubmefmnd.m ⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
2 symgsubmefmnd.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
3 symgsubmefmnd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 2 3 symgbas ⊢ 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 }
5 inab ⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∩ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } ) = { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1→ 𝐴 ∧ 𝑓 : 𝐴 –onto→ 𝐴 ) }
6 df-f1o ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ↔ ( 𝑓 : 𝐴 –1-1→ 𝐴 ∧ 𝑓 : 𝐴 –onto→ 𝐴 ) )
7 6 bicomi ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐴 ∧ 𝑓 : 𝐴 –onto→ 𝐴 ) ↔ 𝑓 : 𝐴 –1-1-onto→ 𝐴 )
8 7 abbii ⊢ { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1→ 𝐴 ∧ 𝑓 : 𝐴 –onto→ 𝐴 ) } = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 }
9 5 8 eqtr2i ⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } = ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∩ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } )
10 1 injsubmefmnd ⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) )
11 1 sursubmefmnd ⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) )
12 insubm ⊢ ( ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) ∧ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) ) → ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∩ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } ) ∈ ( SubMnd ‘ 𝑀 ) )
13 10 11 12 syl2anc ⊢ ( 𝐴 ∈ 𝑉 → ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ∩ { 𝑓 ∣ 𝑓 : 𝐴 –onto→ 𝐴 } ) ∈ ( SubMnd ‘ 𝑀 ) )
14 9 13 eqeltrid ⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) )
15 4 14 eqeltrid ⊢ ( 𝐴 ∈ 𝑉 → 𝐵 ∈ ( SubMnd ‘ 𝑀 ) )