Theorem uptrlem2

Description: Lemma for uptr . (Contributed by Zhi Wang, 16-Nov-2025)

	Ref	Expression
Hypotheses	uptrlem1.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	uptrlem1.i	$$⊢I=\mathrm{Hom}\left(D\right)$$
	uptrlem1.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
	uptrlem1.d	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(D\right)$$
	uptrlem1.e	No typesetting found for |- .o. = ( comp ` E ) with typecode |-
	uptrlem2.a	$$⊢A={\mathrm{Base}}_C$$
	uptrlem2.b	$$⊢B={\mathrm{Base}}_D$$
	uptrlem2.x	$$⊢\phi \to X\in B$$
	uptrlem2.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
	uptrlem2.z	$$⊢\phi \to Z\in A$$
	uptrlem2.w	$$⊢\phi \to W\in A$$
	uptrlem2.m	$$⊢\phi \to M\in \left(XI{1}^{st}\left(F\right)\left(Z\right)\right)$$
	uptrlem2.n	$$⊢\phi \to \left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)\left(M\right)=N$$
	uptrlem2.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	uptrlem2.k	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
	uptrlem2.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
Assertion	uptrlem2	Could not format assertion : No typesetting found for |- ( ph -> ( A. h e. ( Y J ( ( 1st ` G ) ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z ( 2nd ` G ) W ) ` k ) ( <. Y , ( ( 1st ` G ) ` Z ) >. .o. ( ( 1st ` G ) ` W ) ) N ) <-> A. g e. ( X I ( ( 1st ` F ) ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z ( 2nd ` F ) W ) ` k ) ( <. X , ( ( 1st ` F ) ` Z ) >. .xb ( ( 1st ` F ) ` W ) ) M ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		uptrlem1.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
2		uptrlem1.i	$$⊢I=\mathrm{Hom}\left(D\right)$$
3		uptrlem1.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
4		uptrlem1.d	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(D\right)$$
5		uptrlem1.e	Could not format .o. = ( comp ` E ) : No typesetting found for |- .o. = ( comp ` E ) with typecode |-
6		uptrlem2.a	$$⊢A={\mathrm{Base}}_C$$
7		uptrlem2.b	$$⊢B={\mathrm{Base}}_D$$
8		uptrlem2.x	$$⊢\phi \to X\in B$$
9		uptrlem2.y	$$⊢\phi \to 1^{st}\left(K\right)\left(X\right)=Y$$
10		uptrlem2.z	$$⊢\phi \to Z\in A$$
11		uptrlem2.w	$$⊢\phi \to W\in A$$
12		uptrlem2.m	$$⊢\phi \to M\in \left(XI{1}^{st}\left(F\right)\left(Z\right)\right)$$
13		uptrlem2.n	$$⊢\phi \to \left(X{2}^{nd}\left(K\right)1^{st}\left(F\right)\left(Z\right)\right)\left(M\right)=N$$
14		uptrlem2.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
15		uptrlem2.k	$$⊢\phi \to K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
16		uptrlem2.g	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=G$$
17	8 7	eleqtrdi	$$⊢\phi \to X\in {\mathrm{Base}}_D$$
18	10 6	eleqtrdi	$$⊢\phi \to Z\in {\mathrm{Base}}_C$$
19	11 6	eleqtrdi	$$⊢\phi \to W\in {\mathrm{Base}}_C$$
20	14	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
21		relfull	$$⊢\mathrm{Rel}\left(D\mathrm{Full}E\right)$$
22		relin1	$$⊢\mathrm{Rel}\left(D\mathrm{Full}E\right)\to \mathrm{Rel}\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
23	21 22	ax-mp	$$⊢\mathrm{Rel}\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
24		1st2nd	$$⊢\left(\mathrm{Rel}\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)\wedge K\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)\right)\to K=⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
25	23 15 24	sylancr	$$⊢\phi \to K=⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩$$
26	25 15	eqeltrrd	$$⊢\phi \to ⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
27		df-br	$$⊢1^{st}\left(K\right)\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)2^{nd}\left(K\right)\leftrightarrow ⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩\in \left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)$$
28	26 27	sylibr	$$⊢\phi \to 1^{st}\left(K\right)\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)2^{nd}\left(K\right)$$
29		inss1	$$⊢\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\subseteq D\mathrm{Full}E$$
30		fullfunc	$$⊢D\mathrm{Full}E\subseteq D\mathrm{Func}E$$
31	29 30	sstri	$$⊢\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\subseteq D\mathrm{Func}E$$
32	31 15	sselid	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$
33	14 32	cofu1st2nd	$$⊢\phi \to K{\circ }_{\mathrm{func}}F=⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
34		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}E\right)$$
35	14 32	cofucl	$$⊢\phi \to K{\circ }_{\mathrm{func}}F\in \left(C\mathrm{Func}E\right)$$
36	16 35	eqeltrrd	$$⊢\phi \to G\in \left(C\mathrm{Func}E\right)$$
37		1st2nd	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}E\right)\wedge G\in \left(C\mathrm{Func}E\right)\right)\to G=⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩$$
38	34 36 37	sylancr	$$⊢\phi \to G=⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩$$
39	16 33 38	3eqtr3d	$$⊢\phi \to ⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩=⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩$$
40	1 2 3 4 5 17 9 18 19 12 13 20 28 39	uptrlem1	Could not format ( ph -> ( A. h e. ( Y J ( ( 1st ` G ) ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z ( 2nd ` G ) W ) ` k ) ( <. Y , ( ( 1st ` G ) ` Z ) >. .o. ( ( 1st ` G ) ` W ) ) N ) <-> A. g e. ( X I ( ( 1st ` F ) ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z ( 2nd ` F ) W ) ` k ) ( <. X , ( ( 1st ` F ) ` Z ) >. .xb ( ( 1st ` F ) ` W ) ) M ) ) ) : No typesetting found for |- ( ph -> ( A. h e. ( Y J ( ( 1st ` G ) ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z ( 2nd ` G ) W ) ` k ) ( <. Y , ( ( 1st ` G ) ` Z ) >. .o. ( ( 1st ` G ) ` W ) ) N ) <-> A. g e. ( X I ( ( 1st ` F ) ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z ( 2nd ` F ) W ) ` k ) ( <. X , ( ( 1st ` F ) ` Z ) >. .xb ( ( 1st ` F ) ` W ) ) M ) ) ) with typecode |-