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

Metamath Proof Explorer

Theorem uptr

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 ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
uptr.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
uptr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
uptr.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
uptr.n ⊢ ( 𝜑 → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
uptr.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
uptr.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐽 ( 𝐹 ‘ 𝑍 ) ) )
Assertion uptr ( 𝜑 → ( 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )

Proof

Step Hyp Ref Expression
1 uptr.y ⊢ ( 𝜑 → ( 𝑅 ‘ 𝑋 ) = 𝑌 )
2 uptr.r ⊢ ( 𝜑 → 𝑅 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑆 )
3 uptr.k ⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
4 uptr.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
5 uptr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 uptr.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
7 uptr.n ⊢ ( 𝜑 → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
8 uptr.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
9 uptr.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐽 ( 𝐹 ‘ 𝑍 ) ) )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 )
12 1 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( 𝑅 ‘ 𝑋 ) = 𝑌 )
13 2 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑅 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑆 )
14 3 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
15 5 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑋 ∈ 𝐵 )
16 6 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
17 7 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
18 9 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑀 ∈ ( 𝑋 𝐽 ( 𝐹 ‘ 𝑍 ) ) )
19 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
20 11 19 uprcl4 ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑍 ∈ ( Base ‘ 𝐶 ) )
21 12 13 14 4 15 16 17 8 18 19 20 uptrlem3 ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
22 11 21 mpbird ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 )
23 1 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( 𝑅 ‘ 𝑋 ) = 𝑌 )
24 2 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑅 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑆 )
25 3 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
26 5 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑋 ∈ 𝐵 )
27 6 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
28 7 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
29 9 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑀 ∈ ( 𝑋 𝐽 ( 𝐹 ‘ 𝑍 ) ) )
30 10 19 uprcl4 ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑍 ∈ ( Base ‘ 𝐶 ) )
31 23 24 25 4 26 27 28 8 29 19 30 uptrlem3 ⊢ ( ( 𝜑 ∧ 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
32 10 22 31 bibiad ⊢ ( 𝜑 → ( 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )