ismntd

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

	Ref	Expression
Hypotheses	ismntd.1	$⊢ A = {Base}_{V}$
	ismntd.2	$⊢ B = {Base}_{W}$
	ismntd.3	$⊢ \underset{˙}{\leq} = \leq_{V}$
	ismntd.4	No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
	ismntd.5	$⊢ φ \to V \in C$
	ismntd.6	$⊢ φ \to W \in D$
	ismntd.7	$⊢ φ \to F \in (V Monot W)$
	ismntd.8	$⊢ φ \to X \in A$
	ismntd.9	$⊢ φ \to Y \in A$
	ismntd.10	$⊢ φ \to X \underset{˙}{\leq} 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 = {Base}_{V}$
2		ismntd.2	$⊢ B = {Base}_{W}$
3		ismntd.3	$⊢ \underset{˙}{\leq} = \leq_{V}$
4		ismntd.4	Could not format .c_ = ( le ` W ) : No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
5		ismntd.5	$⊢ φ \to V \in C$
6		ismntd.6	$⊢ φ \to W \in D$
7		ismntd.7	$⊢ φ \to F \in (V Monot W)$
8		ismntd.8	$⊢ φ \to X \in A$
9		ismntd.9	$⊢ φ \to Y \in A$
10		ismntd.10	$⊢ φ \to X \underset{˙}{\leq} 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 (x \underset{˙}{\leq} y \leftrightarrow X \underset{˙}{\leq} y)$
16		fveq2	$⊢ x = X \to F (x) = F (X)$
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 (X \underset{˙}{\leq} y \leftrightarrow X \underset{˙}{\leq} Y)$
20		fveq2	$⊢ y = Y \to F (y) = F (Y)$
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	$⊢ (φ \land x = X) \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 \|-

Metamath Proof Explorer

Theorem ismntd

Proof