This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ismnt

Description: Express the statement " F is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024)

Ref Expression
Hypotheses mntoval.1 ⊢ A = Base V
mntoval.2 ⊢ B = Base W
mntoval.3 ⊢ ≤ ˙ = ≤ V
mntoval.4 No typesetting found for |- .c_ = ( le ` W ) with typecode |-
Assertion ismnt Could not format assertion : No typesetting found for |- ( ( V e. X /\ W e. Y ) -> ( 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 |-

Proof

Step Hyp Ref Expression
1 mntoval.1 ⊢ A = Base V
2 mntoval.2 ⊢ B = Base W
3 mntoval.3 ⊢ ≤ ˙ = ≤ V
4 mntoval.4 Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5 1 2 3 4 mntoval 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 |-
6 5 eleq2d Could not format ( ( V e. X /\ W e. Y ) -> ( F e. ( V Monot W ) <-> F e. { 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 ) -> ( F e. ( V Monot W ) <-> F e. { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) ) with typecode |-
7 fveq1 ⊢ f = F → f ⁡ x = F ⁡ x
8 fveq1 ⊢ f = F → f ⁡ y = F ⁡ y
9 7 8 breq12d Could not format ( f = F -> ( ( f ` x ) .c_ ( f ` y ) <-> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for |- ( f = F -> ( ( f ` x ) .c_ ( f ` y ) <-> ( F ` x ) .c_ ( F ` y ) ) ) with typecode |-
10 9 imbi2d Could not format ( f = F -> ( ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) <-> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) : No typesetting found for |- ( f = F -> ( ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) <-> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) with typecode |-
11 10 2ralbidv Could not format ( f = F -> ( A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) <-> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) : No typesetting found for |- ( f = F -> ( A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) <-> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) with typecode |-
12 11 elrab Could not format ( F e. { 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. { 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 |-
13 6 12 bitrdi Could not format ( ( V e. X /\ W e. Y ) -> ( F e. ( 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 ) -> ( F e. ( 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 |-
14 2 fvexi ⊢ B ∈ V
15 1 fvexi ⊢ A ∈ V
16 14 15 elmap ⊢ F ∈ B A ↔ F : A ⟶ B
17 16 anbi1i Could not format ( ( F e. ( B ^m A ) /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) <-> ( F : A --> B /\ 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 : A --> B /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) with typecode |-
18 13 17 bitrdi Could not format ( ( V e. X /\ W e. Y ) -> ( 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. X /\ W e. Y ) -> ( 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 |-