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 𝑊 ) )