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	$$⊢A={\mathrm{Base}}_V$$
	mgcoval.2	$$⊢B={\mathrm{Base}}_W$$
	mgcoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
	mgcoval.4	No typesetting found for |- .c_ = ( le ` W ) with typecode |-
	mgcval.1	$$⊢H=V\mathrm{MGalConn}W$$
	mgcval.2	$$⊢\phi \to V\in \mathrm{Proset}$$
	mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
	mgccole.1	$$⊢\phi \to FHG$$
Assertion	mgcf1	$$⊢\phi \to F:A⟶B$$

Proof

Step	Hyp	Ref	Expression
1		mgcoval.1	$$⊢A={\mathrm{Base}}_V$$
2		mgcoval.2	$$⊢B={\mathrm{Base}}_W$$
3		mgcoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
4		mgcoval.4	Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5		mgcval.1	$$⊢H=V\mathrm{MGalConn}W$$
6		mgcval.2	$$⊢\phi \to V\in \mathrm{Proset}$$
7		mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
8		mgccole.1	$$⊢\phi \to FHG$$
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	simplld	$$⊢\phi \to F:A⟶B$$