Theorem uptr2a

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

	Ref	Expression
Hypotheses	uptr2a.a	$$⊢A={\mathrm{Base}}_C$$
	uptr2a.b	$$⊢B={\mathrm{Base}}_D$$
	uptr2a.y	$$⊢\phi \to Y=1^{st}\left(K\right)\left(X\right)$$
	uptr2a.f	$$⊢\phi \to G{\circ }_{\mathrm{func}}K=F$$
	uptr2a.x	$$⊢\phi \to X\in A$$
	uptr2a.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
	uptr2a.k	$$⊢\phi \to K\in \left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)$$
	uptr2a.1	$$⊢\phi \to 1^{st}\left(K\right):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={\mathrm{Base}}_C$$
2		uptr2a.b	$$⊢B={\mathrm{Base}}_D$$
3		uptr2a.y	$$⊢\phi \to Y=1^{st}\left(K\right)\left(X\right)$$
4		uptr2a.f	$$⊢\phi \to G{\circ }_{\mathrm{func}}K=F$$
5		uptr2a.x	$$⊢\phi \to X\in A$$
6		uptr2a.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
7		uptr2a.k	$$⊢\phi \to K\in \left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)$$
8		uptr2a.1	$$⊢\phi \to 1^{st}\left(K\right):A\underset{onto}{⟶}B$$
9		relfull	$$⊢\mathrm{Rel}\left(C\mathrm{Full}D\right)$$
10		relin1	$$⊢\mathrm{Rel}\left(C\mathrm{Full}D\right)\to \mathrm{Rel}\left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)$$
11	9 10	ax-mp	$$⊢\mathrm{Rel}\left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)$$
12		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)\wedge K\in \left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)\right)\to 1^{st}\left(K\right)\left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)2^{nd}\left(K\right)$$
13	11 7 12	sylancr	$$⊢\phi \to 1^{st}\left(K\right)\left(\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\right)2^{nd}\left(K\right)$$
14		inss1	$$⊢\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\subseteq C\mathrm{Full}D$$
15		fullfunc	$$⊢C\mathrm{Full}D\subseteq C\mathrm{Func}D$$
16	14 15	sstri	$$⊢\left(C\mathrm{Full}D\right)\cap \left(C\mathrm{Faith}D\right)\subseteq C\mathrm{Func}D$$
17	16 7	sselid	$$⊢\phi \to K\in \left(C\mathrm{Func}D\right)$$
18	17 6	cofu1st2nd	$$⊢\phi \to G{\circ }_{\mathrm{func}}K=⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
19		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}E\right)$$
20	17 6	cofucl	$$⊢\phi \to G{\circ }_{\mathrm{func}}K\in \left(C\mathrm{Func}E\right)$$
21	4 20	eqeltrrd	$$⊢\phi \to F\in \left(C\mathrm{Func}E\right)$$
22		1st2nd	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}E\right)\wedge F\in \left(C\mathrm{Func}E\right)\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
23	19 21 22	sylancr	$$⊢\phi \to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
24	4 18 23	3eqtr3d	$$⊢\phi \to ⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
25	6	func1st2nd	$$⊢\phi \to 1^{st}\left(G\right)\left(D\mathrm{Func}E\right)2^{nd}\left(G\right)$$
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 |-