Metamath Proof Explorer


Theorem 1arymaptf1

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

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

Proof

Step Hyp Ref Expression
1 1arymaptfv.h 𝐻 = ( ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥𝑋 ↦ ( ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) )
2 1 1arymaptf ( 𝑋𝑉𝐻 : ( 1 -aryF 𝑋 ) ⟶ ( 𝑋m 𝑋 ) )
3 1 1arymaptfv ( 𝑓 ∈ ( 1 -aryF 𝑋 ) → ( 𝐻𝑓 ) = ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) )
4 3 ad2antrl ( ( 𝑋𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( 𝐻𝑓 ) = ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) )
5 1 1arymaptfv ( 𝑔 ∈ ( 1 -aryF 𝑋 ) → ( 𝐻𝑔 ) = ( 𝑥𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) )
6 5 ad2antll ( ( 𝑋𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( 𝐻𝑔 ) = ( 𝑥𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) )
7 4 6 eqeq12d ( ( 𝑋𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( ( 𝐻𝑓 ) = ( 𝐻𝑔 ) ↔ ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) = ( 𝑥𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) ) )
8 fvex ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ∈ V
9 8 rgenw 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ∈ V
10 mpteqb ( ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ∈ V → ( ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) = ( 𝑥𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) ↔ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) )
11 9 10 mp1i ( ( 𝑋𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) = ( 𝑥𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) ↔ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) )
12 1aryfvalel ( 𝑋𝑉 → ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↔ 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) )
13 1aryfvalel ( 𝑋𝑉 → ( 𝑔 ∈ ( 1 -aryF 𝑋 ) ↔ 𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) )
14 12 13 anbi12d ( 𝑋𝑉 → ( ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ↔ ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) ) )
15 ffn ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑓 Fn ( 𝑋m { 0 } ) )
16 15 adantr ( ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) → 𝑓 Fn ( 𝑋m { 0 } ) )
17 16 3ad2ant2 ( ( 𝑋𝑉 ∧ ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) → 𝑓 Fn ( 𝑋m { 0 } ) )
18 ffn ( 𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 Fn ( 𝑋m { 0 } ) )
19 18 adantl ( ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) → 𝑔 Fn ( 𝑋m { 0 } ) )
20 19 3ad2ant2 ( ( 𝑋𝑉 ∧ ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) → 𝑔 Fn ( 𝑋m { 0 } ) )
21 elmapi ( 𝑦 ∈ ( 𝑋m { 0 } ) → 𝑦 : { 0 } ⟶ 𝑋 )
22 c0ex 0 ∈ V
23 22 fsn2 ( 𝑦 : { 0 } ⟶ 𝑋 ↔ ( ( 𝑦 ‘ 0 ) ∈ 𝑋𝑦 = { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) )
24 21 23 sylib ( 𝑦 ∈ ( 𝑋m { 0 } ) → ( ( 𝑦 ‘ 0 ) ∈ 𝑋𝑦 = { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) )
25 opeq2 ( 𝑥 = ( 𝑦 ‘ 0 ) → ⟨ 0 , 𝑥 ⟩ = ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ )
26 25 sneqd ( 𝑥 = ( 𝑦 ‘ 0 ) → { ⟨ 0 , 𝑥 ⟩ } = { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } )
27 26 fveq2d ( 𝑥 = ( 𝑦 ‘ 0 ) → ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑓 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) )
28 26 fveq2d ( 𝑥 = ( 𝑦 ‘ 0 ) → ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) )
29 27 28 eqeq12d ( 𝑥 = ( 𝑦 ‘ 0 ) → ( ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ↔ ( 𝑓 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) ) )
30 29 rspccv ( ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) → ( ( 𝑦 ‘ 0 ) ∈ 𝑋 → ( 𝑓 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) ) )
31 30 3ad2ant3 ( ( 𝑋𝑉 ∧ ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) → ( ( 𝑦 ‘ 0 ) ∈ 𝑋 → ( 𝑓 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) ) )
32 31 com12 ( ( 𝑦 ‘ 0 ) ∈ 𝑋 → ( ( 𝑋𝑉 ∧ ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) → ( 𝑓 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) ) )
33 32 adantr ( ( ( 𝑦 ‘ 0 ) ∈ 𝑋𝑦 = { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) → ( ( 𝑋𝑉 ∧ ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) → ( 𝑓 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) ) )
34 fveq2 ( 𝑦 = { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } → ( 𝑓𝑦 ) = ( 𝑓 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) )
35 fveq2 ( 𝑦 = { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } → ( 𝑔𝑦 ) = ( 𝑔 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) )
36 34 35 eqeq12d ( 𝑦 = { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } → ( ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ( 𝑓 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) ) )
37 36 adantl ( ( ( 𝑦 ‘ 0 ) ∈ 𝑋𝑦 = { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) → ( ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ↔ ( 𝑓 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) ) )
38 33 37 sylibrd ( ( ( 𝑦 ‘ 0 ) ∈ 𝑋𝑦 = { ⟨ 0 , ( 𝑦 ‘ 0 ) ⟩ } ) → ( ( 𝑋𝑉 ∧ ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) → ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ) )
39 24 38 syl ( 𝑦 ∈ ( 𝑋m { 0 } ) → ( ( 𝑋𝑉 ∧ ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) → ( 𝑓𝑦 ) = ( 𝑔𝑦 ) ) )
40 39 impcom ( ( ( 𝑋𝑉 ∧ ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) ∧ 𝑦 ∈ ( 𝑋m { 0 } ) ) → ( 𝑓𝑦 ) = ( 𝑔𝑦 ) )
41 17 20 40 eqfnfvd ( ( 𝑋𝑉 ∧ ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) → 𝑓 = 𝑔 )
42 41 3exp ( 𝑋𝑉 → ( ( 𝑓 : ( 𝑋m { 0 } ) ⟶ 𝑋𝑔 : ( 𝑋m { 0 } ) ⟶ 𝑋 ) → ( ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) → 𝑓 = 𝑔 ) ) )
43 14 42 sylbid ( 𝑋𝑉 → ( ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) → ( ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) → 𝑓 = 𝑔 ) ) )
44 43 imp ( ( 𝑋𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( ∀ 𝑥𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) → 𝑓 = 𝑔 ) )
45 11 44 sylbid ( ( 𝑋𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) = ( 𝑥𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) → 𝑓 = 𝑔 ) )
46 7 45 sylbid ( ( 𝑋𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( ( 𝐻𝑓 ) = ( 𝐻𝑔 ) → 𝑓 = 𝑔 ) )
47 46 ralrimivva ( 𝑋𝑉 → ∀ 𝑓 ∈ ( 1 -aryF 𝑋 ) ∀ 𝑔 ∈ ( 1 -aryF 𝑋 ) ( ( 𝐻𝑓 ) = ( 𝐻𝑔 ) → 𝑓 = 𝑔 ) )
48 dff13 ( 𝐻 : ( 1 -aryF 𝑋 ) –1-1→ ( 𝑋m 𝑋 ) ↔ ( 𝐻 : ( 1 -aryF 𝑋 ) ⟶ ( 𝑋m 𝑋 ) ∧ ∀ 𝑓 ∈ ( 1 -aryF 𝑋 ) ∀ 𝑔 ∈ ( 1 -aryF 𝑋 ) ( ( 𝐻𝑓 ) = ( 𝐻𝑔 ) → 𝑓 = 𝑔 ) ) )
49 2 47 48 sylanbrc ( 𝑋𝑉𝐻 : ( 1 -aryF 𝑋 ) –1-1→ ( 𝑋m 𝑋 ) )