| Step |
Hyp |
Ref |
Expression |
| 1 |
|
uptr.y |
|- ( ph -> ( R ` X ) = Y ) |
| 2 |
|
uptr.r |
|- ( ph -> R ( ( D Full E ) i^i ( D Faith E ) ) S ) |
| 3 |
|
uptr.k |
|- ( ph -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. ) |
| 4 |
|
uptri.n |
|- ( ph -> ( ( X S ( F ` Z ) ) ` M ) = N ) |
| 5 |
|
uptri.z |
|- ( ph -> Z ( <. F , G >. ( C UP D ) X ) M ) |
| 6 |
1
|
adantr |
|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( R ` X ) = Y ) |
| 7 |
2
|
adantr |
|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> R ( ( D Full E ) i^i ( D Faith E ) ) S ) |
| 8 |
3
|
adantr |
|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( <. R , S >. o.func <. F , G >. ) = <. K , L >. ) |
| 9 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
| 10 |
5
|
adantr |
|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> Z ( <. F , G >. ( C UP D ) X ) M ) |
| 11 |
10 9
|
uprcl3 |
|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> X e. ( Base ` D ) ) |
| 12 |
10
|
uprcl2 |
|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> F ( C Func D ) G ) |
| 13 |
4
|
adantr |
|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( ( X S ( F ` Z ) ) ` M ) = N ) |
| 14 |
|
eqid |
|- ( Hom ` D ) = ( Hom ` D ) |
| 15 |
10 14
|
uprcl5 |
|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> M e. ( X ( Hom ` D ) ( F ` Z ) ) ) |
| 16 |
6 7 8 9 11 12 13 14 15
|
uptr |
|- ( ( ph /\ Z ( <. F , G >. ( C UP D ) X ) M ) -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) |
| 17 |
5 16
|
mpdan |
|- ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) |
| 18 |
5 17
|
mpbid |
|- ( ph -> Z ( <. K , L >. ( C UP E ) Y ) N ) |