Theorem initopropdlem

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

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

Proof

Step	Hyp	Ref	Expression
1		initopropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2		initopropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3		initopropdlem.1	⊢ ( 𝜑 → ¬ 𝐶 ∈ V )
4		initofn	⊢ InitO Fn Cat
5		ssv	⊢ Cat ⊆ V
6		simpr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → 𝐷 ∈ Cat )
7		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9	6 7 8	initoval	⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → ( InitO ‘ 𝐷 ) = { 𝑎 ∈ ( 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 ) → ( InitO ‘ 𝐷 ) = ∅ )
20	4 3 5 19	initopropdlemlem	⊢ ( 𝜑 → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )