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

Metamath Proof Explorer

Theorem uptr

Proof