This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem termopropdlem

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

Ref Expression
Hypotheses initopropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
initopropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
initopropdlem.1 ⊢ ( 𝜑 → ¬ 𝐶 ∈ V )
Assertion termopropdlem ( 𝜑 → ( TermO ‘ 𝐶 ) = ( TermO ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 initopropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2 initopropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3 initopropdlem.1 ⊢ ( 𝜑 → ¬ 𝐶 ∈ V )
4 termofn ⊢ TermO Fn Cat
5 ssv ⊢ Cat ⊆ V
6 simpr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → 𝐷 ∈ Cat )
7 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9 6 7 8 termoval ⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → ( TermO ‘ 𝐷 ) = { 𝑎 ∈ ( Base ‘ 𝐷 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑏 ( Hom ‘ 𝐷 ) 𝑎 ) } )
10 fvprc ⊢ ( ¬ 𝐶 ∈ V → ( Homf ‘ 𝐶 ) = ∅ )
11 3 10 syl ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ∅ )
12 1 11 eqtr3d ⊢ ( 𝜑 → ( Homf ‘ 𝐷 ) = ∅ )
13 homf0 ⊢ ( ( Base ‘ 𝐷 ) = ∅ ↔ ( Homf ‘ 𝐷 ) = ∅ )
14 12 13 sylibr ⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ∅ )
15 14 rabeqdv ⊢ ( 𝜑 → { 𝑎 ∈ ( Base ‘ 𝐷 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑏 ( Hom ‘ 𝐷 ) 𝑎 ) } = { 𝑎 ∈ ∅ ∣ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑏 ( Hom ‘ 𝐷 ) 𝑎 ) } )
16 rab0 ⊢ { 𝑎 ∈ ∅ ∣ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑏 ( Hom ‘ 𝐷 ) 𝑎 ) } = ∅
17 15 16 eqtrdi ⊢ ( 𝜑 → { 𝑎 ∈ ( Base ‘ 𝐷 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑏 ( Hom ‘ 𝐷 ) 𝑎 ) } = ∅ )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → { 𝑎 ∈ ( Base ‘ 𝐷 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑏 ( Hom ‘ 𝐷 ) 𝑎 ) } = ∅ )
19 9 18 eqtrd ⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → ( TermO ‘ 𝐷 ) = ∅ )
20 4 3 5 19 initopropdlemlem ⊢ ( 𝜑 → ( TermO ‘ 𝐶 ) = ( TermO ‘ 𝐷 ) )