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

Metamath Proof Explorer

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 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } )