Metamath Proof Explorer

Theorem 2arymaptf1

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

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

Proof

Step Hyp Ref Expression
1 2arymaptf.h ⊢ 𝐻 = ( ℎ ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
2 1 2arymaptf ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 2 -aryF 𝑋 ) ⟶ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )
3 1 2arymaptfv ⊢ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) → ( 𝐻 ‘ 𝑓 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
4 3 ad2antrl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 2 -aryF 𝑋 ) ) ) → ( 𝐻 ‘ 𝑓 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
5 1 2arymaptfv ⊢ ( 𝑔 ∈ ( 2 -aryF 𝑋 ) → ( 𝐻 ‘ 𝑔 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
6 5 ad2antll ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 2 -aryF 𝑋 ) ) ) → ( 𝐻 ‘ 𝑔 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
7 4 6 eqeq12d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 2 -aryF 𝑋 ) ) ) → ( ( 𝐻 ‘ 𝑓 ) = ( 𝐻 ‘ 𝑔 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ) )
8 fvex ⊢ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ∈ V
9 8 rgen2w ⊢ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ∈ V
10 mpo2eqb ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ∈ V → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
11 9 10 mp1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 2 -aryF 𝑋 ) ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
12 2aryfvalel ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ↔ 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) )
13 2aryfvalel ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑔 ∈ ( 2 -aryF 𝑋 ) ↔ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) )
14 12 13 anbi12d ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 2 -aryF 𝑋 ) ) ↔ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ) )
15 ffn ⊢ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 → 𝑓 Fn ( 𝑋 ↑m { 0 , 1 } ) )
16 15 adantr ⊢ ( ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) → 𝑓 Fn ( 𝑋 ↑m { 0 , 1 } ) )
17 16 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → 𝑓 Fn ( 𝑋 ↑m { 0 , 1 } ) )
18 ffn ⊢ ( 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 → 𝑔 Fn ( 𝑋 ↑m { 0 , 1 } ) )
19 18 adantl ⊢ ( ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) → 𝑔 Fn ( 𝑋 ↑m { 0 , 1 } ) )
20 19 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → 𝑔 Fn ( 𝑋 ↑m { 0 , 1 } ) )
21 elmapi ⊢ ( 𝑧 ∈ ( 𝑋 ↑m { 0 , 1 } ) → 𝑧 : { 0 , 1 } ⟶ 𝑋 )
22 0ne1 ⊢ 0 ≠ 1
23 c0ex ⊢ 0 ∈ V
24 1ex ⊢ 1 ∈ V
25 23 24 fprb ⊢ ( 0 ≠ 1 → ( 𝑧 : { 0 , 1 } ⟶ 𝑋 ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) )
26 22 25 ax-mp ⊢ ( 𝑧 : { 0 , 1 } ⟶ 𝑋 ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } )
27 21 26 sylib ⊢ ( 𝑧 ∈ ( 𝑋 ↑m { 0 , 1 } ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } )
28 opeq2 ⊢ ( 𝑥 = 𝑎 → ⟨ 0 , 𝑥 ⟩ = ⟨ 0 , 𝑎 ⟩ )
29 28 preq1d ⊢ ( 𝑥 = 𝑎 → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑦 ⟩ } )
30 29 fveq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) )
31 29 fveq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) )
32 30 31 eqeq12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ↔ ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
33 opeq2 ⊢ ( 𝑦 = 𝑏 → ⟨ 1 , 𝑦 ⟩ = ⟨ 1 , 𝑏 ⟩ )
34 33 preq2d ⊢ ( 𝑦 = 𝑏 → { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑦 ⟩ } = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } )
35 34 fveq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) )
36 34 fveq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) )
37 35 36 eqeq12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ↔ ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) ) )
38 32 37 rspc2va ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) )
39 38 expcom ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) ) )
40 39 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) ) )
41 40 com12 ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) ) )
42 41 adantr ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) ) )
43 fveq2 ⊢ ( 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) )
44 fveq2 ⊢ ( 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } → ( 𝑔 ‘ 𝑧 ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) )
45 43 44 eqeq12d ⊢ ( 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } → ( ( 𝑓 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) ↔ ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) ) )
46 45 adantl ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) → ( ( 𝑓 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) ↔ ( 𝑓 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) ) )
47 42 46 sylibrd ⊢ ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } ) → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) ) )
48 47 ex ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) ) ) )
49 48 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 𝑧 = { ⟨ 0 , 𝑎 ⟩ , ⟨ 1 , 𝑏 ⟩ } → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) ) )
50 27 49 syl ⊢ ( 𝑧 ∈ ( 𝑋 ↑m { 0 , 1 } ) → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) ) )
51 50 impcom ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ∧ 𝑧 ∈ ( 𝑋 ↑m { 0 , 1 } ) ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑧 ) )
52 17 20 51 eqfnfvd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → 𝑓 = 𝑔 )
53 52 3exp ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑓 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) → 𝑓 = 𝑔 ) ) )
54 14 53 sylbid ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 2 -aryF 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) → 𝑓 = 𝑔 ) ) )
55 54 imp ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 2 -aryF 𝑋 ) ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) = ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) → 𝑓 = 𝑔 ) )
56 11 55 sylbid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 2 -aryF 𝑋 ) ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑔 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) → 𝑓 = 𝑔 ) )
57 7 56 sylbid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 2 -aryF 𝑋 ) ) ) → ( ( 𝐻 ‘ 𝑓 ) = ( 𝐻 ‘ 𝑔 ) → 𝑓 = 𝑔 ) )
58 57 ralrimivva ⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑓 ∈ ( 2 -aryF 𝑋 ) ∀ 𝑔 ∈ ( 2 -aryF 𝑋 ) ( ( 𝐻 ‘ 𝑓 ) = ( 𝐻 ‘ 𝑔 ) → 𝑓 = 𝑔 ) )
59 dff13 ⊢ ( 𝐻 : ( 2 -aryF 𝑋 ) –1-1→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ↔ ( 𝐻 : ( 2 -aryF 𝑋 ) ⟶ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( 2 -aryF 𝑋 ) ∀ 𝑔 ∈ ( 2 -aryF 𝑋 ) ( ( 𝐻 ‘ 𝑓 ) = ( 𝐻 ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) )
60 2 58 59 sylanbrc ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 2 -aryF 𝑋 ) –1-1→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )