Theorem mntoval

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

	Ref	Expression
Hypotheses	mntoval.1	$$⊢A={\mathrm{Base}}_V$$
	mntoval.2	$$⊢B={\mathrm{Base}}_W$$
	mntoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
	mntoval.4	No typesetting found for |- .c_ = ( le ` W ) with typecode |-
Assertion	mntoval	Could not format assertion : No typesetting found for |- ( ( V e. X /\ W e. Y ) -> ( V Monot W ) = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mntoval.1	$$⊢A={\mathrm{Base}}_V$$
2		mntoval.2	$$⊢B={\mathrm{Base}}_W$$
3		mntoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
4		mntoval.4	Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5		df-mnt	Could not format Monot = ( v e. _V , w e. _V |-> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } ) : No typesetting found for |- Monot = ( v e. _V , w e. _V |-> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } ) with typecode |-
6	5	a1i	Could not format ( ( V e. X /\ W e. Y ) -> Monot = ( v e. _V , w e. _V |-> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } ) ) : No typesetting found for |- ( ( V e. X /\ W e. Y ) -> Monot = ( v e. _V , w e. _V |-> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } ) ) with typecode |-
7		fvexd	$$⊢\left(v=V\wedge w=W\right)\to {\mathrm{Base}}_v\in \mathrm{V}$$
8		fveq2	$$⊢v=V\to {\mathrm{Base}}_v={\mathrm{Base}}_V$$
9	8 1	eqtr4di	$$⊢v=V\to {\mathrm{Base}}_v=A$$
10	9	adantr	$$⊢\left(v=V\wedge w=W\right)\to {\mathrm{Base}}_v=A$$
11		simplr	$$⊢\left(\left(v=V\wedge w=W\right)\wedge a=A\right)\to w=W$$
12	11	fveq2d	$$⊢\left(\left(v=V\wedge w=W\right)\wedge a=A\right)\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
13	12 2	eqtr4di	$$⊢\left(\left(v=V\wedge w=W\right)\wedge a=A\right)\to {\mathrm{Base}}_w=B$$
14		simpr	$$⊢\left(\left(v=V\wedge w=W\right)\wedge a=A\right)\to a=A$$
15	13 14	oveq12d	$$⊢\left(\left(v=V\wedge w=W\right)\wedge a=A\right)\to {{\mathrm{Base}}_w}^a=B^A$$
16		simpll	$$⊢\left(\left(v=V\wedge w=W\right)\wedge a=A\right)\to v=V$$
17	16	fveq2d	$$⊢\left(\left(v=V\wedge w=W\right)\wedge a=A\right)\to {\le }_v={\le }_V$$
18	17 3	eqtr4di	$$⊢\left(\left(v=V\wedge w=W\right)\wedge a=A\right)\to {\le }_v=\underset{\dot{}}{\le }$$
19	18	breqd	$$⊢\left(\left(v=V\wedge w=W\right)\wedge a=A\right)\to \left(x{\le }_{v}y\leftrightarrow x\underset{\dot{}}{\le }y\right)$$
20	11	fveq2d	$$⊢\left(\left(v=V\wedge w=W\right)\wedge a=A\right)\to {\le }_w={\le }_W$$
21	20 4	eqtr4di	Could not format ( ( ( v = V /\ w = W ) /\ a = A ) -> ( le ` w ) = .c_ ) : No typesetting found for |- ( ( ( v = V /\ w = W ) /\ a = A ) -> ( le ` w ) = .c_ ) with typecode |-
22	21	breqd	Could not format ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( f ` x ) ( le ` w ) ( f ` y ) <-> ( f ` x ) .c_ ( f ` y ) ) ) : No typesetting found for |- ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( f ` x ) ( le ` w ) ( f ` y ) <-> ( f ` x ) .c_ ( f ` y ) ) ) with typecode |-
23	19 22	imbi12d	Could not format ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) ) : No typesetting found for |- ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) ) with typecode |-
24	14 23	raleqbidv	Could not format ( ( ( v = V /\ w = W ) /\ a = A ) -> ( A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) ) : No typesetting found for |- ( ( ( v = V /\ w = W ) /\ a = A ) -> ( A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) ) with typecode |-
25	14 24	raleqbidv	Could not format ( ( ( v = V /\ w = W ) /\ a = A ) -> ( A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) ) : No typesetting found for |- ( ( ( v = V /\ w = W ) /\ a = A ) -> ( A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) ) with typecode |-
26	15 25	rabeqbidv	Could not format ( ( ( v = V /\ w = W ) /\ a = A ) -> { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) : No typesetting found for |- ( ( ( v = V /\ w = W ) /\ a = A ) -> { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) with typecode |-
27	7 10 26	csbied2	Could not format ( ( v = V /\ w = W ) -> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) : No typesetting found for |- ( ( v = V /\ w = W ) -> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) with typecode |-
28	27	adantl	Could not format ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) -> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) : No typesetting found for |- ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) -> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) with typecode |-
29		elex	$$⊢V\in X\to V\in \mathrm{V}$$
30	29	adantr	$$⊢\left(V\in X\wedge W\in Y\right)\to V\in \mathrm{V}$$
31		elex	$$⊢W\in Y\to W\in \mathrm{V}$$
32	31	adantl	$$⊢\left(V\in X\wedge W\in Y\right)\to W\in \mathrm{V}$$
33		eqid	Could not format { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } : No typesetting found for |- { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } with typecode |-
34		ovexd	$$⊢\left(V\in X\wedge W\in Y\right)\to B^A\in \mathrm{V}$$
35	33 34	rabexd	Could not format ( ( V e. X /\ W e. Y ) -> { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } e. _V ) : No typesetting found for |- ( ( V e. X /\ W e. Y ) -> { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } e. _V ) with typecode |-
36	6 28 30 32 35	ovmpod	Could not format ( ( V e. X /\ W e. Y ) -> ( V Monot W ) = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) : No typesetting found for |- ( ( V e. X /\ W e. Y ) -> ( V Monot W ) = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) with typecode |-