isuplem

Description: Lemma for isup and other theorems. (Contributed by Zhi Wang, 25-Sep-2025)

	Ref	Expression
Hypotheses	upfval.b	$⊢ B = {Base}_{D}$
	upfval.c	$⊢ C = {Base}_{E}$
	upfval.h	$⊢ H = Hom (D)$
	upfval.j	$⊢ J = Hom (E)$
	upfval.o	$⊢ O = comp (E)$
	upfval2.w	$⊢ φ \to W \in C$
	upfval3.f	$⊢ φ \to F (D Func E) G$
Assertion	isuplem	Could not format assertion : No typesetting found for \|- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		upfval.b	$⊢ B = {Base}_{D}$
2		upfval.c	$⊢ C = {Base}_{E}$
3		upfval.h	$⊢ H = Hom (D)$
4		upfval.j	$⊢ J = Hom (E)$
5		upfval.o	$⊢ O = comp (E)$
6		upfval2.w	$⊢ φ \to W \in C$
7		upfval3.f	$⊢ φ \to F (D Func E) G$
8	1 2 3 4 5 6 7	upfval3	Could not format ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. \| ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) } ) : No typesetting found for \|- ( ph -> ( <. F , G >. ( D UP E ) W ) = { <. x , m >. \| ( ( x e. B /\ m e. ( W J ( F ` x ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( x H y ) g = ( ( ( x G y ) ` k ) ( <. W , ( F ` x ) >. O ( F ` y ) ) m ) ) } ) with typecode \|-
9		oveq1	$⊢ x = X \to x H y = X H y$
10		fveq2	$⊢ x = X \to F (x) = F (X)$
11	10	opeq2d	$⊢ x = X \to ⟨W, F (x)⟩ = ⟨W, F (X)⟩$
12	11	oveq1d	$⊢ x = X \to ⟨W, F (x)⟩ O F (y) = ⟨W, F (X)⟩ O F (y)$
13		oveq1	$⊢ x = X \to x G y = X G y$
14	13	fveq1d	$⊢ x = X \to (x G y) (k) = (X G y) (k)$
15		eqidd	$⊢ x = X \to m = m$
16	12 14 15	oveq123d	$⊢ x = X \to (x G y) (k) (⟨W, F (x)⟩ O F (y)) m = (X G y) (k) (⟨W, F (X)⟩ O F (y)) m$
17	16	eqeq2d	$⊢ x = X \to (g = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m \leftrightarrow g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) m)$
18	9 17	reueqbidv	$⊢ x = X \to (\exists! k \in (x H y) g = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m \leftrightarrow \exists! k \in (X H y) g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) m)$
19	18	2ralbidv	$⊢ x = X \to (\forall y \in B \forall g \in (W J F (y)) \exists! k \in (x H y) g = (x G y) (k) (⟨W, F (x)⟩ O F (y)) m \leftrightarrow \forall y \in B \forall g \in (W J F (y)) \exists! k \in (X H y) g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) m)$
20		oveq2	$⊢ m = M \to (X G y) (k) (⟨W, F (X)⟩ O F (y)) m = (X G y) (k) (⟨W, F (X)⟩ O F (y)) M$
21	20	eqeq2d	$⊢ m = M \to (g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) m \leftrightarrow g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) M)$
22	21	reubidv	$⊢ m = M \to (\exists! k \in (X H y) g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) m \leftrightarrow \exists! k \in (X H y) g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) M)$
23	22	2ralbidv	$⊢ m = M \to (\forall y \in B \forall g \in (W J F (y)) \exists! k \in (X H y) g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) m \leftrightarrow \forall y \in B \forall g \in (W J F (y)) \exists! k \in (X H y) g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) M)$
24		eqidd	$⊢ (x = X \land m = M) \to B = B$
25		simpl	$⊢ (x = X \land m = M) \to x = X$
26	25	fveq2d	$⊢ (x = X \land m = M) \to F (x) = F (X)$
27	26	oveq2d	$⊢ (x = X \land m = M) \to W J F (x) = W J F (X)$
28	8 19 23 24 27	brab2ddw	Could not format ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) ) : No typesetting found for \|- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W J ( F ` X ) ) ) /\ A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem isuplem

Proof