Metamath Proof Explorer

Theorem uptrai

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 𝐹 ) = 𝐺 )
		uptrai.n	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
		uptrai.z	⊢ ( 𝜑 → 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 )
	Assertion	uptrai	⊢ ( 𝜑 → 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		uptra.y	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
2		uptra.k	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
3		uptra.g	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
4		uptrai.n	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
5		uptrai.z	⊢ ( 𝜑 → 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 )
11	10	up1st2nd	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑍 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 )
12	11 9	uprcl3	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑋 ∈ ( Base ‘ 𝐷 ) )
13	10	uprcl2a	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
14	4	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
15		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
16	11 15	uprcl5	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → 𝑀 ∈ ( 𝑋 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
17	6 7 8 9 12 13 14 15 16	uptra	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ) → ( 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
18	5 17	mpdan	⊢ ( 𝜑 → ( 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
19	5 18	mpbid	⊢ ( 𝜑 → 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 )