| Step |
Hyp |
Ref |
Expression |
| 1 |
|
termcnatval.c |
|- ( ph -> C e. TermCat ) |
| 2 |
|
termcnatval.n |
|- N = ( C Nat D ) |
| 3 |
|
termcnatval.a |
|- ( ph -> A e. ( F N G ) ) |
| 4 |
|
termcnatval.b |
|- B = ( Base ` C ) |
| 5 |
|
termcnatval.x |
|- ( ph -> X e. B ) |
| 6 |
|
termcnatval.r |
|- R = ( A ` X ) |
| 7 |
2 3
|
nat1st2nd |
|- ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) ) |
| 8 |
2 7 4
|
natfn |
|- ( ph -> A Fn B ) |
| 9 |
1 4 5
|
termcbas2 |
|- ( ph -> B = { X } ) |
| 10 |
9
|
fneq2d |
|- ( ph -> ( A Fn B <-> A Fn { X } ) ) |
| 11 |
8 10
|
mpbid |
|- ( ph -> A Fn { X } ) |
| 12 |
|
fnsnbg |
|- ( X e. B -> ( A Fn { X } <-> A = { <. X , ( A ` X ) >. } ) ) |
| 13 |
5 12
|
syl |
|- ( ph -> ( A Fn { X } <-> A = { <. X , ( A ` X ) >. } ) ) |
| 14 |
11 13
|
mpbid |
|- ( ph -> A = { <. X , ( A ` X ) >. } ) |
| 15 |
6
|
opeq2i |
|- <. X , R >. = <. X , ( A ` X ) >. |
| 16 |
15
|
sneqi |
|- { <. X , R >. } = { <. X , ( A ` X ) >. } |
| 17 |
14 16
|
eqtr4di |
|- ( ph -> A = { <. X , R >. } ) |