Step | Hyp | Ref
| Expression |
1 | | cidlsrg 32297 |
. 2
class
IDLsrg |
2 | | vr |
. . 3
setvar π |
3 | | cvv 3447 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . 5
class π |
6 | | clidl 20676 |
. . . . 5
class
LIdeal |
7 | 5, 6 | cfv 6500 |
. . . 4
class
(LIdealβπ) |
8 | | cnx 17073 |
. . . . . . . 8
class
ndx |
9 | | cbs 17091 |
. . . . . . . 8
class
Base |
10 | 8, 9 | cfv 6500 |
. . . . . . 7
class
(Baseβndx) |
11 | 4 | cv 1541 |
. . . . . . 7
class π |
12 | 10, 11 | cop 4596 |
. . . . . 6
class
β¨(Baseβndx), πβ© |
13 | | cplusg 17141 |
. . . . . . . 8
class
+g |
14 | 8, 13 | cfv 6500 |
. . . . . . 7
class
(+gβndx) |
15 | | clsm 19424 |
. . . . . . . 8
class
LSSum |
16 | 5, 15 | cfv 6500 |
. . . . . . 7
class
(LSSumβπ) |
17 | 14, 16 | cop 4596 |
. . . . . 6
class
β¨(+gβndx), (LSSumβπ)β© |
18 | | cmulr 17142 |
. . . . . . . 8
class
.r |
19 | 8, 18 | cfv 6500 |
. . . . . . 7
class
(.rβndx) |
20 | | vi |
. . . . . . . 8
setvar π |
21 | | vj |
. . . . . . . 8
setvar π |
22 | 20 | cv 1541 |
. . . . . . . . . 10
class π |
23 | 21 | cv 1541 |
. . . . . . . . . 10
class π |
24 | | cmgp 19904 |
. . . . . . . . . . . 12
class
mulGrp |
25 | 5, 24 | cfv 6500 |
. . . . . . . . . . 11
class
(mulGrpβπ) |
26 | 25, 15 | cfv 6500 |
. . . . . . . . . 10
class
(LSSumβ(mulGrpβπ)) |
27 | 22, 23, 26 | co 7361 |
. . . . . . . . 9
class (π(LSSumβ(mulGrpβπ))π) |
28 | | crsp 20677 |
. . . . . . . . . 10
class
RSpan |
29 | 5, 28 | cfv 6500 |
. . . . . . . . 9
class
(RSpanβπ) |
30 | 27, 29 | cfv 6500 |
. . . . . . . 8
class
((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)) |
31 | 20, 21, 11, 11, 30 | cmpo 7363 |
. . . . . . 7
class (π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π))) |
32 | 19, 31 | cop 4596 |
. . . . . 6
class
β¨(.rβndx), (π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β© |
33 | 12, 17, 32 | ctp 4594 |
. . . . 5
class
{β¨(Baseβndx), πβ©, β¨(+gβndx),
(LSSumβπ)β©,
β¨(.rβndx), (π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β©} |
34 | | cts 17147 |
. . . . . . . 8
class
TopSet |
35 | 8, 34 | cfv 6500 |
. . . . . . 7
class
(TopSetβndx) |
36 | 22, 23 | wss 3914 |
. . . . . . . . . . 11
wff π β π |
37 | 36 | wn 3 |
. . . . . . . . . 10
wff Β¬
π β π |
38 | 37, 21, 11 | crab 3406 |
. . . . . . . . 9
class {π β π β£ Β¬ π β π} |
39 | 20, 11, 38 | cmpt 5192 |
. . . . . . . 8
class (π β π β¦ {π β π β£ Β¬ π β π}) |
40 | 39 | crn 5638 |
. . . . . . 7
class ran
(π β π β¦ {π β π β£ Β¬ π β π}) |
41 | 35, 40 | cop 4596 |
. . . . . 6
class
β¨(TopSetβndx), ran (π β π β¦ {π β π β£ Β¬ π β π})β© |
42 | | cple 17148 |
. . . . . . . 8
class
le |
43 | 8, 42 | cfv 6500 |
. . . . . . 7
class
(leβndx) |
44 | 22, 23 | cpr 4592 |
. . . . . . . . . 10
class {π, π} |
45 | 44, 11 | wss 3914 |
. . . . . . . . 9
wff {π, π} β π |
46 | 45, 36 | wa 397 |
. . . . . . . 8
wff ({π, π} β π β§ π β π) |
47 | 46, 20, 21 | copab 5171 |
. . . . . . 7
class
{β¨π, πβ© β£ ({π, π} β π β§ π β π)} |
48 | 43, 47 | cop 4596 |
. . . . . 6
class
β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β© |
49 | 41, 48 | cpr 4592 |
. . . . 5
class
{β¨(TopSetβndx), ran (π β π β¦ {π β π β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β©} |
50 | 33, 49 | cun 3912 |
. . . 4
class
({β¨(Baseβndx), πβ©, β¨(+gβndx),
(LSSumβπ)β©,
β¨(.rβndx), (π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β π β¦ {π β π β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β©}) |
51 | 4, 7, 50 | csb 3859 |
. . 3
class
β¦(LIdealβπ) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (LSSumβπ)β©, β¨(.rβndx),
(π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β π β¦ {π β π β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β©}) |
52 | 2, 3, 51 | cmpt 5192 |
. 2
class (π β V β¦
β¦(LIdealβπ) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (LSSumβπ)β©, β¨(.rβndx),
(π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β π β¦ {π β π β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β©})) |
53 | 1, 52 | wceq 1542 |
1
wff IDLsrg =
(π β V β¦
β¦(LIdealβπ) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (LSSumβπ)β©, β¨(.rβndx),
(π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β π β¦ {π β π β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β©})) |