uptra

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

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

Proof

Step	Hyp	Ref	Expression
1		uptra.y	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
2		uptra.k	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
3		uptra.g	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
4		uptra.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
5		uptra.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		uptra.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
7		uptra.n	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
8		uptra.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
9		uptra.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
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 𝐸 ) ) ) → ( 1^st ‘ 𝐾 ) ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ( 2^nd ‘ 𝐾 ) )
14	12 2 13	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ( 2^nd ‘ 𝐾 ) )
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 𝐹 ) = ( ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ∘_func ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
20		relfunc	⊢ Rel ( 𝐶 Func 𝐸 )
21	6 18	cofucl	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) )
22	3 21	eqeltrrd	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
23		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
24	20 22 23	sylancr	⊢ ( 𝜑 → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
25	3 19 24	3eqtr3d	⊢ ( 𝜑 → ( ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ∘_func ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
26	6	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
27	1 14 25 4 5 26 7 8 9	uptr	⊢ ( 𝜑 → ( 𝑍 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
28	6	up1st2ndb	⊢ ( 𝜑 → ( 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) )
29	22	up1st2ndb	⊢ ( 𝜑 → ( 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ↔ 𝑍 ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
30	27 28 29	3bitr4d	⊢ ( 𝜑 → ( 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )

Metamath Proof Explorer

Theorem uptra

Proof