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 𝑋 ) )