Theorem fv2arycl

Description: Closure of a binary (endo)function. (Contributed by AV, 20-May-2024)

	Ref	Expression
Assertion	fv2arycl	⊢ ( ( 𝐺 ∈ ( 2 -aryF 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 0 ..^ 2 ) = ( 0 ..^ 2 )
2	1	naryrcl	⊢ ( 𝐺 ∈ ( 2 -aryF 𝑋 ) → ( 2 ∈ ℕ0 ∧ 𝑋 ∈ V ) )
3		2aryfvalel	⊢ ( 𝑋 ∈ V → ( 𝐺 ∈ ( 2 -aryF 𝑋 ) ↔ 𝐺 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ) )
4		simp2	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐺 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 )
5		c0ex	⊢ 0 ∈ V
6		1ex	⊢ 1 ∈ V
7		0ne1	⊢ 0 ≠ 1
8	5 6 7	3pm3.2i	⊢ ( 0 ∈ V ∧ 1 ∈ V ∧ 0 ≠ 1 )
9	8	a1i	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 0 ∈ V ∧ 1 ∈ V ∧ 0 ≠ 1 ) )
10		fprmappr	⊢ ( ( 𝑋 ∈ V ∧ ( 0 ∈ V ∧ 1 ∈ V ∧ 0 ≠ 1 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∈ ( 𝑋 ↑m { 0 , 1 } ) )
11	9 10	syld3an2	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ∈ ( 𝑋 ↑m { 0 , 1 } ) )
12	4 11	ffvelrnd	⊢ ( ( 𝑋 ∈ V ∧ 𝐺 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) ∈ 𝑋 )
13	12	3exp	⊢ ( 𝑋 ∈ V → ( 𝐺 : ( 𝑋 ↑m { 0 , 1 } ) ⟶ 𝑋 → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) ∈ 𝑋 ) ) )
14	3 13	sylbid	⊢ ( 𝑋 ∈ V → ( 𝐺 ∈ ( 2 -aryF 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) ∈ 𝑋 ) ) )
15	14	adantl	⊢ ( ( 2 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝐺 ∈ ( 2 -aryF 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) ∈ 𝑋 ) ) )
16	2 15	mpcom	⊢ ( 𝐺 ∈ ( 2 -aryF 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) ∈ 𝑋 ) )
17	16	3impib	⊢ ( ( 𝐺 ∈ ( 2 -aryF 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐺 ‘ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) ∈ 𝑋 )