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 ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) } )