Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|
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 |
|
5 |
|
c0ex |
|
6 |
|
1ex |
|
7 |
|
0ne1 |
|
8 |
5 6 7
|
3pm3.2i |
|
9 |
8
|
a1i |
|
10 |
|
fprmappr |
|
11 |
9 10
|
syld3an2 |
|
12 |
4 11
|
ffvelrnd |
|
13 |
12
|
3exp |
|
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 |- |