This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mgcf1olem1

Description: Property of a Galois connection, lemma for mgcf1o . (Contributed by Thierry Arnoux, 26-Jul-2024)

Ref Expression
Hypotheses mgcf1o.h ⊢ H = V MGalConn W
mgcf1o.a ⊢ A = Base V
mgcf1o.b ⊢ B = Base W
mgcf1o.1 ⊢ ≤ ˙ = ≤ V
mgcf1o.2 No typesetting found for |- .c_ = ( le ` W ) with typecode |-
mgcf1o.v ⊢ φ → V ∈ Poset
mgcf1o.w ⊢ φ → W ∈ Poset
mgcf1o.f ⊢ φ → F H G
mgcf1olem1.1 ⊢ φ → X ∈ A
Assertion mgcf1olem1 ⊢ φ → F ⁡ G ⁡ F ⁡ X = F ⁡ X

Proof

Step Hyp Ref Expression
1 mgcf1o.h ⊢ H = V MGalConn W
2 mgcf1o.a ⊢ A = Base V
3 mgcf1o.b ⊢ B = Base W
4 mgcf1o.1 ⊢ ≤ ˙ = ≤ V
5 mgcf1o.2 Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
6 mgcf1o.v ⊢ φ → V ∈ Poset
7 mgcf1o.w ⊢ φ → W ∈ Poset
8 mgcf1o.f ⊢ φ → F H G
9 mgcf1olem1.1 ⊢ φ → X ∈ A
10 posprs ⊢ V ∈ Poset → V ∈ Proset
11 6 10 syl ⊢ φ → V ∈ Proset
12 posprs ⊢ W ∈ Poset → W ∈ Proset
13 7 12 syl ⊢ φ → W ∈ Proset
14 2 3 4 5 1 11 13 dfmgc2 Could not format ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) ) with typecode |-
15 8 14 mpbid Could not format ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) with typecode |-
16 15 simplld ⊢ φ → F : A ⟶ B
17 15 simplrd ⊢ φ → G : B ⟶ A
18 16 9 ffvelcdmd ⊢ φ → F ⁡ X ∈ B
19 17 18 ffvelcdmd ⊢ φ → G ⁡ F ⁡ X ∈ A
20 16 19 ffvelcdmd ⊢ φ → F ⁡ G ⁡ F ⁡ X ∈ B
21 2 3 4 5 1 11 13 8 18 mgccole2 Could not format ( ph -> ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) ) : No typesetting found for |- ( ph -> ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) ) with typecode |-
22 2 3 4 5 1 11 13 8 9 mgccole1 ⊢ φ → X ≤ ˙ G ⁡ F ⁡ X
23 2 3 4 5 1 11 13 8 9 19 22 mgcmnt1 Could not format ( ph -> ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) : No typesetting found for |- ( ph -> ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) with typecode |-
24 3 5 posasymb Could not format ( ( W e. Poset /\ ( F ` ( G ` ( F ` X ) ) ) e. B /\ ( F ` X ) e. B ) -> ( ( ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) /\ ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) <-> ( F ` ( G ` ( F ` X ) ) ) = ( F ` X ) ) ) : No typesetting found for |- ( ( W e. Poset /\ ( F ` ( G ` ( F ` X ) ) ) e. B /\ ( F ` X ) e. B ) -> ( ( ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) /\ ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) <-> ( F ` ( G ` ( F ` X ) ) ) = ( F ` X ) ) ) with typecode |-
25 24 biimpa Could not format ( ( ( W e. Poset /\ ( F ` ( G ` ( F ` X ) ) ) e. B /\ ( F ` X ) e. B ) /\ ( ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) /\ ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) ) -> ( F ` ( G ` ( F ` X ) ) ) = ( F ` X ) ) : No typesetting found for |- ( ( ( W e. Poset /\ ( F ` ( G ` ( F ` X ) ) ) e. B /\ ( F ` X ) e. B ) /\ ( ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) /\ ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) ) -> ( F ` ( G ` ( F ` X ) ) ) = ( F ` X ) ) with typecode |-
26 7 20 18 21 23 25 syl32anc ⊢ φ → F ⁡ G ⁡ F ⁡ X = F ⁡ X