Metamath Proof Explorer


Theorem fv2arycl

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

Ref Expression
Assertion fv2arycl Could not format assertion : No typesetting found for |- ( ( G e. ( 2 -aryF X ) /\ A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) with typecode |-

Proof

Step Hyp Ref Expression
1 eqid 0 ..^ 2 = 0 ..^ 2
2 1 naryrcl Could not format ( G e. ( 2 -aryF X ) -> ( 2 e. NN0 /\ X e. _V ) ) : No typesetting found for |- ( G e. ( 2 -aryF X ) -> ( 2 e. NN0 /\ X e. _V ) ) with typecode |-
3 2aryfvalel Could not format ( X e. _V -> ( G e. ( 2 -aryF X ) <-> G : ( X ^m { 0 , 1 } ) --> X ) ) : No typesetting found for |- ( X e. _V -> ( G e. ( 2 -aryF X ) <-> G : ( X ^m { 0 , 1 } ) --> X ) ) with typecode |-
4 simp2 X V G : X 0 1 X A X B X G : X 0 1 X
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 X V G : X 0 1 X A X B X 0 V 1 V 0 1
10 fprmappr X V 0 V 1 V 0 1 A X B X 0 A 1 B X 0 1
11 9 10 syld3an2 X V G : X 0 1 X A X B X 0 A 1 B X 0 1
12 4 11 ffvelrnd X V G : X 0 1 X A X B X G 0 A 1 B X
13 12 3exp X V G : X 0 1 X A X B X G 0 A 1 B X
14 3 13 sylbid Could not format ( X e. _V -> ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) ) : No typesetting found for |- ( X e. _V -> ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) ) with typecode |-
15 14 adantl Could not format ( ( 2 e. NN0 /\ X e. _V ) -> ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) ) : No typesetting found for |- ( ( 2 e. NN0 /\ X e. _V ) -> ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) ) with typecode |-
16 2 15 mpcom Could not format ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) : No typesetting found for |- ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) with typecode |-
17 16 3impib Could not format ( ( G e. ( 2 -aryF X ) /\ A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) : No typesetting found for |- ( ( G e. ( 2 -aryF X ) /\ A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) with typecode |-