Metamath Proof Explorer

Theorem sursubmefmnd

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

Ref Expression
Hypothesis sursubmefmnd.m ⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
Assertion sursubmefmnd ( 𝐴 ∈ 𝑉 → { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 sursubmefmnd.m ⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
2 vex ⊢ 𝑥 ∈ V
3 foeq1 ⊢ ( ℎ = 𝑥 → ( ℎ : 𝐴 –onto→ 𝐴 ↔ 𝑥 : 𝐴 –onto→ 𝐴 ) )
4 2 3 elab ⊢ ( 𝑥 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ↔ 𝑥 : 𝐴 –onto→ 𝐴 )
5 fof ⊢ ( 𝑥 : 𝐴 –onto→ 𝐴 → 𝑥 : 𝐴 ⟶ 𝐴 )
6 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
7 1 6 elefmndbas ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( Base ‘ 𝑀 ) ↔ 𝑥 : 𝐴 ⟶ 𝐴 ) )
8 5 7 syl5ibr ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 : 𝐴 –onto→ 𝐴 → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
9 4 8 syl5bi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
10 9 ssrdv ⊢ ( 𝐴 ∈ 𝑉 → { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ⊆ ( Base ‘ 𝑀 ) )
11 1 efmndid ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) = ( 0g ‘ 𝑀 ) )
12 resiexg ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ V )
13 f1oi ⊢ ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴
14 f1ofo ⊢ ( ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴 → ( I ↾ 𝐴 ) : 𝐴 –onto→ 𝐴 )
15 13 14 mp1i ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) : 𝐴 –onto→ 𝐴 )
16 foeq1 ⊢ ( ℎ = ( I ↾ 𝐴 ) → ( ℎ : 𝐴 –onto→ 𝐴 ↔ ( I ↾ 𝐴 ) : 𝐴 –onto→ 𝐴 ) )
17 12 15 16 elabd ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } )
18 11 17 eqeltrrd ⊢ ( 𝐴 ∈ 𝑉 → ( 0g ‘ 𝑀 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } )
19 vex ⊢ 𝑦 ∈ V
20 foeq1 ⊢ ( ℎ = 𝑦 → ( ℎ : 𝐴 –onto→ 𝐴 ↔ 𝑦 : 𝐴 –onto→ 𝐴 ) )
21 19 20 elab ⊢ ( 𝑦 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ↔ 𝑦 : 𝐴 –onto→ 𝐴 )
22 4 21 anbi12i ⊢ ( ( 𝑥 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∧ 𝑦 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ) ↔ ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) )
23 foco ⊢ ( ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) → ( 𝑥 ∘ 𝑦 ) : 𝐴 –onto→ 𝐴 )
24 23 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) ) → ( 𝑥 ∘ 𝑦 ) : 𝐴 –onto→ 𝐴 )
25 fof ⊢ ( 𝑦 : 𝐴 –onto→ 𝐴 → 𝑦 : 𝐴 ⟶ 𝐴 )
26 5 25 anim12i ⊢ ( ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) → ( 𝑥 : 𝐴 ⟶ 𝐴 ∧ 𝑦 : 𝐴 ⟶ 𝐴 ) )
27 1 6 elefmndbas ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ ( Base ‘ 𝑀 ) ↔ 𝑦 : 𝐴 ⟶ 𝐴 ) )
28 7 27 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ↔ ( 𝑥 : 𝐴 ⟶ 𝐴 ∧ 𝑦 : 𝐴 ⟶ 𝐴 ) ) )
29 26 28 syl5ibr ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) → ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) )
30 29 imp ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) )
31 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
32 1 6 31 efmndov ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
33 30 32 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
34 33 eleq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ↔ ( 𝑥 ∘ 𝑦 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ) )
35 2 19 coex ⊢ ( 𝑥 ∘ 𝑦 ) ∈ V
36 foeq1 ⊢ ( ℎ = ( 𝑥 ∘ 𝑦 ) → ( ℎ : 𝐴 –onto→ 𝐴 ↔ ( 𝑥 ∘ 𝑦 ) : 𝐴 –onto→ 𝐴 ) )
37 35 36 elab ⊢ ( ( 𝑥 ∘ 𝑦 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ↔ ( 𝑥 ∘ 𝑦 ) : 𝐴 –onto→ 𝐴 )
38 34 37 bitrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ↔ ( 𝑥 ∘ 𝑦 ) : 𝐴 –onto→ 𝐴 ) )
39 24 38 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } )
40 39 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 : 𝐴 –onto→ 𝐴 ∧ 𝑦 : 𝐴 –onto→ 𝐴 ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ) )
41 22 40 syl5bi ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∧ 𝑦 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ) )
42 41 ralrimivv ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∀ 𝑦 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } )
43 1 efmndmnd ⊢ ( 𝐴 ∈ 𝑉 → 𝑀 ∈ Mnd )
44 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
45 6 44 31 issubm ⊢ ( 𝑀 ∈ Mnd → ( { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) ↔ ( { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∧ ∀ 𝑥 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∀ 𝑦 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ) ) )
46 43 45 syl ⊢ ( 𝐴 ∈ 𝑉 → ( { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) ↔ ( { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∧ ∀ 𝑥 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∀ 𝑦 ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ) ) )
47 10 18 42 46 mpbir3and ⊢ ( 𝐴 ∈ 𝑉 → { ℎ ∣ ℎ : 𝐴 –onto→ 𝐴 } ∈ ( SubMnd ‘ 𝑀 ) )