Metamath Proof Explorer

Definition df-mgc

Description: Define monotone Galois connections. See mgcval for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024)

Ref Expression
Assertion df-mgc ⊢ MGalConn = v ∈ V , w ∈ V ⟼ ⦋ Base v / a⦌ ⦋ Base w / b⦌ f g | f ∈ b a ∧ g ∈ a b ∧ ∀ x ∈ a ∀ y ∈ b f ⁡ x ≤ w y ↔ x ≤ v g ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgc class MGalConn
1 vv setvar v
2 cvv class V
3 vw setvar w
4 cbs class Base
5 1 cv setvar v
6 5 4 cfv class Base v
7 va setvar a
8 3 cv setvar w
9 8 4 cfv class Base w
10 vb setvar b
11 vf setvar f
12 vg setvar g
13 11 cv setvar f
14 10 cv setvar b
15 cmap class ↑ 𝑚
16 7 cv setvar a
17 14 16 15 co class b a
18 13 17 wcel wff f ∈ b a
19 12 cv setvar g
20 16 14 15 co class a b
21 19 20 wcel wff g ∈ a b
22 18 21 wa wff f ∈ b a ∧ g ∈ a b
23 vx setvar x
24 vy setvar y
25 23 cv setvar x
26 25 13 cfv class f ⁡ x
27 cple class le
28 8 27 cfv class ≤ w
29 24 cv setvar y
30 26 29 28 wbr wff f ⁡ x ≤ w y
31 5 27 cfv class ≤ v
32 29 19 cfv class g ⁡ y
33 25 32 31 wbr wff x ≤ v g ⁡ y
34 30 33 wb wff f ⁡ x ≤ w y ↔ x ≤ v g ⁡ y
35 34 24 14 wral wff ∀ y ∈ b f ⁡ x ≤ w y ↔ x ≤ v g ⁡ y
36 35 23 16 wral wff ∀ x ∈ a ∀ y ∈ b f ⁡ x ≤ w y ↔ x ≤ v g ⁡ y
37 22 36 wa wff f ∈ b a ∧ g ∈ a b ∧ ∀ x ∈ a ∀ y ∈ b f ⁡ x ≤ w y ↔ x ≤ v g ⁡ y
38 37 11 12 copab class f g | f ∈ b a ∧ g ∈ a b ∧ ∀ x ∈ a ∀ y ∈ b f ⁡ x ≤ w y ↔ x ≤ v g ⁡ y
39 10 9 38 csb class ⦋ Base w / b⦌ f g | f ∈ b a ∧ g ∈ a b ∧ ∀ x ∈ a ∀ y ∈ b f ⁡ x ≤ w y ↔ x ≤ v g ⁡ y
40 7 6 39 csb class ⦋ Base v / a⦌ ⦋ Base w / b⦌ f g | f ∈ b a ∧ g ∈ a b ∧ ∀ x ∈ a ∀ y ∈ b f ⁡ x ≤ w y ↔ x ≤ v g ⁡ y
41 1 3 2 2 40 cmpo class v ∈ V , w ∈ V ⟼ ⦋ Base v / a⦌ ⦋ Base w / b⦌ f g | f ∈ b a ∧ g ∈ a b ∧ ∀ x ∈ a ∀ y ∈ b f ⁡ x ≤ w y ↔ x ≤ v g ⁡ y
42 0 41 wceq wff MGalConn = v ∈ V , w ∈ V ⟼ ⦋ Base v / a⦌ ⦋ Base w / b⦌ f g | f ∈ b a ∧ g ∈ a b ∧ ∀ x ∈ a ∀ y ∈ b f ⁡ x ≤ w y ↔ x ≤ v g ⁡ y