Theorem mgcf1

Description: The lower adjoint F of a Galois connection is a function. (Contributed by Thierry Arnoux, 24-Apr-2024)

	Ref	Expression
Hypotheses	mgcoval.1	⊢ 𝐴 = ( Base ‘ 𝑉 )
	mgcoval.2	⊢ 𝐵 = ( Base ‘ 𝑊 )
	mgcoval.3	⊢ ≤ = ( le ‘ 𝑉 )
	mgcoval.4	⊢ ≲ = ( le ‘ 𝑊 )
	mgcval.1	⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
	mgcval.2	⊢ ( 𝜑 → 𝑉 ∈ Proset )
	mgcval.3	⊢ ( 𝜑 → 𝑊 ∈ Proset )
	mgccole.1	⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
Assertion	mgcf1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mgcoval.1	⊢ 𝐴 = ( Base ‘ 𝑉 )
2		mgcoval.2	⊢ 𝐵 = ( Base ‘ 𝑊 )
3		mgcoval.3	⊢ ≤ = ( le ‘ 𝑉 )
4		mgcoval.4	⊢ ≲ = ( le ‘ 𝑊 )
5		mgcval.1	⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
6		mgcval.2	⊢ ( 𝜑 → 𝑉 ∈ Proset )
7		mgcval.3	⊢ ( 𝜑 → 𝑊 ∈ Proset )
8		mgccole.1	⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
9	1 2 3 4 5 6 7	mgcval	⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) )
10	8 9	mpbid	⊢ ( 𝜑 → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) )
11	10	simplld	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )