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	$⊢ \underset{˙}{\leq} = \leq_{V}$
	mgcoval.4	No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
	mgcval.1	$⊢ H = V MGalConn W$
	mgcval.2	$⊢ φ \to V \in Proset$
	mgcval.3	$⊢ φ \to W \in Proset$
	mgccole.1	$⊢ φ \to F H G$
Assertion	mgcf2	$⊢ φ \to G : B ⟶ A$

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

Metamath Proof Explorer