mntoval

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

	Ref	Expression
Hypotheses	mntoval.1	$⊢ A = {Base}_{V}$
	mntoval.2	$⊢ B = {Base}_{W}$
	mntoval.3	$⊢ \underset{˙}{\leq} = \leq_{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 = {Base}_{V}$
2		mntoval.2	$⊢ B = {Base}_{W}$
3		mntoval.3	$⊢ \underset{˙}{\leq} = \leq_{V}$
4		mntoval.4	Could not format .c_ = ( le ` W ) : No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
5		df-mnt	$⊢ Monot = (v \in V, w \in V ⟼ ⦋ {Base}_{v} / a ⦌ \{f \in ({Base}_{w}^{a}) \| \forall x \in a \forall y \in a (x \leq_{v} y \to f (x) \leq_{w} f (y))\})$
6	5	a1i	$⊢ (V \in X \land W \in Y) \to Monot = (v \in V, w \in V ⟼ ⦋ {Base}_{v} / a ⦌ \{f \in ({Base}_{w}^{a}) \| \forall x \in a \forall y \in a (x \leq_{v} y \to f (x) \leq_{w} f (y))\})$
7		fvexd	$⊢ (v = V \land w = W) \to {Base}_{v} \in V$
8		fveq2	$⊢ v = V \to {Base}_{v} = {Base}_{V}$
9	8 1	eqtr4di	$⊢ v = V \to {Base}_{v} = A$
10	9	adantr	$⊢ (v = V \land w = W) \to {Base}_{v} = A$
11		simplr	$⊢ ((v = V \land w = W) \land a = A) \to w = W$
12	11	fveq2d	$⊢ ((v = V \land w = W) \land a = A) \to {Base}_{w} = {Base}_{W}$
13	12 2	eqtr4di	$⊢ ((v = V \land w = W) \land a = A) \to {Base}_{w} = B$
14		simpr	$⊢ ((v = V \land w = W) \land a = A) \to a = A$
15	13 14	oveq12d	$⊢ ((v = V \land w = W) \land a = A) \to {Base}_{w}^{a} = B^{A}$
16		simpll	$⊢ ((v = V \land w = W) \land a = A) \to v = V$
17	16	fveq2d	$⊢ ((v = V \land w = W) \land a = A) \to \leq_{v} = \leq_{V}$
18	17 3	eqtr4di	$⊢ ((v = V \land w = W) \land a = A) \to \leq_{v} = \underset{˙}{\leq}$
19	18	breqd	$⊢ ((v = V \land w = W) \land a = A) \to (x \leq_{v} y \leftrightarrow x \underset{˙}{\leq} y)$
20	11	fveq2d	$⊢ ((v = V \land w = W) \land a = A) \to \leq_{w} = \leq_{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 V$
30	29	adantr	$⊢ (V \in X \land W \in Y) \to V \in V$
31		elex	$⊢ W \in Y \to W \in V$
32	31	adantl	$⊢ (V \in X \land W \in Y) \to W \in 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	$⊢ (V \in X \land W \in Y) \to B^{A} \in 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 \|-

Metamath Proof Explorer

Theorem mntoval

Proof