Theorem ismntd

Description: Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024)

	Ref	Expression
Hypotheses	ismntd.1	$$⊢A={\mathrm{Base}}_V$$
	ismntd.2	$$⊢B={\mathrm{Base}}_W$$
	ismntd.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
	ismntd.4	No typesetting found for |- .c_ = ( le ` W ) with typecode |-
	ismntd.5	$$⊢\phi \to V\in C$$
	ismntd.6	$$⊢\phi \to W\in D$$
	ismntd.7	No typesetting found for |- ( ph -> F e. ( V Monot W ) ) with typecode |-
	ismntd.8	$$⊢\phi \to X\in A$$
	ismntd.9	$$⊢\phi \to Y\in A$$
	ismntd.10	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
Assertion	ismntd	Could not format assertion : No typesetting found for |- ( ph -> ( F ` X ) .c_ ( F ` Y ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ismntd.1	$$⊢A={\mathrm{Base}}_V$$
2		ismntd.2	$$⊢B={\mathrm{Base}}_W$$
3		ismntd.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
4		ismntd.4	Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5		ismntd.5	$$⊢\phi \to V\in C$$
6		ismntd.6	$$⊢\phi \to W\in D$$
7		ismntd.7	Could not format ( ph -> F e. ( V Monot W ) ) : No typesetting found for |- ( ph -> F e. ( V Monot W ) ) with typecode |-
8		ismntd.8	$$⊢\phi \to X\in A$$
9		ismntd.9	$$⊢\phi \to Y\in A$$
10		ismntd.10	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
11	1 2 3 4	ismnt	Could not format ( ( V e. C /\ W e. D ) -> ( F e. ( V Monot W ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) ) : No typesetting found for |- ( ( V e. C /\ W e. D ) -> ( F e. ( V Monot W ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) ) with typecode |-
12	11	biimp3a	Could not format ( ( V e. C /\ W e. D /\ F e. ( V Monot W ) ) -> ( F : A --> B /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) : No typesetting found for |- ( ( V e. C /\ W e. D /\ F e. ( V Monot W ) ) -> ( F : A --> B /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) with typecode |-
13	12	simprd	Could not format ( ( V e. C /\ W e. D /\ F e. ( V Monot W ) ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for |- ( ( V e. C /\ W e. D /\ F e. ( V Monot W ) ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode |-
14	5 6 7 13	syl3anc	Could not format ( ph -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for |- ( ph -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode |-
15		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }y\right)$$
16		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
17	16	breq1d	Could not format ( x = X -> ( ( F ` x ) .c_ ( F ` y ) <-> ( F ` X ) .c_ ( F ` y ) ) ) : No typesetting found for |- ( x = X -> ( ( F ` x ) .c_ ( F ` y ) <-> ( F ` X ) .c_ ( F ` y ) ) ) with typecode |-
18	15 17	imbi12d	Could not format ( x = X -> ( ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> ( X .<_ y -> ( F ` X ) .c_ ( F ` y ) ) ) ) : No typesetting found for |- ( x = X -> ( ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> ( X .<_ y -> ( F ` X ) .c_ ( F ` y ) ) ) ) with typecode |-
19		breq2	$$⊢y=Y\to \left(X\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
20		fveq2	$$⊢y=Y\to F\left(y\right)=F\left(Y\right)$$
21	20	breq2d	Could not format ( y = Y -> ( ( F ` X ) .c_ ( F ` y ) <-> ( F ` X ) .c_ ( F ` Y ) ) ) : No typesetting found for |- ( y = Y -> ( ( F ` X ) .c_ ( F ` y ) <-> ( F ` X ) .c_ ( F ` Y ) ) ) with typecode |-
22	19 21	imbi12d	Could not format ( y = Y -> ( ( X .<_ y -> ( F ` X ) .c_ ( F ` y ) ) <-> ( X .<_ Y -> ( F ` X ) .c_ ( F ` Y ) ) ) ) : No typesetting found for |- ( y = Y -> ( ( X .<_ y -> ( F ` X ) .c_ ( F ` y ) ) <-> ( X .<_ Y -> ( F ` X ) .c_ ( F ` Y ) ) ) ) with typecode |-
23		eqidd	$$⊢\left(\phi \wedge x=X\right)\to A=A$$
24	18 22 8 23 9	rspc2vd	Could not format ( ph -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) -> ( X .<_ Y -> ( F ` X ) .c_ ( F ` Y ) ) ) ) : No typesetting found for |- ( ph -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) -> ( X .<_ Y -> ( F ` X ) .c_ ( F ` Y ) ) ) ) with typecode |-
25	14 10 24	mp2d	Could not format ( ph -> ( F ` X ) .c_ ( F ` Y ) ) : No typesetting found for |- ( ph -> ( F ` X ) .c_ ( F ` Y ) ) with typecode |-