Step | Hyp | Ref
| Expression |
1 | | cefmnd 18679 |
. 2
class
EndoFMnd |
2 | | vx |
. . 3
setvar π₯ |
3 | | cvv 3446 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . 5
class π₯ |
6 | | cmap 8766 |
. . . . 5
class
βm |
7 | 5, 5, 6 | co 7358 |
. . . 4
class (π₯ βm π₯) |
8 | | cnx 17066 |
. . . . . . 7
class
ndx |
9 | | cbs 17084 |
. . . . . . 7
class
Base |
10 | 8, 9 | cfv 6497 |
. . . . . 6
class
(Baseβndx) |
11 | 4 | cv 1541 |
. . . . . 6
class π |
12 | 10, 11 | cop 4593 |
. . . . 5
class
β¨(Baseβndx), πβ© |
13 | | cplusg 17134 |
. . . . . . 7
class
+g |
14 | 8, 13 | cfv 6497 |
. . . . . 6
class
(+gβndx) |
15 | | vf |
. . . . . . 7
setvar π |
16 | | vg |
. . . . . . 7
setvar π |
17 | 15 | cv 1541 |
. . . . . . . 8
class π |
18 | 16 | cv 1541 |
. . . . . . . 8
class π |
19 | 17, 18 | ccom 5638 |
. . . . . . 7
class (π β π) |
20 | 15, 16, 11, 11, 19 | cmpo 7360 |
. . . . . 6
class (π β π, π β π β¦ (π β π)) |
21 | 14, 20 | cop 4593 |
. . . . 5
class
β¨(+gβndx), (π β π, π β π β¦ (π β π))β© |
22 | | cts 17140 |
. . . . . . 7
class
TopSet |
23 | 8, 22 | cfv 6497 |
. . . . . 6
class
(TopSetβndx) |
24 | 5 | cpw 4561 |
. . . . . . . . 9
class π«
π₯ |
25 | 24 | csn 4587 |
. . . . . . . 8
class
{π« π₯} |
26 | 5, 25 | cxp 5632 |
. . . . . . 7
class (π₯ Γ {π« π₯}) |
27 | | cpt 17321 |
. . . . . . 7
class
βt |
28 | 26, 27 | cfv 6497 |
. . . . . 6
class
(βtβ(π₯ Γ {π« π₯})) |
29 | 23, 28 | cop 4593 |
. . . . 5
class
β¨(TopSetβndx), (βtβ(π₯ Γ {π« π₯}))β© |
30 | 12, 21, 29 | ctp 4591 |
. . . 4
class
{β¨(Baseβndx), πβ©, β¨(+gβndx),
(π β π, π β π β¦ (π β π))β©, β¨(TopSetβndx),
(βtβ(π₯ Γ {π« π₯}))β©} |
31 | 4, 7, 30 | csb 3856 |
. . 3
class
β¦(π₯
βm π₯) /
πβ¦{β¨(Baseβndx), πβ©,
β¨(+gβndx), (π β π, π β π β¦ (π β π))β©, β¨(TopSetβndx),
(βtβ(π₯ Γ {π« π₯}))β©} |
32 | 2, 3, 31 | cmpt 5189 |
. 2
class (π₯ β V β¦
β¦(π₯
βm π₯) /
πβ¦{β¨(Baseβndx), πβ©,
β¨(+gβndx), (π β π, π β π β¦ (π β π))β©, β¨(TopSetβndx),
(βtβ(π₯ Γ {π« π₯}))β©}) |
33 | 1, 32 | wceq 1542 |
1
wff EndoFMnd =
(π₯ β V β¦
β¦(π₯
βm π₯) /
πβ¦{β¨(Baseβndx), πβ©,
β¨(+gβndx), (π β π, π β π β¦ (π β π))β©, β¨(TopSetβndx),
(βtβ(π₯ Γ {π« π₯}))β©}) |