Step | Hyp | Ref
| Expression |
1 | | cfrmd 18662 |
. 2
class
freeMnd |
2 | | vi |
. . 3
setvar π |
3 | | cvv 3444 |
. . 3
class
V |
4 | | cnx 17070 |
. . . . . 6
class
ndx |
5 | | cbs 17088 |
. . . . . 6
class
Base |
6 | 4, 5 | cfv 6497 |
. . . . 5
class
(Baseβndx) |
7 | 2 | cv 1541 |
. . . . . 6
class π |
8 | 7 | cword 14408 |
. . . . 5
class Word
π |
9 | 6, 8 | cop 4593 |
. . . 4
class
β¨(Baseβndx), Word πβ© |
10 | | cplusg 17138 |
. . . . . 6
class
+g |
11 | 4, 10 | cfv 6497 |
. . . . 5
class
(+gβndx) |
12 | | cconcat 14464 |
. . . . . 6
class
++ |
13 | 8, 8 | cxp 5632 |
. . . . . 6
class (Word
π Γ Word π) |
14 | 12, 13 | cres 5636 |
. . . . 5
class ( ++
βΎ (Word π Γ
Word π)) |
15 | 11, 14 | cop 4593 |
. . . 4
class
β¨(+gβndx), ( ++ βΎ (Word π Γ Word π))β© |
16 | 9, 15 | cpr 4589 |
. . 3
class
{β¨(Baseβndx), Word πβ©, β¨(+gβndx), ( ++
βΎ (Word π Γ
Word π))β©} |
17 | 2, 3, 16 | cmpt 5189 |
. 2
class (π β V β¦
{β¨(Baseβndx), Word πβ©, β¨(+gβndx), ( ++
βΎ (Word π Γ
Word π))β©}) |
18 | 1, 17 | wceq 1542 |
1
wff freeMnd =
(π β V β¦
{β¨(Baseβndx), Word πβ©, β¨(+gβndx), ( ++
βΎ (Word π Γ
Word π))β©}) |