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

Metamath Proof Explorer

Theorem mgcmnt1d

Description: Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024)

Ref Expression
Hypotheses mgcmntd.1 ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
mgcmntd.2 ⊢ ( 𝜑 → 𝑉 ∈ Proset )
mgcmntd.3 ⊢ ( 𝜑 → 𝑊 ∈ Proset )
mgcmntd.4 ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
Assertion mgcmnt1d ( 𝜑 → 𝐹 ∈ ( 𝑉 Monot 𝑊 ) )

Proof

Step Hyp Ref Expression
1 mgcmntd.1 ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
2 mgcmntd.2 ⊢ ( 𝜑 → 𝑉 ∈ Proset )
3 mgcmntd.3 ⊢ ( 𝜑 → 𝑊 ∈ Proset )
4 mgcmntd.4 ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
5 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
6 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7 eqid ⊢ ( le ‘ 𝑉 ) = ( le ‘ 𝑉 )
8 eqid ⊢ ( le ‘ 𝑊 ) = ( le ‘ 𝑊 )
9 5 6 7 8 1 2 3 4 mgcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) )
10 5 6 7 8 1 2 3 dfmgc2 ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ∧ 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ) ∧ ( ( ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ∀ 𝑦 ∈ ( Base ‘ 𝑉 ) ( 𝑥 ( le ‘ 𝑉 ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( 𝑢 ( le ‘ 𝑊 ) 𝑣 → ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ( le ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) ) )
11 4 10 mpbid ⊢ ( 𝜑 → ( ( 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ∧ 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ) ∧ ( ( ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ∀ 𝑦 ∈ ( Base ‘ 𝑉 ) ( 𝑥 ( le ‘ 𝑉 ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( 𝑢 ( le ‘ 𝑊 ) 𝑣 → ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ( le ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
12 11 simprld ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ∀ 𝑦 ∈ ( Base ‘ 𝑉 ) ( 𝑥 ( le ‘ 𝑉 ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( 𝑢 ( le ‘ 𝑊 ) 𝑣 → ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑣 ) ) ) )
13 12 simpld ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ∀ 𝑦 ∈ ( Base ‘ 𝑉 ) ( 𝑥 ( le ‘ 𝑉 ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) )
14 5 6 7 8 ismnt ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ↔ ( 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ∀ 𝑦 ∈ ( Base ‘ 𝑉 ) ( 𝑥 ( le ‘ 𝑉 ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
15 14 biimpar ⊢ ( ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) ∧ ( 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ∀ 𝑦 ∈ ( Base ‘ 𝑉 ) ( 𝑥 ( le ‘ 𝑉 ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐹 ∈ ( 𝑉 Monot 𝑊 ) )
16 2 3 9 13 15 syl22anc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑉 Monot 𝑊 ) )