uptr2a

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

	Ref	Expression
Hypotheses	uptr2a.a	$⊢ A = {Base}_{C}$
	uptr2a.b	$⊢ B = {Base}_{D}$
	uptr2a.y	$⊢ φ \to Y = 1^{st} (K) (X)$
	uptr2a.f	$⊢ φ \to G \circ_{func} K = F$
	uptr2a.x	$⊢ φ \to X \in A$
	uptr2a.g	$⊢ φ \to G \in (D Func E)$
	uptr2a.k	$⊢ φ \to K \in ((C Full D) \cap (C Faith D))$
	uptr2a.1	$⊢ φ \to 1^{st} (K) : A \underset{onto}{⟶} B$
Assertion	uptr2a	Could not format assertion : No typesetting found for \|- ( ph -> ( X ( F ( C UP E ) Z ) M <-> Y ( G ( D UP E ) Z ) M ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		uptr2a.a	$⊢ A = {Base}_{C}$
2		uptr2a.b	$⊢ B = {Base}_{D}$
3		uptr2a.y	$⊢ φ \to Y = 1^{st} (K) (X)$
4		uptr2a.f	$⊢ φ \to G \circ_{func} K = F$
5		uptr2a.x	$⊢ φ \to X \in A$
6		uptr2a.g	$⊢ φ \to G \in (D Func E)$
7		uptr2a.k	$⊢ φ \to K \in ((C Full D) \cap (C Faith D))$
8		uptr2a.1	$⊢ φ \to 1^{st} (K) : A \underset{onto}{⟶} B$
9		relfull	$⊢ Rel (C Full D)$
10		relin1	$⊢ Rel (C Full D) \to Rel ((C Full D) \cap (C Faith D))$
11	9 10	ax-mp	$⊢ Rel ((C Full D) \cap (C Faith D))$
12		1st2ndbr	$⊢ (Rel ((C Full D) \cap (C Faith D)) \land K \in ((C Full D) \cap (C Faith D))) \to 1^{st} (K) ((C Full D) \cap (C Faith D)) 2^{nd} (K)$
13	11 7 12	sylancr	$⊢ φ \to 1^{st} (K) ((C Full D) \cap (C Faith D)) 2^{nd} (K)$
14		inss1	$⊢ (C Full D) \cap (C Faith D) \subseteq C Full D$
15		fullfunc	$⊢ C Full D \subseteq C Func D$
16	14 15	sstri	$⊢ (C Full D) \cap (C Faith D) \subseteq C Func D$
17	16 7	sselid	$⊢ φ \to K \in (C Func D)$
18	17 6	cofu1st2nd	$⊢ φ \to G \circ_{func} K = ⟨1^{st} (G), 2^{nd} (G)⟩ \circ_{func} ⟨1^{st} (K), 2^{nd} (K)⟩$
19		relfunc	$⊢ Rel (C Func E)$
20	17 6	cofucl	$⊢ φ \to G \circ_{func} K \in (C Func E)$
21	4 20	eqeltrrd	$⊢ φ \to F \in (C Func E)$
22		1st2nd	$⊢ (Rel (C Func E) \land F \in (C Func E)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
23	19 21 22	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
24	4 18 23	3eqtr3d	$⊢ φ \to ⟨1^{st} (G), 2^{nd} (G)⟩ \circ_{func} ⟨1^{st} (K), 2^{nd} (K)⟩ = ⟨1^{st} (F), 2^{nd} (F)⟩$
25	6	func1st2nd	$⊢ φ \to 1^{st} (G) (D Func E) 2^{nd} (G)$
26	1 2 3 8 13 24 5 25	uptr2	Could not format ( ph -> ( X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP E ) Z ) M <-> Y ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( D UP E ) Z ) M ) ) : No typesetting found for \|- ( ph -> ( X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP E ) Z ) M <-> Y ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( D UP E ) Z ) M ) ) with typecode \|-
27	21	up1st2ndb	Could not format ( ph -> ( X ( F ( C UP E ) Z ) M <-> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP E ) Z ) M ) ) : No typesetting found for \|- ( ph -> ( X ( F ( C UP E ) Z ) M <-> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP E ) Z ) M ) ) with typecode \|-
28	6	up1st2ndb	Could not format ( ph -> ( Y ( G ( D UP E ) Z ) M <-> Y ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( D UP E ) Z ) M ) ) : No typesetting found for \|- ( ph -> ( Y ( G ( D UP E ) Z ) M <-> Y ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( D UP E ) Z ) M ) ) with typecode \|-
29	26 27 28	3bitr4d	Could not format ( ph -> ( X ( F ( C UP E ) Z ) M <-> Y ( G ( D UP E ) Z ) M ) ) : No typesetting found for \|- ( ph -> ( X ( F ( C UP E ) Z ) M <-> Y ( G ( D UP E ) Z ) M ) ) with typecode \|-

Metamath Proof Explorer

Theorem uptr2a

Proof