Step |
Hyp |
Ref |
Expression |
1 |
|
snex |
|- { 0 } e. _V |
2 |
1
|
a1i |
|- ( ( A e. S /\ B e. T ) -> { 0 } e. _V ) |
3 |
|
simpr |
|- ( ( A e. S /\ B e. T ) -> B e. T ) |
4 |
|
simpll |
|- ( ( ( A e. S /\ B e. T ) /\ i e. { 0 } ) -> A e. S ) |
5 |
|
s1val |
|- ( A e. S -> <" A "> = { <. 0 , A >. } ) |
6 |
|
0nn0 |
|- 0 e. NN0 |
7 |
|
fmptsn |
|- ( ( 0 e. NN0 /\ A e. S ) -> { <. 0 , A >. } = ( i e. { 0 } |-> A ) ) |
8 |
6 7
|
mpan |
|- ( A e. S -> { <. 0 , A >. } = ( i e. { 0 } |-> A ) ) |
9 |
5 8
|
eqtrd |
|- ( A e. S -> <" A "> = ( i e. { 0 } |-> A ) ) |
10 |
9
|
adantr |
|- ( ( A e. S /\ B e. T ) -> <" A "> = ( i e. { 0 } |-> A ) ) |
11 |
2 3 4 10
|
ofcfval2 |
|- ( ( A e. S /\ B e. T ) -> ( <" A "> oFC R B ) = ( i e. { 0 } |-> ( A R B ) ) ) |
12 |
|
ovex |
|- ( A R B ) e. _V |
13 |
|
s1val |
|- ( ( A R B ) e. _V -> <" ( A R B ) "> = { <. 0 , ( A R B ) >. } ) |
14 |
12 13
|
ax-mp |
|- <" ( A R B ) "> = { <. 0 , ( A R B ) >. } |
15 |
|
fmptsn |
|- ( ( 0 e. NN0 /\ ( A R B ) e. _V ) -> { <. 0 , ( A R B ) >. } = ( i e. { 0 } |-> ( A R B ) ) ) |
16 |
6 12 15
|
mp2an |
|- { <. 0 , ( A R B ) >. } = ( i e. { 0 } |-> ( A R B ) ) |
17 |
14 16
|
eqtri |
|- <" ( A R B ) "> = ( i e. { 0 } |-> ( A R B ) ) |
18 |
11 17
|
eqtr4di |
|- ( ( A e. S /\ B e. T ) -> ( <" A "> oFC R B ) = <" ( A R B ) "> ) |