Metamath Proof Explorer
Description: The upper adjoint G 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 |
mgcf2 |
⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 ) |
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
|
simplrd |
⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 ) |