Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|
2 |
1
|
naryrcl |
Could not format ( G e. ( 1 -aryF X ) -> ( 1 e. NN0 /\ X e. _V ) ) : No typesetting found for |- ( G e. ( 1 -aryF X ) -> ( 1 e. NN0 /\ X e. _V ) ) with typecode |- |
3 |
|
1aryfvalel |
Could not format ( X e. _V -> ( G e. ( 1 -aryF X ) <-> G : ( X ^m { 0 } ) --> X ) ) : No typesetting found for |- ( X e. _V -> ( G e. ( 1 -aryF X ) <-> G : ( X ^m { 0 } ) --> X ) ) with typecode |- |
4 |
|
simp2 |
|
5 |
|
c0ex |
|
6 |
5
|
a1i |
|
7 |
|
simp3 |
|
8 |
6 7
|
fsnd |
|
9 |
|
simp1 |
|
10 |
|
snex |
|
11 |
10
|
a1i |
|
12 |
9 11
|
elmapd |
|
13 |
8 12
|
mpbird |
|
14 |
4 13
|
ffvelrnd |
|
15 |
14
|
3exp |
|
16 |
3 15
|
sylbid |
Could not format ( X e. _V -> ( G e. ( 1 -aryF X ) -> ( A e. X -> ( G ` { <. 0 , A >. } ) e. X ) ) ) : No typesetting found for |- ( X e. _V -> ( G e. ( 1 -aryF X ) -> ( A e. X -> ( G ` { <. 0 , A >. } ) e. X ) ) ) with typecode |- |
17 |
16
|
adantl |
Could not format ( ( 1 e. NN0 /\ X e. _V ) -> ( G e. ( 1 -aryF X ) -> ( A e. X -> ( G ` { <. 0 , A >. } ) e. X ) ) ) : No typesetting found for |- ( ( 1 e. NN0 /\ X e. _V ) -> ( G e. ( 1 -aryF X ) -> ( A e. X -> ( G ` { <. 0 , A >. } ) e. X ) ) ) with typecode |- |
18 |
2 17
|
mpcom |
Could not format ( G e. ( 1 -aryF X ) -> ( A e. X -> ( G ` { <. 0 , A >. } ) e. X ) ) : No typesetting found for |- ( G e. ( 1 -aryF X ) -> ( A e. X -> ( G ` { <. 0 , A >. } ) e. X ) ) with typecode |- |
19 |
18
|
imp |
Could not format ( ( G e. ( 1 -aryF X ) /\ A e. X ) -> ( G ` { <. 0 , A >. } ) e. X ) : No typesetting found for |- ( ( G e. ( 1 -aryF X ) /\ A e. X ) -> ( G ` { <. 0 , A >. } ) e. X ) with typecode |- |