Metamath Proof Explorer

Theorem termopropdlem

Description: Lemma for termopropd . (Contributed by Zhi Wang, 26-Oct-2025)

Ref Expression
Hypotheses initopropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
initopropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
initopropdlem.1 
|- ( ph -> -. C e. _V )
Assertion termopropdlem 
|- ( ph -> ( TermO ` C ) = ( TermO ` D ) )

Proof

Step Hyp Ref Expression
1 initopropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 initopropd.2 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 initopropdlem.1 
 |-  ( ph -> -. C e. _V )
4 termofn 
 |-  TermO Fn Cat
5 ssv 
 |-  Cat C_ _V
6 simpr 
 |-  ( ( ph /\ D e. Cat ) -> D e. Cat )
7 eqid 
 |-  ( Base ` D ) = ( Base ` D )
8 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
9 6 7 8 termoval 
 |-  ( ( ph /\ D e. Cat ) -> ( TermO ` D ) = { a e. ( Base ` D ) | A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) } )
10 fvprc 
 |-  ( -. C e. _V -> ( Homf ` C ) = (/) )
11 3 10 syl 
 |-  ( ph -> ( Homf ` C ) = (/) )
12 1 11 eqtr3d 
 |-  ( ph -> ( Homf ` D ) = (/) )
13 homf0 
 |-  ( ( Base ` D ) = (/) <-> ( Homf ` D ) = (/) )
14 12 13 sylibr 
 |-  ( ph -> ( Base ` D ) = (/) )
15 14 rabeqdv 
 |-  ( ph -> { a e. ( Base ` D ) | A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) } = { a e. (/) | A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) } )
16 rab0 
 |-  { a e. (/) | A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) } = (/)
17 15 16 eqtrdi 
 |-  ( ph -> { a e. ( Base ` D ) | A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) } = (/) )
18 17 adantr 
 |-  ( ( ph /\ D e. Cat ) -> { a e. ( Base ` D ) | A. b e. ( Base ` D ) E! h h e. ( b ( Hom ` D ) a ) } = (/) )
19 9 18 eqtrd 
 |-  ( ( ph /\ D e. Cat ) -> ( TermO ` D ) = (/) )
20 4 3 5 19 initopropdlemlem 
 |-  ( ph -> ( TermO ` C ) = ( TermO ` D ) )