Theorem uptrlem3

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

	Ref	Expression
Hypotheses	uptr.y	$$⊢\phi \to R\left(X\right)=Y$$
	uptr.r	$$⊢\phi \to R\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)S$$
	uptr.k	$$⊢\phi \to ⟨R,S⟩{\circ }_{\mathrm{func}}⟨F,G⟩=⟨K,L⟩$$
	uptr.b	$$⊢B={\mathrm{Base}}_D$$
	uptr.x	$$⊢\phi \to X\in B$$
	uptr.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
	uptr.n	$$⊢\phi \to \left(XSF\left(Z\right)\right)\left(M\right)=N$$
	uptr.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	uptr.m	$$⊢\phi \to M\in \left(XJF\left(Z\right)\right)$$
	uptrlem3.a	$$⊢A={\mathrm{Base}}_C$$
	uptrlem3.z	$$⊢\phi \to Z\in A$$
Assertion	uptrlem3	Could not format assertion : No typesetting found for |- ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		uptr.y	$$⊢\phi \to R\left(X\right)=Y$$
2		uptr.r	$$⊢\phi \to R\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)S$$
3		uptr.k	$$⊢\phi \to ⟨R,S⟩{\circ }_{\mathrm{func}}⟨F,G⟩=⟨K,L⟩$$
4		uptr.b	$$⊢B={\mathrm{Base}}_D$$
5		uptr.x	$$⊢\phi \to X\in B$$
6		uptr.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
7		uptr.n	$$⊢\phi \to \left(XSF\left(Z\right)\right)\left(M\right)=N$$
8		uptr.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
9		uptr.m	$$⊢\phi \to M\in \left(XJF\left(Z\right)\right)$$
10		uptrlem3.a	$$⊢A={\mathrm{Base}}_C$$
11		uptrlem3.z	$$⊢\phi \to Z\in A$$
12		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
13		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
14		eqid	$$⊢\mathrm{comp}\left(D\right)=\mathrm{comp}\left(D\right)$$
15		eqid	$$⊢\mathrm{comp}\left(E\right)=\mathrm{comp}\left(E\right)$$
16	5 4	eleqtrdi	$$⊢\phi \to X\in {\mathrm{Base}}_D$$
17	16	adantr	$$⊢\left(\phi \wedge y\in A\right)\to X\in {\mathrm{Base}}_D$$
18	1	adantr	$$⊢\left(\phi \wedge y\in A\right)\to R\left(X\right)=Y$$
19	11 10	eleqtrdi	$$⊢\phi \to Z\in {\mathrm{Base}}_C$$
20	19	adantr	$$⊢\left(\phi \wedge y\in A\right)\to Z\in {\mathrm{Base}}_C$$
21		simpr	$$⊢\left(\phi \wedge y\in A\right)\to y\in A$$
22	21 10	eleqtrdi	$$⊢\left(\phi \wedge y\in A\right)\to y\in {\mathrm{Base}}_C$$
23	9	adantr	$$⊢\left(\phi \wedge y\in A\right)\to M\in \left(XJF\left(Z\right)\right)$$
24	7	adantr	$$⊢\left(\phi \wedge y\in A\right)\to \left(XSF\left(Z\right)\right)\left(M\right)=N$$
25	6	adantr	$$⊢\left(\phi \wedge y\in A\right)\to F\left(C\mathrm{Func}D\right)G$$
26	2	adantr	$$⊢\left(\phi \wedge y\in A\right)\to R\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)S$$
27	3	adantr	$$⊢\left(\phi \wedge y\in A\right)\to ⟨R,S⟩{\circ }_{\mathrm{func}}⟨F,G⟩=⟨K,L⟩$$
28	12 8 13 14 15 17 18 20 22 23 24 25 26 27	uptrlem1	$$⊢\left(\phi \wedge y\in A\right)\to \left(\forall h\in \left(Y\mathrm{Hom}\left(E\right)K\left(y\right)\right)\exists !k\in \left(Z\mathrm{Hom}\left(C\right)y\right)h=\left(ZLy\right)\left(k\right)\left(⟨Y,K\left(Z\right)⟩\mathrm{comp}\left(E\right)K\left(y\right)\right)N\leftrightarrow \forall g\in \left(XJF\left(y\right)\right)\exists !k\in \left(Z\mathrm{Hom}\left(C\right)y\right)g=\left(ZGy\right)\left(k\right)\left(⟨X,F\left(Z\right)⟩\mathrm{comp}\left(D\right)F\left(y\right)\right)M\right)$$
29	28	ralbidva	$$⊢\phi \to \left(\forall y\in A\forall h\in \left(Y\mathrm{Hom}\left(E\right)K\left(y\right)\right)\exists !k\in \left(Z\mathrm{Hom}\left(C\right)y\right)h=\left(ZLy\right)\left(k\right)\left(⟨Y,K\left(Z\right)⟩\mathrm{comp}\left(E\right)K\left(y\right)\right)N\leftrightarrow \forall y\in A\forall g\in \left(XJF\left(y\right)\right)\exists !k\in \left(Z\mathrm{Hom}\left(C\right)y\right)g=\left(ZGy\right)\left(k\right)\left(⟨X,F\left(Z\right)⟩\mathrm{comp}\left(D\right)F\left(y\right)\right)M\right)$$
30		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
31		inss1	$$⊢\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\subseteq D\mathrm{Full}E$$
32		fullfunc	$$⊢D\mathrm{Full}E\subseteq D\mathrm{Func}E$$
33	31 32	sstri	$$⊢\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\subseteq D\mathrm{Func}E$$
34	33	ssbri	$$⊢R\left(\left(D\mathrm{Full}E\right)\cap \left(D\mathrm{Faith}E\right)\right)S\to R\left(D\mathrm{Func}E\right)S$$
35	2 34	syl	$$⊢\phi \to R\left(D\mathrm{Func}E\right)S$$
36	4 30 35	funcf1	$$⊢\phi \to R:B⟶{\mathrm{Base}}_E$$
37	36 5	ffvelcdmd	$$⊢\phi \to R\left(X\right)\in {\mathrm{Base}}_E$$
38	1 37	eqeltrrd	$$⊢\phi \to Y\in {\mathrm{Base}}_E$$
39	6 35	cofucla	$$⊢\phi \to ⟨R,S⟩{\circ }_{\mathrm{func}}⟨F,G⟩\in \left(C\mathrm{Func}E\right)$$
40	3 39	eqeltrrd	$$⊢\phi \to ⟨K,L⟩\in \left(C\mathrm{Func}E\right)$$
41		df-br	$$⊢K\left(C\mathrm{Func}E\right)L\leftrightarrow ⟨K,L⟩\in \left(C\mathrm{Func}E\right)$$
42	40 41	sylibr	$$⊢\phi \to K\left(C\mathrm{Func}E\right)L$$
43	10 4 6	funcf1	$$⊢\phi \to F:A⟶B$$
44	43 11	ffvelcdmd	$$⊢\phi \to F\left(Z\right)\in B$$
45	4 8 13 35 5 44	funcf2	$$⊢\phi \to \left(XSF\left(Z\right)\right):XJF\left(Z\right)⟶R\left(X\right)\mathrm{Hom}\left(E\right)R\left(F\left(Z\right)\right)$$
46	45 9	ffvelcdmd	$$⊢\phi \to \left(XSF\left(Z\right)\right)\left(M\right)\in \left(R\left(X\right)\mathrm{Hom}\left(E\right)R\left(F\left(Z\right)\right)\right)$$
47	10 6 35 3 11	cofu1a	$$⊢\phi \to R\left(F\left(Z\right)\right)=K\left(Z\right)$$
48	1 47	oveq12d	$$⊢\phi \to R\left(X\right)\mathrm{Hom}\left(E\right)R\left(F\left(Z\right)\right)=Y\mathrm{Hom}\left(E\right)K\left(Z\right)$$
49	46 7 48	3eltr3d	$$⊢\phi \to N\in \left(Y\mathrm{Hom}\left(E\right)K\left(Z\right)\right)$$
50	10 30 12 13 15 38 42 11 49	isup	Could not format ( ph -> ( Z ( <. K , L >. ( C UP E ) Y ) N <-> A. y e. A A. h e. ( Y ( Hom ` E ) ( K ` y ) ) E! k e. ( Z ( Hom ` C ) y ) h = ( ( ( Z L y ) ` k ) ( <. Y , ( K ` Z ) >. ( comp ` E ) ( K ` y ) ) N ) ) ) : No typesetting found for |- ( ph -> ( Z ( <. K , L >. ( C UP E ) Y ) N <-> A. y e. A A. h e. ( Y ( Hom ` E ) ( K ` y ) ) E! k e. ( Z ( Hom ` C ) y ) h = ( ( ( Z L y ) ` k ) ( <. Y , ( K ` Z ) >. ( comp ` E ) ( K ` y ) ) N ) ) ) with typecode |-
51	10 4 12 8 14 5 6 11 9	isup	Could not format ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> A. y e. A A. g e. ( X J ( F ` y ) ) E! k e. ( Z ( Hom ` C ) y ) g = ( ( ( Z G y ) ` k ) ( <. X , ( F ` Z ) >. ( comp ` D ) ( F ` y ) ) M ) ) ) : No typesetting found for |- ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> A. y e. A A. g e. ( X J ( F ` y ) ) E! k e. ( Z ( Hom ` C ) y ) g = ( ( ( Z G y ) ` k ) ( <. X , ( F ` Z ) >. ( comp ` D ) ( F ` y ) ) M ) ) ) with typecode |-
52	29 50 51	3bitr4rd	Could not format ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) : No typesetting found for |- ( ph -> ( Z ( <. F , G >. ( C UP D ) X ) M <-> Z ( <. K , L >. ( C UP E ) Y ) N ) ) with typecode |-