Step |
Hyp |
Ref |
Expression |
1 |
|
c0ex |
|- 0 e. _V |
2 |
|
1ex |
|- 1 e. _V |
3 |
|
2ex |
|- 2 e. _V |
4 |
1 2 3
|
3pm3.2i |
|- ( 0 e. _V /\ 1 e. _V /\ 2 e. _V ) |
5 |
4
|
a1i |
|- ( ( A e. V /\ B e. V /\ C e. V ) -> ( 0 e. _V /\ 1 e. _V /\ 2 e. _V ) ) |
6 |
|
funcnvtp |
|- ( ( ( 0 e. _V /\ 1 e. _V /\ 2 e. _V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> Fun `' { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } ) |
7 |
5 6
|
sylan |
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> Fun `' { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } ) |
8 |
|
s3tpop |
|- ( ( A e. V /\ B e. V /\ C e. V ) -> <" A B C "> = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } ) |
9 |
8
|
adantr |
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> <" A B C "> = { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } ) |
10 |
9
|
cnveqd |
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> `' <" A B C "> = `' { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } ) |
11 |
10
|
funeqd |
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( Fun `' <" A B C "> <-> Fun `' { <. 0 , A >. , <. 1 , B >. , <. 2 , C >. } ) ) |
12 |
7 11
|
mpbird |
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> Fun `' <" A B C "> ) |