Theorem mntoval

Description: Operation value of the monotone function. (Contributed by Thierry Arnoux, 23-Apr-2024)

	Ref	Expression
Hypotheses	mntoval.1	⊢ 𝐴 = ( Base ‘ 𝑉 )
	mntoval.2	⊢ 𝐵 = ( Base ‘ 𝑊 )
	mntoval.3	⊢ ≤ = ( le ‘ 𝑉 )
	mntoval.4	⊢ ≲ = ( le ‘ 𝑊 )
Assertion	mntoval	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑉 Monot 𝑊 ) = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		mntoval.1	⊢ 𝐴 = ( Base ‘ 𝑉 )
2		mntoval.2	⊢ 𝐵 = ( Base ‘ 𝑊 )
3		mntoval.3	⊢ ≤ = ( le ‘ 𝑉 )
4		mntoval.4	⊢ ≲ = ( le ‘ 𝑊 )
5		df-mnt	⊢ Monot = ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( Base ‘ 𝑣 ) / 𝑎 ⦌ { 𝑓 ∈ ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) } )
6	5	a1i	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → Monot = ( 𝑣 ∈ V , 𝑤 ∈ V ↦ ⦋ ( Base ‘ 𝑣 ) / 𝑎 ⦌ { 𝑓 ∈ ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) } ) )
7		fvexd	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) → ( Base ‘ 𝑣 ) ∈ V )
8		fveq2	⊢ ( 𝑣 = 𝑉 → ( Base ‘ 𝑣 ) = ( Base ‘ 𝑉 ) )
9	8 1	eqtr4di	⊢ ( 𝑣 = 𝑉 → ( Base ‘ 𝑣 ) = 𝐴 )
10	9	adantr	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) → ( Base ‘ 𝑣 ) = 𝐴 )
11		simplr	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → 𝑤 = 𝑊 )
12	11	fveq2d	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
13	12 2	eqtr4di	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( Base ‘ 𝑤 ) = 𝐵 )
14		simpr	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → 𝑎 = 𝐴 )
15	13 14	oveq12d	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) = ( 𝐵 ↑m 𝐴 ) )
16		simpll	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → 𝑣 = 𝑉 )
17	16	fveq2d	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( le ‘ 𝑣 ) = ( le ‘ 𝑉 ) )
18	17 3	eqtr4di	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( le ‘ 𝑣 ) = ≤ )
19	18	breqd	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( 𝑥 ( le ‘ 𝑣 ) 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
20	11	fveq2d	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( le ‘ 𝑤 ) = ( le ‘ 𝑊 ) )
21	20 4	eqtr4di	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( le ‘ 𝑤 ) = ≲ )
22	21	breqd	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) )
23	19 22	imbi12d	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) ) )
24	14 23	raleqbidv	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) ) )
25	14 24	raleqbidv	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) ) )
26	15 25	rabeqbidv	⊢ ( ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ∧ 𝑎 = 𝐴 ) → { 𝑓 ∈ ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) } = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } )
27	7 10 26	csbied2	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) → ⦋ ( Base ‘ 𝑣 ) / 𝑎 ⦌ { 𝑓 ∈ ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) } = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } )
28	27	adantl	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) ∧ ( 𝑣 = 𝑉 ∧ 𝑤 = 𝑊 ) ) → ⦋ ( Base ‘ 𝑣 ) / 𝑎 ⦌ { 𝑓 ∈ ( ( Base ‘ 𝑤 ) ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( le ‘ 𝑣 ) 𝑦 → ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑤 ) ( 𝑓 ‘ 𝑦 ) ) } = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } )
29		elex	⊢ ( 𝑉 ∈ 𝑋 → 𝑉 ∈ V )
30	29	adantr	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → 𝑉 ∈ V )
31		elex	⊢ ( 𝑊 ∈ 𝑌 → 𝑊 ∈ V )
32	31	adantl	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → 𝑊 ∈ V )
33		eqid	⊢ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) }
34		ovexd	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐵 ↑m 𝐴 ) ∈ V )
35	33 34	rabexd	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } ∈ V )
36	6 28 30 32 35	ovmpod	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑉 Monot 𝑊 ) = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } )