Theorem uptri

Description: Universal property and fully faithful functor. (Contributed by Zhi Wang, 16-Nov-2025)

	Ref	Expression
Hypotheses	uptr.y	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑋 ) = 𝑌 )
	uptr.r	⊢ ( 𝜑 → 𝑅 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑆 )
	uptr.k	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
	uptri.n	⊢ ( 𝜑 → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
	uptri.z	⊢ ( 𝜑 → 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 )
Assertion	uptri	⊢ ( 𝜑 → 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		uptr.y	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑋 ) = 𝑌 )
2		uptr.r	⊢ ( 𝜑 → 𝑅 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑆 )
3		uptr.k	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
4		uptri.n	⊢ ( 𝜑 → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
5		uptri.z	⊢ ( 𝜑 → 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( 𝑅 ‘ 𝑋 ) = 𝑌 )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑅 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑆 )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10	5	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 )
11	10 9	uprcl3	⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑋 ∈ ( Base ‘ 𝐷 ) )
12	10	uprcl2	⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
13	4	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
14		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
15	10 14	uprcl5	⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑀 ∈ ( 𝑋 ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑍 ) ) )
16	6 7 8 9 11 12 13 14 15	uptr	⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
17	5 16	mpdan	⊢ ( 𝜑 → ( 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
18	5 17	mpbid	⊢ ( 𝜑 → 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 )