mgcoval

Description: Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024)

	Ref	Expression
Hypotheses	mgcoval.1	$⊢ A = {Base}_{V}$
	mgcoval.2	$⊢ B = {Base}_{W}$
	mgcoval.3	$⊢ \underset{˙}{\leq} = \leq_{V}$
	mgcoval.4	No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
Assertion	mgcoval	Could not format assertion : No typesetting found for \|- ( ( V e. X /\ W e. Y ) -> ( V MGalConn W ) = { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		mgcoval.1	$⊢ A = {Base}_{V}$
2		mgcoval.2	$⊢ B = {Base}_{W}$
3		mgcoval.3	$⊢ \underset{˙}{\leq} = \leq_{V}$
4		mgcoval.4	Could not format .c_ = ( le ` W ) : No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
5		df-mgc	$⊢ MGalConn = (v \in V, w \in V ⟼ ⦋ {Base}_{v} / a ⦌ ⦋ {Base}_{w} / b ⦌ \{⟨f, g⟩ \| ((f \in (b^{a}) \land g \in (a^{b})) \land \forall x \in a \forall y \in b (f (x) \leq_{w} y \leftrightarrow x \leq_{v} g (y)))\})$
6	5	a1i	$⊢ (V \in X \land W \in Y) \to MGalConn = (v \in V, w \in V ⟼ ⦋ {Base}_{v} / a ⦌ ⦋ {Base}_{w} / b ⦌ \{⟨f, g⟩ \| ((f \in (b^{a}) \land g \in (a^{b})) \land \forall x \in a \forall y \in b (f (x) \leq_{w} y \leftrightarrow x \leq_{v} g (y)))\})$
7		fvexd	$⊢ ((V \in X \land W \in Y) \land (v = V \land w = W)) \to {Base}_{v} \in V$
8		simprl	$⊢ ((V \in X \land W \in Y) \land (v = V \land w = W)) \to v = V$
9	8	fveq2d	$⊢ ((V \in X \land W \in Y) \land (v = V \land w = W)) \to {Base}_{v} = {Base}_{V}$
10	9 1	eqtr4di	$⊢ ((V \in X \land W \in Y) \land (v = V \land w = W)) \to {Base}_{v} = A$
11		fvexd	$⊢ (((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \to {Base}_{w} \in V$
12		simplrr	$⊢ (((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \to w = W$
13	12	fveq2d	$⊢ (((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \to {Base}_{w} = {Base}_{W}$
14	13 2	eqtr4di	$⊢ (((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \to {Base}_{w} = B$
15		simpr	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to b = B$
16		simplr	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to a = A$
17	15 16	oveq12d	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to b^{a} = B^{A}$
18	17	eleq2d	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to (f \in (b^{a}) \leftrightarrow f \in (B^{A}))$
19	16 15	oveq12d	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to a^{b} = A^{B}$
20	19	eleq2d	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to (g \in (a^{b}) \leftrightarrow g \in (A^{B}))$
21	18 20	anbi12d	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to ((f \in (b^{a}) \land g \in (a^{b})) \leftrightarrow (f \in (B^{A}) \land g \in (A^{B})))$
22	12	adantr	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to w = W$
23	22	fveq2d	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to \leq_{w} = \leq_{W}$
24	23 4	eqtr4di	Could not format ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( le ` w ) = .c_ ) : No typesetting found for \|- ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( le ` w ) = .c_ ) with typecode \|-
25	24	breqd	Could not format ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( ( f ` x ) ( le ` w ) y <-> ( f ` x ) .c_ y ) ) : No typesetting found for \|- ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( ( f ` x ) ( le ` w ) y <-> ( f ` x ) .c_ y ) ) with typecode \|-
26	8	ad2antrr	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to v = V$
27	26	fveq2d	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to \leq_{v} = \leq_{V}$
28	27 3	eqtr4di	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to \leq_{v} = \underset{˙}{\leq}$
29	28	breqd	$⊢ ((((V \in X \land W \in Y) \land (v = V \land w = W)) \land a = A) \land b = B) \to (x \leq_{v} g (y) \leftrightarrow x \underset{˙}{\leq} g (y))$
30	25 29	bibi12d	Could not format ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) <-> ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) : No typesetting found for \|- ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) <-> ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) with typecode \|-
31	15 30	raleqbidv	Could not format ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) <-> A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) : No typesetting found for \|- ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) <-> A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) with typecode \|-
32	16 31	raleqbidv	Could not format ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) <-> A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) : No typesetting found for \|- ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) <-> A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) with typecode \|-
33	21 32	anbi12d	Could not format ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) <-> ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) ) : No typesetting found for \|- ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) <-> ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) ) with typecode \|-
34	33	opabbidv	Could not format ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> { <. f , g >. \| ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) } = { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) : No typesetting found for \|- ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> { <. f , g >. \| ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) } = { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode \|-
35	11 14 34	csbied2	Could not format ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) -> [_ ( Base ` w ) / b ]_ { <. f , g >. \| ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) } = { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) : No typesetting found for \|- ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) -> [_ ( Base ` w ) / b ]_ { <. f , g >. \| ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) } = { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode \|-
36	7 10 35	csbied2	Could not format ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) -> [_ ( Base ` v ) / a ]_ [_ ( Base ` w ) / b ]_ { <. f , g >. \| ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) } = { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) : No typesetting found for \|- ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) -> [_ ( Base ` v ) / a ]_ [_ ( Base ` w ) / b ]_ { <. f , g >. \| ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) } = { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode \|-
37		simpl	$⊢ (V \in X \land W \in Y) \to V \in X$
38	37	elexd	$⊢ (V \in X \land W \in Y) \to V \in V$
39		simpr	$⊢ (V \in X \land W \in Y) \to W \in Y$
40	39	elexd	$⊢ (V \in X \land W \in Y) \to W \in V$
41		ovexd	$⊢ (V \in X \land W \in Y) \to B^{A} \in V$
42		ovexd	$⊢ (V \in X \land W \in Y) \to A^{B} \in V$
43		simprll	Could not format ( ( ( V e. X /\ W e. Y ) /\ ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) -> f e. ( B ^m A ) ) : No typesetting found for \|- ( ( ( V e. X /\ W e. Y ) /\ ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) -> f e. ( B ^m A ) ) with typecode \|-
44		simprlr	Could not format ( ( ( V e. X /\ W e. Y ) /\ ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) -> g e. ( A ^m B ) ) : No typesetting found for \|- ( ( ( V e. X /\ W e. Y ) /\ ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) -> g e. ( A ^m B ) ) with typecode \|-
45	41 42 43 44	opabex2	Could not format ( ( V e. X /\ W e. Y ) -> { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } e. _V ) : No typesetting found for \|- ( ( V e. X /\ W e. Y ) -> { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } e. _V ) with typecode \|-
46	6 36 38 40 45	ovmpod	Could not format ( ( V e. X /\ W e. Y ) -> ( V MGalConn W ) = { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) : No typesetting found for \|- ( ( V e. X /\ W e. Y ) -> ( V MGalConn W ) = { <. f , g >. \| ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode \|-

Metamath Proof Explorer

Theorem mgcoval

Proof