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

Metamath Proof Explorer

Definition df-mnt

Description: Define a monotone function between two ordered sets. (Contributed by Thierry Arnoux, 20-Apr-2024)

Ref Expression
Assertion df-mnt Monot = ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( Base ‘ 𝑣 ) / 𝑎 ⦌ { 𝑓 ∈ ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmnt ⊢ Monot
1 vv ⊢ 𝑣
2 cvv ⊢ V
3 vw ⊢ 𝑤
4 cbs ⊢ Base
5 1 cv ⊢ 𝑣
6 5 4 cfv ⊢ ( Base ‘ 𝑣 )
7 va ⊢ 𝑎
8 vf ⊢ 𝑓
9 3 cv ⊢ 𝑤
10 9 4 cfv ⊢ ( Base ‘ 𝑤 )
11 cmap ⊢ ↑m
12 7 cv ⊢ 𝑎
13 10 12 11 co ⊢ ( ( Base ‘ 𝑤 ) ↑m 𝑎 )
14 vx ⊢ 𝑥
15 vy ⊢ 𝑦
16 14 cv ⊢ 𝑥
17 cple ⊢ le
18 5 17 cfv ⊢ ( le ‘ 𝑣 )
19 15 cv ⊢ 𝑦
20 16 19 18 wbr ⊢ 𝑥 ( le ‘ 𝑣 ) 𝑦
21 8 cv ⊢ 𝑓
22 16 21 cfv ⊢ ( 𝑓 ‘ 𝑥 )
23 9 17 cfv ⊢ ( le ‘ 𝑤 )
24 19 21 cfv ⊢ ( 𝑓 ‘ 𝑦 )
25 22 24 23 wbr ⊢ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 )
26 20 25 wi ⊢ ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) )
27 26 15 12 wral ⊢ ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) )
28 27 14 12 wral ⊢ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) )
29 28 8 13 crab ⊢ { 𝑓 ∈ ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) }
30 7 6 29 csb ⊢ ⦋ ( Base ‘ 𝑣 ) / 𝑎 ⦌ { 𝑓 ∈ ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) }
31 1 3 2 2 30 cmpo ⊢ ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( Base ‘ 𝑣 ) / 𝑎 ⦌ { 𝑓 ∈ ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) } )
32 0 31 wceq ⊢ Monot = ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( Base ‘ 𝑣 ) / 𝑎 ⦌ { 𝑓 ∈ ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) } )