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

Metamath Proof Explorer

Theorem uptra

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

Ref Expression
Hypotheses uptra.y ⊢ ( 𝜑 → ( ( 1st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
uptra.k ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
uptra.g ⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) = 𝐺 )
uptra.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
uptra.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
uptra.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
uptra.n ⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝐾 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
uptra.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
uptra.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐽 ( ( 1st ‘ 𝐹 ) ‘ 𝑍 ) ) )
Assertion uptra ( 𝜑 → ( 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )

Proof

Step Hyp Ref Expression
1 uptra.y ⊢ ( 𝜑 → ( ( 1st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
2 uptra.k ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
3 uptra.g ⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) = 𝐺 )
4 uptra.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
5 uptra.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 uptra.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
7 uptra.n ⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝐾 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
8 uptra.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
9 uptra.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐽 ( ( 1st ‘ 𝐹 ) ‘ 𝑍 ) ) )
10 relfull ⊢ Rel ( 𝐷 Full 𝐸 )
11 relin1 ⊢ ( Rel ( 𝐷 Full 𝐸 ) → Rel ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
12 10 11 ax-mp ⊢ Rel ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) )
13 1st2ndbr ⊢ ( ( Rel ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ∧ 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ) → ( 1st ‘ 𝐾 ) ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ( 2nd ‘ 𝐾 ) )
14 12 2 13 sylancr ⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ( 2nd ‘ 𝐾 ) )
15 inss1 ⊢ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ⊆ ( 𝐷 Full 𝐸 )
16 fullfunc ⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
17 15 16 sstri ⊢ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ⊆ ( 𝐷 Func 𝐸 )
18 17 2 sselid ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
19 6 18 cofu1st2nd ⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) = ( ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ ∘func ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )
20 relfunc ⊢ Rel ( 𝐶 Func 𝐸 )
21 6 18 cofucl ⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) )
22 3 21 eqeltrrd ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
23 1st2nd ⊢ ( ( Rel ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) → 𝐺 = ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ )
24 20 22 23 sylancr ⊢ ( 𝜑 → 𝐺 = ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ )
25 3 19 24 3eqtr3d ⊢ ( 𝜑 → ( ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ ∘func ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) = ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ )
26 6 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
27 1 14 25 4 5 26 7 8 9 uptr ⊢ ( 𝜑 → ( 𝑍 ( ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
28 6 up1st2ndb ⊢ ( 𝜑 → ( 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) )
29 22 up1st2ndb ⊢ ( 𝜑 → ( 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ↔ 𝑍 ( ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
30 27 28 29 3bitr4d ⊢ ( 𝜑 → ( 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )