Theorem 2arymaptf

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

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

Proof

Step	Hyp	Ref	Expression
1		2arymaptf.h	⊢ 𝐻 = ( ℎ ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
2		simplr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ℎ ∈ ( 2 -aryF 𝑋 ) ) ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ℎ ∈ ( 2 -aryF 𝑋 ) )
3		xp1st	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → ( 1st ‘ 𝑧 ) ∈ 𝑋 )
4	3	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ℎ ∈ ( 2 -aryF 𝑋 ) ) ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( 1st ‘ 𝑧 ) ∈ 𝑋 )
5		xp2nd	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑋 ) → ( 2nd ‘ 𝑧 ) ∈ 𝑋 )
6	5	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ℎ ∈ ( 2 -aryF 𝑋 ) ) ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( 2nd ‘ 𝑧 ) ∈ 𝑋 )
7		fv2arycl	⊢ ( ( ℎ ∈ ( 2 -aryF 𝑋 ) ∧ ( 1st ‘ 𝑧 ) ∈ 𝑋 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝑋 ) → ( ℎ ‘ { ⟨ 0 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑧 ) ⟩ } ) ∈ 𝑋 )
8	2 4 6 7	syl3anc	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ℎ ∈ ( 2 -aryF 𝑋 ) ) ∧ 𝑧 ∈ ( 𝑋 × 𝑋 ) ) → ( ℎ ‘ { ⟨ 0 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑧 ) ⟩ } ) ∈ 𝑋 )
9		vex	⊢ 𝑥 ∈ V
10		vex	⊢ 𝑦 ∈ V
11	9 10	op1std	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝑧 ) = 𝑥 )
12	11	opeq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 0 , ( 1st ‘ 𝑧 ) ⟩ = ⟨ 0 , 𝑥 ⟩ )
13	9 10	op2ndd	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑦 )
14	13	opeq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 1 , ( 2nd ‘ 𝑧 ) ⟩ = ⟨ 1 , 𝑦 ⟩ )
15	12 14	preq12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → { ⟨ 0 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑧 ) ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } )
16	15	fveq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ℎ ‘ { ⟨ 0 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑧 ) ⟩ } ) = ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) )
17	16	mpompt	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑋 ) ↦ ( ℎ ‘ { ⟨ 0 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑧 ) ⟩ } ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) )
18	17	eqcomi	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑋 ) ↦ ( ℎ ‘ { ⟨ 0 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑧 ) ⟩ } ) )
19	8 18	fmptd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ℎ ∈ ( 2 -aryF 𝑋 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
20		sqxpexg	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 × 𝑋 ) ∈ V )
21		elmapg	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑋 × 𝑋 ) ∈ V ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
22	20 21	mpdan	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
23	22	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ℎ ∈ ( 2 -aryF 𝑋 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
24	19 23	mpbird	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ℎ ∈ ( 2 -aryF 𝑋 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ∈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )
25	24 1	fmptd	⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 2 -aryF 𝑋 ) ⟶ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )