Metamath Proof Explorer

Theorem mgcmnt2d

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

		Ref	Expression
	Hypotheses	mgcmntd.1	⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
		mgcmntd.2	⊢ ( 𝜑 → 𝑉 ∈ Proset )
		mgcmntd.3	⊢ ( 𝜑 → 𝑊 ∈ Proset )
		mgcmntd.4	⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
	Assertion	mgcmnt2d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑊 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	mgcf2	⊢ ( 𝜑 → 𝐺 : ( 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	simprd	⊢ ( 𝜑 → ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( 𝑢 ( le ‘ 𝑊 ) 𝑣 → ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑣 ) ) )
14	6 5 8 7	ismnt	⊢ ( ( 𝑊 ∈ Proset ∧ 𝑉 ∈ Proset ) → ( 𝐺 ∈ ( 𝑊 Monot 𝑉 ) ↔ ( 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( 𝑢 ( le ‘ 𝑊 ) 𝑣 → ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑣 ) ) ) ) )
15	14	biimpar	⊢ ( ( ( 𝑊 ∈ Proset ∧ 𝑉 ∈ Proset ) ∧ ( 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( 𝑢 ( le ‘ 𝑊 ) 𝑣 → ( 𝐺 ‘ 𝑢 ) ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑣 ) ) ) ) → 𝐺 ∈ ( 𝑊 Monot 𝑉 ) )
16	3 2 9 13 15	syl22anc	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑊 Monot 𝑉 ) )