Detailed syntax breakdown of Definition df-idlsrg
Step | Hyp | Ref
| Expression |
1 | | cidlsrg 31359 |
. 2
class
IDLsrg |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar 𝑏 |
5 | 2 | cv 1542 |
. . . . 5
class 𝑟 |
6 | | clidl 20207 |
. . . . 5
class
LIdeal |
7 | 5, 6 | cfv 6380 |
. . . 4
class
(LIdeal‘𝑟) |
8 | | cnx 16744 |
. . . . . . . 8
class
ndx |
9 | | cbs 16760 |
. . . . . . . 8
class
Base |
10 | 8, 9 | cfv 6380 |
. . . . . . 7
class
(Base‘ndx) |
11 | 4 | cv 1542 |
. . . . . . 7
class 𝑏 |
12 | 10, 11 | cop 4547 |
. . . . . 6
class
〈(Base‘ndx), 𝑏〉 |
13 | | cplusg 16802 |
. . . . . . . 8
class
+g |
14 | 8, 13 | cfv 6380 |
. . . . . . 7
class
(+g‘ndx) |
15 | | clsm 19023 |
. . . . . . . 8
class
LSSum |
16 | 5, 15 | cfv 6380 |
. . . . . . 7
class
(LSSum‘𝑟) |
17 | 14, 16 | cop 4547 |
. . . . . 6
class
〈(+g‘ndx), (LSSum‘𝑟)〉 |
18 | | cmulr 16803 |
. . . . . . . 8
class
.r |
19 | 8, 18 | cfv 6380 |
. . . . . . 7
class
(.r‘ndx) |
20 | | vi |
. . . . . . . 8
setvar 𝑖 |
21 | | vj |
. . . . . . . 8
setvar 𝑗 |
22 | 20 | cv 1542 |
. . . . . . . . . 10
class 𝑖 |
23 | 21 | cv 1542 |
. . . . . . . . . 10
class 𝑗 |
24 | | cmgp 19504 |
. . . . . . . . . . . 12
class
mulGrp |
25 | 5, 24 | cfv 6380 |
. . . . . . . . . . 11
class
(mulGrp‘𝑟) |
26 | 25, 15 | cfv 6380 |
. . . . . . . . . 10
class
(LSSum‘(mulGrp‘𝑟)) |
27 | 22, 23, 26 | co 7213 |
. . . . . . . . 9
class (𝑖(LSSum‘(mulGrp‘𝑟))𝑗) |
28 | | crsp 20208 |
. . . . . . . . . 10
class
RSpan |
29 | 5, 28 | cfv 6380 |
. . . . . . . . 9
class
(RSpan‘𝑟) |
30 | 27, 29 | cfv 6380 |
. . . . . . . 8
class
((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)) |
31 | 20, 21, 11, 11, 30 | cmpo 7215 |
. . . . . . 7
class (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗))) |
32 | 19, 31 | cop 4547 |
. . . . . 6
class
〈(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉 |
33 | 12, 17, 32 | ctp 4545 |
. . . . 5
class
{〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx),
(LSSum‘𝑟)〉,
〈(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉} |
34 | | cts 16808 |
. . . . . . . 8
class
TopSet |
35 | 8, 34 | cfv 6380 |
. . . . . . 7
class
(TopSet‘ndx) |
36 | 22, 23 | wss 3866 |
. . . . . . . . . . 11
wff 𝑖 ⊆ 𝑗 |
37 | 36 | wn 3 |
. . . . . . . . . 10
wff ¬
𝑖 ⊆ 𝑗 |
38 | 37, 21, 11 | crab 3065 |
. . . . . . . . 9
class {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗} |
39 | 20, 11, 38 | cmpt 5135 |
. . . . . . . 8
class (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗}) |
40 | 39 | crn 5552 |
. . . . . . 7
class ran
(𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗}) |
41 | 35, 40 | cop 4547 |
. . . . . 6
class
〈(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉 |
42 | | cple 16809 |
. . . . . . . 8
class
le |
43 | 8, 42 | cfv 6380 |
. . . . . . 7
class
(le‘ndx) |
44 | 22, 23 | cpr 4543 |
. . . . . . . . . 10
class {𝑖, 𝑗} |
45 | 44, 11 | wss 3866 |
. . . . . . . . 9
wff {𝑖, 𝑗} ⊆ 𝑏 |
46 | 45, 36 | wa 399 |
. . . . . . . 8
wff ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗) |
47 | 46, 20, 21 | copab 5115 |
. . . . . . 7
class
{〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)} |
48 | 43, 47 | cop 4547 |
. . . . . 6
class
〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉 |
49 | 41, 48 | cpr 4543 |
. . . . 5
class
{〈(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉} |
50 | 33, 49 | cun 3864 |
. . . 4
class
({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx),
(LSSum‘𝑟)〉,
〈(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉}) |
51 | 4, 7, 50 | csb 3811 |
. . 3
class
⦋(LIdeal‘𝑟) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (LSSum‘𝑟)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉}) |
52 | 2, 3, 51 | cmpt 5135 |
. 2
class (𝑟 ∈ V ↦
⦋(LIdeal‘𝑟) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (LSSum‘𝑟)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉})) |
53 | 1, 52 | wceq 1543 |
1
wff IDLsrg =
(𝑟 ∈ V ↦
⦋(LIdeal‘𝑟) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (LSSum‘𝑟)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉})) |