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

Metamath Proof Explorer

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 𝐸 ) 𝑌 ) 𝑁 )