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 = ( Base ` V )
	mgcoval.2	|- B = ( Base ` W )
	mgcoval.3	|- .<_ = ( le ` V )
	mgcoval.4	|- .c_ = ( le ` W )
	mgcval.1	|- H = ( V MGalConn W )
	mgcval.2	|- ( ph -> V e. Proset )
	mgcval.3	|- ( ph -> W e. Proset )
	mgccole.1	|- ( ph -> F H G )
Assertion	mgcf1	|- ( ph -> F : A --> B )

Proof

Step	Hyp	Ref	Expression
1		mgcoval.1	|- A = ( Base ` V )
2		mgcoval.2	|- B = ( Base ` W )
3		mgcoval.3	|- .<_ = ( le ` V )
4		mgcoval.4	|- .c_ = ( le ` W )
5		mgcval.1	|- H = ( V MGalConn W )
6		mgcval.2	|- ( ph -> V e. Proset )
7		mgcval.3	|- ( ph -> W e. Proset )
8		mgccole.1	|- ( ph -> F H G )
9	1 2 3 4 5 6 7	mgcval	|- ( 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 ) ) ) ) )
10	8 9	mpbid	|- ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) )
11	10	simplld	|- ( ph -> F : A --> B )