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	⊢ 𝐴 = ( Base ‘ 𝑉 )
		mntoval.2	⊢ 𝐵 = ( Base ‘ 𝑊 )
		mntoval.3	⊢ ≤ = ( le ‘ 𝑉 )
		mntoval.4	⊢ ≲ = ( le ‘ 𝑊 )
	Assertion	ismnt	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mntoval.1	⊢ 𝐴 = ( Base ‘ 𝑉 )
2		mntoval.2	⊢ 𝐵 = ( Base ‘ 𝑊 )
3		mntoval.3	⊢ ≤ = ( le ‘ 𝑉 )
4		mntoval.4	⊢ ≲ = ( le ‘ 𝑊 )
5	1 2 3 4	mntoval	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑉 Monot 𝑊 ) = { 𝑓 ∈ ( 𝐵 ↑_m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } )
6	5	eleq2d	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝐵 ↑_m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } ) )
7		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
8		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
9	7 8	breq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
10	9	imbi2d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) )
11	10	2ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) )
12	11	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝐵 ↑_m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝑓 ‘ 𝑥 ) ≲ ( 𝑓 ‘ 𝑦 ) ) } ↔ ( 𝐹 ∈ ( 𝐵 ↑_m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) )
13	6 12	bitrdi	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ↔ ( 𝐹 ∈ ( 𝐵 ↑_m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) ) )
14	2	fvexi	⊢ 𝐵 ∈ V
15	1	fvexi	⊢ 𝐴 ∈ V
16	14 15	elmap	⊢ ( 𝐹 ∈ ( 𝐵 ↑_m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 )
17	16	anbi1i	⊢ ( ( 𝐹 ∈ ( 𝐵 ↑_m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) )
18	13 17	bitrdi	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) ) )