Detailed syntax breakdown of Definition df-mgc
Step | Hyp | Ref
| Expression |
1 | | cmgc 30768 |
. 2
class
MGalConn |
2 | | vv |
. . 3
setvar 𝑣 |
3 | | vw |
. . 3
setvar 𝑤 |
4 | | cvv 3407 |
. . 3
class
V |
5 | | va |
. . . 4
setvar 𝑎 |
6 | 2 | cv 1538 |
. . . . 5
class 𝑣 |
7 | | cbs 16526 |
. . . . 5
class
Base |
8 | 6, 7 | cfv 6328 |
. . . 4
class
(Base‘𝑣) |
9 | | vb |
. . . . 5
setvar 𝑏 |
10 | 3 | cv 1538 |
. . . . . 6
class 𝑤 |
11 | 10, 7 | cfv 6328 |
. . . . 5
class
(Base‘𝑤) |
12 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
13 | 12 | cv 1538 |
. . . . . . . . 9
class 𝑓 |
14 | 9 | cv 1538 |
. . . . . . . . . 10
class 𝑏 |
15 | 5 | cv 1538 |
. . . . . . . . . 10
class 𝑎 |
16 | | cmap 8409 |
. . . . . . . . . 10
class
↑m |
17 | 14, 15, 16 | co 7143 |
. . . . . . . . 9
class (𝑏 ↑m 𝑎) |
18 | 13, 17 | wcel 2112 |
. . . . . . . 8
wff 𝑓 ∈ (𝑏 ↑m 𝑎) |
19 | | vg |
. . . . . . . . . 10
setvar 𝑔 |
20 | 19 | cv 1538 |
. . . . . . . . 9
class 𝑔 |
21 | 15, 14, 16 | co 7143 |
. . . . . . . . 9
class (𝑎 ↑m 𝑏) |
22 | 20, 21 | wcel 2112 |
. . . . . . . 8
wff 𝑔 ∈ (𝑎 ↑m 𝑏) |
23 | 18, 22 | wa 400 |
. . . . . . 7
wff (𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) |
24 | | vx |
. . . . . . . . . . . . 13
setvar 𝑥 |
25 | 24 | cv 1538 |
. . . . . . . . . . . 12
class 𝑥 |
26 | 25, 13 | cfv 6328 |
. . . . . . . . . . 11
class (𝑓‘𝑥) |
27 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
28 | 27 | cv 1538 |
. . . . . . . . . . 11
class 𝑦 |
29 | | cple 16615 |
. . . . . . . . . . . 12
class
le |
30 | 10, 29 | cfv 6328 |
. . . . . . . . . . 11
class
(le‘𝑤) |
31 | 26, 28, 30 | wbr 5025 |
. . . . . . . . . 10
wff (𝑓‘𝑥)(le‘𝑤)𝑦 |
32 | 28, 20 | cfv 6328 |
. . . . . . . . . . 11
class (𝑔‘𝑦) |
33 | 6, 29 | cfv 6328 |
. . . . . . . . . . 11
class
(le‘𝑣) |
34 | 25, 32, 33 | wbr 5025 |
. . . . . . . . . 10
wff 𝑥(le‘𝑣)(𝑔‘𝑦) |
35 | 31, 34 | wb 209 |
. . . . . . . . 9
wff ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)) |
36 | 35, 27, 14 | wral 3068 |
. . . . . . . 8
wff
∀𝑦 ∈
𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)) |
37 | 36, 24, 15 | wral 3068 |
. . . . . . 7
wff
∀𝑥 ∈
𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)) |
38 | 23, 37 | wa 400 |
. . . . . 6
wff ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦))) |
39 | 38, 12, 19 | copab 5087 |
. . . . 5
class
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))} |
40 | 9, 11, 39 | csb 3801 |
. . . 4
class
⦋(Base‘𝑤) / 𝑏⦌{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))} |
41 | 5, 8, 40 | csb 3801 |
. . 3
class
⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))} |
42 | 2, 3, 4, 4, 41 | cmpo 7145 |
. 2
class (𝑣 ∈ V, 𝑤 ∈ V ↦
⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))}) |
43 | 1, 42 | wceq 1539 |
1
wff MGalConn =
(𝑣 ∈ V, 𝑤 ∈ V ↦
⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))}) |