Metamath Proof Explorer


Theorem mgcf2

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

Ref Expression
Hypotheses mgcoval.1 A = Base V
mgcoval.2 B = Base W
mgcoval.3 ˙ = V
mgcoval.4 No typesetting found for |- .c_ = ( le ` W ) with typecode |-
mgcval.1 No typesetting found for |- H = ( V MGalConn W ) with typecode |-
mgcval.2 φ V Proset
mgcval.3 φ W Proset
mgccole.1 φ F H G
Assertion mgcf2 φ G : B A

Proof

Step Hyp Ref Expression
1 mgcoval.1 A = Base V
2 mgcoval.2 B = Base W
3 mgcoval.3 ˙ = V
4 mgcoval.4 Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5 mgcval.1 Could not format H = ( V MGalConn W ) : No typesetting found for |- H = ( V MGalConn W ) with typecode |-
6 mgcval.2 φ V Proset
7 mgcval.3 φ W Proset
8 mgccole.1 φ F H G
9 1 2 3 4 5 6 7 mgcval Could not format ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) with typecode |-
10 8 9 mpbid Could not format ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) with typecode |-
11 10 simplrd φ G : B A