Metamath Proof Explorer

Theorem 2arymaptfo

Description: The mapping of binary (endo)functions is a function onto the set of binary operations. (Contributed by AV, 23-May-2024)

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

Proof

Step Hyp Ref Expression
1 2arymaptf.h ⊢ 𝐻 = ( ℎ ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
2 1 2arymaptf ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 2 -aryF 𝑋 ) ⟶ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )
3 elmapi ⊢ ( 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) → 𝑓 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
4 eqid ⊢ ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) )
5 4 2arympt ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ∈ ( 2 -aryF 𝑋 ) )
6 3 5 sylan2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) → ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ∈ ( 2 -aryF 𝑋 ) )
7 fveq2 ⊢ ( 𝑔 = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) → ( 𝐻 ‘ 𝑔 ) = ( 𝐻 ‘ ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) )
8 7 eqeq2d ⊢ ( 𝑔 = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) → ( 𝑓 = ( 𝐻 ‘ 𝑔 ) ↔ 𝑓 = ( 𝐻 ‘ ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) ) )
9 8 adantl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ∧ 𝑔 = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) → ( 𝑓 = ( 𝐻 ‘ 𝑔 ) ↔ 𝑓 = ( 𝐻 ‘ ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) ) )
10 elmapfn ⊢ ( 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) → 𝑓 Fn ( 𝑋 × 𝑋 ) )
11 10 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) → 𝑓 Fn ( 𝑋 × 𝑋 ) )
12 fnov ⊢ ( 𝑓 Fn ( 𝑋 × 𝑋 ) ↔ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝑓 𝑦 ) ) )
13 11 12 sylib ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) → 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝑓 𝑦 ) ) )
14 simp1r ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) )
15 fveq1 ⊢ ( 𝑎 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } → ( 𝑎 ‘ 0 ) = ( { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ‘ 0 ) )
16 0ne1 ⊢ 0 ≠ 1
17 c0ex ⊢ 0 ∈ V
18 vex ⊢ 𝑥 ∈ V
19 17 18 fvpr1 ⊢ ( 0 ≠ 1 → ( { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ‘ 0 ) = 𝑥 )
20 16 19 ax-mp ⊢ ( { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ‘ 0 ) = 𝑥
21 15 20 eqtrdi ⊢ ( 𝑎 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } → ( 𝑎 ‘ 0 ) = 𝑥 )
22 fveq1 ⊢ ( 𝑎 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } → ( 𝑎 ‘ 1 ) = ( { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ‘ 1 ) )
23 1ex ⊢ 1 ∈ V
24 vex ⊢ 𝑦 ∈ V
25 23 24 fvpr2 ⊢ ( 0 ≠ 1 → ( { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ‘ 1 ) = 𝑦 )
26 16 25 ax-mp ⊢ ( { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ‘ 1 ) = 𝑦
27 22 26 eqtrdi ⊢ ( 𝑎 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } → ( 𝑎 ‘ 1 ) = 𝑦 )
28 21 27 oveq12d ⊢ ( 𝑎 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } → ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) = ( 𝑥 𝑓 𝑦 ) )
29 28 adantl ⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑎 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) → ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) = ( 𝑥 𝑓 𝑦 ) )
30 17 23 pm3.2i ⊢ ( 0 ∈ V ∧ 1 ∈ V )
31 fprg ⊢ ( ( ( 0 ∈ V ∧ 1 ∈ V ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ 0 ≠ 1 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } : { 0 , 1 } ⟶ { 𝑥 , 𝑦 } )
32 30 16 31 mp3an13 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } : { 0 , 1 } ⟶ { 𝑥 , 𝑦 } )
33 32 3adant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } : { 0 , 1 } ⟶ { 𝑥 , 𝑦 } )
34 prssi ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → { 𝑥 , 𝑦 } ⊆ 𝑋 )
35 34 3adant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → { 𝑥 , 𝑦 } ⊆ 𝑋 )
36 33 35 fssd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } : { 0 , 1 } ⟶ 𝑋 )
37 simp1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 𝑋 ∈ 𝑉 )
38 prex ⊢ { 0 , 1 } ∈ V
39 38 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → { 0 , 1 } ∈ V )
40 37 39 elmapd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ ( 𝑋 ↑m { 0 , 1 } ) ↔ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } : { 0 , 1 } ⟶ 𝑋 ) )
41 36 40 mpbird ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ ( 𝑋 ↑m { 0 , 1 } ) )
42 41 3adant1r ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ ( 𝑋 ↑m { 0 , 1 } ) )
43 42 3adant1r ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ ( 𝑋 ↑m { 0 , 1 } ) )
44 ovexd ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑓 𝑦 ) ∈ V )
45 nfv ⊢ Ⅎ 𝑎 ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )
46 nfmpt1 ⊢ Ⅎ 𝑎 ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) )
47 46 nfeq2 ⊢ Ⅎ 𝑎 ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) )
48 45 47 nfan ⊢ Ⅎ 𝑎 ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) )
49 nfv ⊢ Ⅎ 𝑎 𝑥 ∈ 𝑋
50 nfv ⊢ Ⅎ 𝑎 𝑦 ∈ 𝑋
51 48 49 50 nf3an ⊢ Ⅎ 𝑎 ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 )
52 nfcv ⊢ Ⅎ 𝑎 { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ }
53 nfcv ⊢ Ⅎ 𝑎 ( 𝑥 𝑓 𝑦 )
54 14 29 43 44 51 52 53 fvmptdf ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑥 𝑓 𝑦 ) )
55 54 mpoeq3dva ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ∧ ℎ = ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝑓 𝑦 ) ) )
56 mpoexga ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝑓 𝑦 ) ) ∈ V )
57 56 anidms ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝑓 𝑦 ) ) ∈ V )
58 57 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝑓 𝑦 ) ) ∈ V )
59 1 55 6 58 fvmptd2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) → ( 𝐻 ‘ ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝑓 𝑦 ) ) )
60 13 59 eqtr4d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) → 𝑓 = ( 𝐻 ‘ ( 𝑎 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑎 ‘ 0 ) 𝑓 ( 𝑎 ‘ 1 ) ) ) ) )
61 6 9 60 rspcedvd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) → ∃ 𝑔 ∈ ( 2 -aryF 𝑋 ) 𝑓 = ( 𝐻 ‘ 𝑔 ) )
62 61 ralrimiva ⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ∃ 𝑔 ∈ ( 2 -aryF 𝑋 ) 𝑓 = ( 𝐻 ‘ 𝑔 ) )
63 dffo3 ⊢ ( 𝐻 : ( 2 -aryF 𝑋 ) –onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ↔ ( 𝐻 : ( 2 -aryF 𝑋 ) ⟶ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ∃ 𝑔 ∈ ( 2 -aryF 𝑋 ) 𝑓 = ( 𝐻 ‘ 𝑔 ) ) )
64 2 62 63 sylanbrc ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 2 -aryF 𝑋 ) –onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )