Theorem 2arympt

Description: A binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024)

	Ref	Expression
Hypothesis	2arympt.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑥 ‘ 0 ) 𝑂 ( 𝑥 ‘ 1 ) ) )
Assertion	2arympt	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑂 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → 𝐹 ∈ ( 2 -aryF 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		2arympt.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) ↦ ( ( 𝑥 ‘ 0 ) 𝑂 ( 𝑥 ‘ 1 ) ) )
2		simplr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑂 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) ) → 𝑂 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
3		elmapi	⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) → 𝑥 : { 0 , 1 } ⟶ 𝑋 )
4		c0ex	⊢ 0 ∈ V
5	4	prid1	⊢ 0 ∈ { 0 , 1 }
6	5	a1i	⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) → 0 ∈ { 0 , 1 } )
7	3 6	ffvelrnd	⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) → ( 𝑥 ‘ 0 ) ∈ 𝑋 )
8	7	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑂 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) ) → ( 𝑥 ‘ 0 ) ∈ 𝑋 )
9		1ex	⊢ 1 ∈ V
10	9	prid2	⊢ 1 ∈ { 0 , 1 }
11	10	a1i	⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) → 1 ∈ { 0 , 1 } )
12	3 11	ffvelrnd	⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) → ( 𝑥 ‘ 1 ) ∈ 𝑋 )
13	12	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑂 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) ) → ( 𝑥 ‘ 1 ) ∈ 𝑋 )
14	2 8 13	fovrnd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑂 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ 𝑥 ∈ ( 𝑋 ↑m { 0 , 1 } ) ) → ( ( 𝑥 ‘ 0 ) 𝑂 ( 𝑥 ‘ 1 ) ) ∈ 𝑋 )
15	14 1	fmptd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑂 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → 𝐹 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 )
16		2aryfvalel	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 ∈ ( 2 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) )
17	16	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑂 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → ( 𝐹 ∈ ( 2 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) )
18	15 17	mpbird	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑂 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → 𝐹 ∈ ( 2 -aryF 𝑋 ) )