uptr2

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

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

Proof

Step	Hyp	Ref	Expression
1		uptr2.a	$⊢ A = {Base}_{C}$
2		uptr2.b	$⊢ B = {Base}_{D}$
3		uptr2.y	$⊢ φ \to Y = R (X)$
4		uptr2.r	$⊢ φ \to R : A \underset{onto}{⟶} B$
5		uptr2.s	$⊢ φ \to R ((C Full D) \cap (C Faith D)) S$
6		uptr2.f	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨R, S⟩ = ⟨F, G⟩$
7		uptr2.x	$⊢ φ \to X \in A$
8		uptr2.k	$⊢ φ \to K (D Func E) L$
9		simpr	Could not format ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> X ( <. F , G >. ( C UP E ) Z ) M ) : No typesetting found for \|- ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> X ( <. F , G >. ( C UP E ) Z ) M ) with typecode \|-
10		eqid	$⊢ {Base}_{E} = {Base}_{E}$
11	9 10	uprcl3	Could not format ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> Z e. ( Base ` E ) ) : No typesetting found for \|- ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> Z e. ( Base ` E ) ) with typecode \|-
12		eqid	$⊢ Hom (E) = Hom (E)$
13	9 12	uprcl5	Could not format ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> M e. ( Z ( Hom ` E ) ( F ` X ) ) ) : No typesetting found for \|- ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> M e. ( Z ( Hom ` E ) ( F ` X ) ) ) with typecode \|-
14	11 13	jca	Could not format ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) : No typesetting found for \|- ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) with typecode \|-
15		simpr	Could not format ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> Y ( <. K , L >. ( D UP E ) Z ) M ) : No typesetting found for \|- ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> Y ( <. K , L >. ( D UP E ) Z ) M ) with typecode \|-
16	15 10	uprcl3	Could not format ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> Z e. ( Base ` E ) ) : No typesetting found for \|- ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> Z e. ( Base ` E ) ) with typecode \|-
17	15 12	uprcl5	Could not format ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> M e. ( Z ( Hom ` E ) ( K ` Y ) ) ) : No typesetting found for \|- ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> M e. ( Z ( Hom ` E ) ( K ` Y ) ) ) with typecode \|-
18	3	fveq2d	$⊢ φ \to K (Y) = K (R (X))$
19		inss1	$⊢ (C Full D) \cap (C Faith D) \subseteq C Full D$
20		fullfunc	$⊢ C Full D \subseteq C Func D$
21	19 20	sstri	$⊢ (C Full D) \cap (C Faith D) \subseteq C Func D$
22	21	ssbri	$⊢ R ((C Full D) \cap (C Faith D)) S \to R (C Func D) S$
23	5 22	syl	$⊢ φ \to R (C Func D) S$
24	1 23 8 6 7	cofu1a	$⊢ φ \to K (R (X)) = F (X)$
25	18 24	eqtrd	$⊢ φ \to K (Y) = F (X)$
26	25	oveq2d	$⊢ φ \to Z Hom (E) K (Y) = Z Hom (E) F (X)$
27	26	adantr	Could not format ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> ( Z ( Hom ` E ) ( K ` Y ) ) = ( Z ( Hom ` E ) ( F ` X ) ) ) : No typesetting found for \|- ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> ( Z ( Hom ` E ) ( K ` Y ) ) = ( Z ( Hom ` E ) ( F ` X ) ) ) with typecode \|-
28	17 27	eleqtrd	Could not format ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> M e. ( Z ( Hom ` E ) ( F ` X ) ) ) : No typesetting found for \|- ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> M e. ( Z ( Hom ` E ) ( F ` X ) ) ) with typecode \|-
29	16 28	jca	Could not format ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) : No typesetting found for \|- ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) with typecode \|-
30	4	adantr	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to R : A \underset{onto}{⟶} B$
31		fof	$⊢ R : A \underset{onto}{⟶} B \to R : A ⟶ B$
32	30 31	syl	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to R : A ⟶ B$
33	32	ffvelcdmda	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A) \to R (x) \in B$
34		foelrn	$⊢ (R : A \underset{onto}{⟶} B \land y \in B) \to \exists x \in A y = R (x)$
35	30 34	sylan	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land y \in B) \to \exists x \in A y = R (x)$
36		simp3	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to y = R (x)$
37	36	fveq2d	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to K (y) = K (R (x))$
38		simp1l	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to φ$
39	38 23	syl	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to R (C Func D) S$
40	8	adantr	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to K (D Func E) L$
41	40	3ad2ant1	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to K (D Func E) L$
42	38 6	syl	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to ⟨K, L⟩ \circ_{func} ⟨R, S⟩ = ⟨F, G⟩$
43		simp2	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to x \in A$
44	1 39 41 42 43	cofu1a	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to K (R (x)) = F (x)$
45	37 44	eqtrd	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to K (y) = F (x)$
46	45	oveq2d	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to Z Hom (E) K (y) = Z Hom (E) F (x)$
47		eqid	$⊢ Hom (C) = Hom (C)$
48		eqid	$⊢ Hom (D) = Hom (D)$
49	38 5	syl	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to R ((C Full D) \cap (C Faith D)) S$
50	38 7	syl	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to X \in A$
51	1 47 48 49 50 43	ffthf1o	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to (X S x) : X Hom (C) x \underset{1-1 onto}{⟶} R (X) Hom (D) R (x)$
52	38 3	syl	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to Y = R (X)$
53	52 36	oveq12d	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to Y Hom (D) y = R (X) Hom (D) R (x)$
54	53	f1oeq3d	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to ((X S x) : X Hom (C) x \underset{1-1 onto}{⟶} Y Hom (D) y \leftrightarrow (X S x) : X Hom (C) x \underset{1-1 onto}{⟶} R (X) Hom (D) R (x))$
55	51 54	mpbird	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to (X S x) : X Hom (C) x \underset{1-1 onto}{⟶} Y Hom (D) y$
56		f1of	$⊢ (X S x) : X Hom (C) x \underset{1-1 onto}{⟶} Y Hom (D) y \to (X S x) : X Hom (C) x ⟶ Y Hom (D) y$
57	55 56	syl	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to (X S x) : X Hom (C) x ⟶ Y Hom (D) y$
58	57	ffvelcdmda	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land k \in (X Hom (C) x)) \to (X S x) (k) \in (Y Hom (D) y)$
59		f1ofveu	$⊢ ((X S x) : X Hom (C) x \underset{1-1 onto}{⟶} Y Hom (D) y \land l \in (Y Hom (D) y)) \to \exists! k \in (X Hom (C) x) (X S x) (k) = l$
60		eqcom	$⊢ (X S x) (k) = l \leftrightarrow l = (X S x) (k)$
61	60	reubii	$⊢ \exists! k \in (X Hom (C) x) (X S x) (k) = l \leftrightarrow \exists! k \in (X Hom (C) x) l = (X S x) (k)$
62	59 61	sylib	$⊢ ((X S x) : X Hom (C) x \underset{1-1 onto}{⟶} Y Hom (D) y \land l \in (Y Hom (D) y)) \to \exists! k \in (X Hom (C) x) l = (X S x) (k)$
63	55 62	sylan	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land l \in (Y Hom (D) y)) \to \exists! k \in (X Hom (C) x) l = (X S x) (k)$
64	38 25	syl	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to K (Y) = F (X)$
65	64	opeq2d	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to ⟨Z, K (Y)⟩ = ⟨Z, F (X)⟩$
66	65 45	oveq12d	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to ⟨Z, K (Y)⟩ comp (E) K (y) = ⟨Z, F (X)⟩ comp (E) F (x)$
67	66	adantr	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to ⟨Z, K (Y)⟩ comp (E) K (y) = ⟨Z, F (X)⟩ comp (E) F (x)$
68	52	adantr	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to Y = R (X)$
69		simpl3	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to y = R (x)$
70	68 69	oveq12d	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to Y L y = R (X) L R (x)$
71		simprr	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to l = (X S x) (k)$
72	70 71	fveq12d	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to (Y L y) (l) = (R (X) L R (x)) ((X S x) (k))$
73	39	adantr	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to R (C Func D) S$
74	41	adantr	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to K (D Func E) L$
75	42	adantr	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to ⟨K, L⟩ \circ_{func} ⟨R, S⟩ = ⟨F, G⟩$
76	50	adantr	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to X \in A$
77	43	adantr	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to x \in A$
78		simprl	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to k \in (X Hom (C) x)$
79	1 73 74 75 76 77 47 78	cofu2a	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to (R (X) L R (x)) ((X S x) (k)) = (X G x) (k)$
80	72 79	eqtrd	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to (Y L y) (l) = (X G x) (k)$
81		eqidd	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to M = M$
82	67 80 81	oveq123d	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to (Y L y) (l) (⟨Z, K (Y)⟩ comp (E) K (y)) M = (X G x) (k) (⟨Z, F (X)⟩ comp (E) F (x)) M$
83	82	eqeq2d	$⊢ (((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \land (k \in (X Hom (C) x) \land l = (X S x) (k))) \to (g = (Y L y) (l) (⟨Z, K (Y)⟩ comp (E) K (y)) M \leftrightarrow g = (X G x) (k) (⟨Z, F (X)⟩ comp (E) F (x)) M)$
84	58 63 83	reuxfr1dd	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to (\exists! l \in (Y Hom (D) y) g = (Y L y) (l) (⟨Z, K (Y)⟩ comp (E) K (y)) M \leftrightarrow \exists! k \in (X Hom (C) x) g = (X G x) (k) (⟨Z, F (X)⟩ comp (E) F (x)) M)$
85	46 84	raleqbidv	$⊢ ((φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \land x \in A \land y = R (x)) \to (\forall g \in (Z Hom (E) K (y)) \exists! l \in (Y Hom (D) y) g = (Y L y) (l) (⟨Z, K (Y)⟩ comp (E) K (y)) M \leftrightarrow \forall g \in (Z Hom (E) F (x)) \exists! k \in (X Hom (C) x) g = (X G x) (k) (⟨Z, F (X)⟩ comp (E) F (x)) M)$
86	33 35 85	ralxfrd2	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to (\forall y \in B \forall g \in (Z Hom (E) K (y)) \exists! l \in (Y Hom (D) y) g = (Y L y) (l) (⟨Z, K (Y)⟩ comp (E) K (y)) M \leftrightarrow \forall x \in A \forall g \in (Z Hom (E) F (x)) \exists! k \in (X Hom (C) x) g = (X G x) (k) (⟨Z, F (X)⟩ comp (E) F (x)) M)$
87		eqid	$⊢ comp (E) = comp (E)$
88		simprl	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to Z \in {Base}_{E}$
89	3	adantr	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to Y = R (X)$
90	7	adantr	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to X \in A$
91	32 90	ffvelcdmd	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to R (X) \in B$
92	89 91	eqeltrd	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to Y \in B$
93		simprr	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to M \in (Z Hom (E) F (X))$
94	26	adantr	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to Z Hom (E) K (Y) = Z Hom (E) F (X)$
95	93 94	eleqtrrd	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to M \in (Z Hom (E) K (Y))$
96	2 10 48 12 87 88 40 92 95	isup	Could not format ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( Y ( <. K , L >. ( D UP E ) Z ) M <-> A. y e. B A. g e. ( Z ( Hom ` E ) ( K ` y ) ) E! l e. ( Y ( Hom ` D ) y ) g = ( ( ( Y L y ) ` l ) ( <. Z , ( K ` Y ) >. ( comp ` E ) ( K ` y ) ) M ) ) ) : No typesetting found for \|- ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( Y ( <. K , L >. ( D UP E ) Z ) M <-> A. y e. B A. g e. ( Z ( Hom ` E ) ( K ` y ) ) E! l e. ( Y ( Hom ` D ) y ) g = ( ( ( Y L y ) ` l ) ( <. Z , ( K ` Y ) >. ( comp ` E ) ( K ` y ) ) M ) ) ) with typecode \|-
97	23 8	cofucla	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨R, S⟩ \in (C Func E)$
98	6 97	eqeltrrd	$⊢ φ \to ⟨F, G⟩ \in (C Func E)$
99		df-br	$⊢ F (C Func E) G \leftrightarrow ⟨F, G⟩ \in (C Func E)$
100	98 99	sylibr	$⊢ φ \to F (C Func E) G$
101	100	adantr	$⊢ (φ \land (Z \in {Base}_{E} \land M \in (Z Hom (E) F (X)))) \to F (C Func E) G$
102	1 10 47 12 87 88 101 90 93	isup	Could not format ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( X ( <. F , G >. ( C UP E ) Z ) M <-> A. x e. A A. g e. ( Z ( Hom ` E ) ( F ` x ) ) E! k e. ( X ( Hom ` C ) x ) g = ( ( ( X G x ) ` k ) ( <. Z , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) M ) ) ) : No typesetting found for \|- ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( X ( <. F , G >. ( C UP E ) Z ) M <-> A. x e. A A. g e. ( Z ( Hom ` E ) ( F ` x ) ) E! k e. ( X ( Hom ` C ) x ) g = ( ( ( X G x ) ` k ) ( <. Z , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) M ) ) ) with typecode \|-
103	86 96 102	3bitr4rd	Could not format ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( X ( <. F , G >. ( C UP E ) Z ) M <-> Y ( <. K , L >. ( D UP E ) Z ) M ) ) : No typesetting found for \|- ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( X ( <. F , G >. ( C UP E ) Z ) M <-> Y ( <. K , L >. ( D UP E ) Z ) M ) ) with typecode \|-
104	14 29 103	bibiad	Could not format ( ph -> ( X ( <. F , G >. ( C UP E ) Z ) M <-> Y ( <. K , L >. ( D UP E ) Z ) M ) ) : No typesetting found for \|- ( ph -> ( X ( <. F , G >. ( C UP E ) Z ) M <-> Y ( <. K , L >. ( D UP E ) Z ) M ) ) with typecode \|-

Metamath Proof Explorer

Theorem uptr2

Proof