uptrar

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

	Ref	Expression
Hypotheses	uptra.y	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
	uptra.k	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
	uptra.g	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
	uptra.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	uptra.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	uptra.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	uptrar.m	⊢ ( 𝜑 → ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑁 ) = 𝑀 )
	uptrar.z	⊢ ( 𝜑 → 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 )
Assertion	uptrar	⊢ ( 𝜑 → 𝑍 ( 𝐹 ( 𝐶 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		uptrar.m	⊢ ( 𝜑 → ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑁 ) = 𝑀 )
8		uptrar.z	⊢ ( 𝜑 → 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
11	3	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
12	5	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑋 ∈ 𝐵 )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
14	7	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑁 ) = 𝑀 )
15	14	fveq2d	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑁 ) ) = ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑀 ) )
16		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
17		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
18		relfull	⊢ Rel ( 𝐷 Full 𝐸 )
19		relin1	⊢ ( Rel ( 𝐷 Full 𝐸 ) → Rel ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
20	18 19	ax-mp	⊢ Rel ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) )
21		1st2ndbr	⊢ ( ( Rel ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ∧ 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ) → ( 1^st ‘ 𝐾 ) ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ( 2^nd ‘ 𝐾 ) )
22	20 2 21	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ( 2^nd ‘ 𝐾 ) )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( 1^st ‘ 𝐾 ) ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ( 2^nd ‘ 𝐾 ) )
24		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
25	13	func1st2nd	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
26	24 4 25	funcf1	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ 𝐵 )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 )
28	27	up1st2nd	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑍 ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 )
29	28 24	uprcl4	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑍 ∈ ( Base ‘ 𝐶 ) )
30	26 29	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ∈ 𝐵 )
31	4 16 17 23 12 30	ffthf1o	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) : ( 𝑋 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) –1-1-onto→ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ) )
32		inss1	⊢ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ⊆ ( 𝐷 Full 𝐸 )
33		fullfunc	⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
34	32 33	sstri	⊢ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ⊆ ( 𝐷 Func 𝐸 )
35	34 2	sselid	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
37	24 13 36 29	cofu1	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( 1^st ‘ ( 𝐾 ∘_func 𝐹 ) ) ‘ 𝑍 ) = ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
38	11	fveq2d	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( 1^st ‘ ( 𝐾 ∘_func 𝐹 ) ) = ( 1^st ‘ 𝐺 ) )
39	38	fveq1d	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( 1^st ‘ ( 𝐾 ∘_func 𝐹 ) ) ‘ 𝑍 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) )
40	37 39	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) )
41	9 40	oveq12d	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ) = ( 𝑌 ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) )
42	41	f1oeq3d	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) : ( 𝑋 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) –1-1-onto→ ( ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ) ↔ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) : ( 𝑋 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) –1-1-onto→ ( 𝑌 ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ) )
43	31 42	mpbid	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) : ( 𝑋 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) –1-1-onto→ ( 𝑌 ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) )
44	28 17	uprcl5	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑁 ∈ ( 𝑌 ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) )
45		f1ocnvfv2	⊢ ( ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) : ( 𝑋 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) –1-1-onto→ ( 𝑌 ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ∧ 𝑁 ∈ ( 𝑌 ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑁 ) ) = 𝑁 )
46	43 44 45	syl2anc	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑁 ) ) = 𝑁 )
47	15 46	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
48		f1ocnvdm	⊢ ( ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) : ( 𝑋 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) –1-1-onto→ ( 𝑌 ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ∧ 𝑁 ∈ ( 𝑌 ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ) → ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑁 ) ∈ ( 𝑋 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
49	43 44 48	syl2anc	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) ‘ 𝑁 ) ∈ ( 𝑋 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
50	14 49	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → 𝑀 ∈ ( 𝑋 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑍 ) ) )
51	9 10 11 4 12 13 47 16 50	uptra	⊢ ( ( 𝜑 ∧ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) → ( 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
52	8 51	mpdan	⊢ ( 𝜑 → ( 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )
53	8 52	mpbird	⊢ ( 𝜑 → 𝑍 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 )

Metamath Proof Explorer

Theorem uptrar

Proof