Metamath Proof Explorer

Theorem 1arymaptfo

Description: The mapping of unary (endo)functions is a function onto the set of endofunctions. (Contributed by AV, 18-May-2024)

Ref Expression
Hypothesis 1arymaptfv.h ⊢ 𝐻 = ( ℎ ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) )
Assertion 1arymaptfo ( 𝑋 ∈ 𝑉 → 𝐻 : ( 1 -aryF 𝑋 ) –onto→ ( 𝑋 ↑m 𝑋 ) )

Proof

Step Hyp Ref Expression
1 1arymaptfv.h ⊢ 𝐻 = ( ℎ ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) )
2 1 1arymaptf ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 1 -aryF 𝑋 ) ⟶ ( 𝑋 ↑m 𝑋 ) )
3 elmapi ⊢ ( 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) → 𝑓 : 𝑋 ⟶ 𝑋 )
4 eqid ⊢ ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) )
5 4 1arympt1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 : 𝑋 ⟶ 𝑋 ) → ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ∈ ( 1 -aryF 𝑋 ) )
6 3 5 sylan2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) → ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ∈ ( 1 -aryF 𝑋 ) )
7 fveq2 ⊢ ( 𝑔 = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) → ( 𝐻 ‘ 𝑔 ) = ( 𝐻 ‘ ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) )
8 7 eqeq2d ⊢ ( 𝑔 = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) → ( 𝑓 = ( 𝐻 ‘ 𝑔 ) ↔ 𝑓 = ( 𝐻 ‘ ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) ) )
9 8 adantl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) ∧ 𝑔 = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) → ( 𝑓 = ( 𝐻 ‘ 𝑔 ) ↔ 𝑓 = ( 𝐻 ‘ ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) ) )
10 3 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) → 𝑓 : 𝑋 ⟶ 𝑋 )
11 10 feqmptd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) → 𝑓 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑥 ) ) )
12 simplr ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) )
13 fveq1 ⊢ ( 𝑎 = { ⟨ 0 , 𝑥 ⟩ } → ( 𝑎 ‘ 0 ) = ( { ⟨ 0 , 𝑥 ⟩ } ‘ 0 ) )
14 c0ex ⊢ 0 ∈ V
15 vex ⊢ 𝑥 ∈ V
16 14 15 fvsn ⊢ ( { ⟨ 0 , 𝑥 ⟩ } ‘ 0 ) = 𝑥
17 13 16 eqtrdi ⊢ ( 𝑎 = { ⟨ 0 , 𝑥 ⟩ } → ( 𝑎 ‘ 0 ) = 𝑥 )
18 17 fveq2d ⊢ ( 𝑎 = { ⟨ 0 , 𝑥 ⟩ } → ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) = ( 𝑓 ‘ 𝑥 ) )
19 18 adantl ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑎 = { ⟨ 0 , 𝑥 ⟩ } ) → ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) = ( 𝑓 ‘ 𝑥 ) )
20 14 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ V )
21 simpr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
22 20 21 fsnd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → { ⟨ 0 , 𝑥 ⟩ } : { 0 } ⟶ 𝑋 )
23 snex ⊢ { 0 } ∈ V
24 23 a1i ⊢ ( 𝑥 ∈ 𝑋 → { 0 } ∈ V )
25 elmapg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 0 } ∈ V ) → ( { ⟨ 0 , 𝑥 ⟩ } ∈ ( 𝑋 ↑m { 0 } ) ↔ { ⟨ 0 , 𝑥 ⟩ } : { 0 } ⟶ 𝑋 ) )
26 24 25 sylan2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → ( { ⟨ 0 , 𝑥 ⟩ } ∈ ( 𝑋 ↑m { 0 } ) ↔ { ⟨ 0 , 𝑥 ⟩ } : { 0 } ⟶ 𝑋 ) )
27 22 26 mpbird ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → { ⟨ 0 , 𝑥 ⟩ } ∈ ( 𝑋 ↑m { 0 } ) )
28 27 ad4ant14 ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) → { ⟨ 0 , 𝑥 ⟩ } ∈ ( 𝑋 ↑m { 0 } ) )
29 fvexd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑥 ) ∈ V )
30 nfv ⊢ Ⅎ 𝑎 ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) )
31 nfmpt1 ⊢ Ⅎ 𝑎 ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) )
32 31 nfeq2 ⊢ Ⅎ 𝑎 ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) )
33 30 32 nfan ⊢ Ⅎ 𝑎 ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) )
34 nfv ⊢ Ⅎ 𝑎 𝑥 ∈ 𝑋
35 33 34 nfan ⊢ Ⅎ 𝑎 ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) ∧ 𝑥 ∈ 𝑋 )
36 nfcv ⊢ Ⅎ 𝑎 { ⟨ 0 , 𝑥 ⟩ }
37 nfcv ⊢ Ⅎ 𝑎 ( 𝑓 ‘ 𝑥 )
38 12 19 28 29 35 36 37 fvmptdf ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑓 ‘ 𝑥 ) )
39 38 mpteq2dva ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑥 ) ) )
40 simpl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) → 𝑋 ∈ 𝑉 )
41 40 mptexd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑥 ) ) ∈ V )
42 1 39 6 41 fvmptd2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) → ( 𝐻 ‘ ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑥 ) ) )
43 11 42 eqtr4d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) → 𝑓 = ( 𝐻 ‘ ( 𝑎 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝑓 ‘ ( 𝑎 ‘ 0 ) ) ) ) )
44 6 9 43 rspcedvd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ) → ∃ 𝑔 ∈ ( 1 -aryF 𝑋 ) 𝑓 = ( 𝐻 ‘ 𝑔 ) )
45 44 ralrimiva ⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ∃ 𝑔 ∈ ( 1 -aryF 𝑋 ) 𝑓 = ( 𝐻 ‘ 𝑔 ) )
46 dffo3 ⊢ ( 𝐻 : ( 1 -aryF 𝑋 ) –onto→ ( 𝑋 ↑m 𝑋 ) ↔ ( 𝐻 : ( 1 -aryF 𝑋 ) ⟶ ( 𝑋 ↑m 𝑋 ) ∧ ∀ 𝑓 ∈ ( 𝑋 ↑m 𝑋 ) ∃ 𝑔 ∈ ( 1 -aryF 𝑋 ) 𝑓 = ( 𝐻 ‘ 𝑔 ) ) )
47 2 45 46 sylanbrc ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 1 -aryF 𝑋 ) –onto→ ( 𝑋 ↑m 𝑋 ) )