uptr2a

Description: Universal property and fully faithful functor surjective on objects. (Contributed by Zhi Wang, 25-Nov-2025)

	Ref	Expression
Hypotheses	uptr2a.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	uptr2a.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	uptr2a.y	⊢ ( 𝜑 → 𝑌 = ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) )
	uptr2a.f	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐾 ) = 𝐹 )
	uptr2a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	uptr2a.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
	uptr2a.k	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) )
	uptr2a.1	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) : 𝐴 –onto→ 𝐵 )
Assertion	uptr2a	⊢ ( 𝜑 → ( 𝑋 ( 𝐹 ( 𝐶 UP 𝐸 ) 𝑍 ) 𝑀 ↔ 𝑌 ( 𝐺 ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ) )

Proof

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

Metamath Proof Explorer

Theorem uptr2a

Proof