Step | Hyp | Ref
| Expression |
1 | | cfldext 32384 |
. 2
class
/FldExt |
2 | | ve |
. . . . . . 7
setvar π |
3 | 2 | cv 1541 |
. . . . . 6
class π |
4 | | cfield 20198 |
. . . . . 6
class
Field |
5 | 3, 4 | wcel 2107 |
. . . . 5
wff π β Field |
6 | | vf |
. . . . . . 7
setvar π |
7 | 6 | cv 1541 |
. . . . . 6
class π |
8 | 7, 4 | wcel 2107 |
. . . . 5
wff π β Field |
9 | 5, 8 | wa 397 |
. . . 4
wff (π β Field β§ π β Field) |
10 | | cbs 17088 |
. . . . . . . 8
class
Base |
11 | 7, 10 | cfv 6497 |
. . . . . . 7
class
(Baseβπ) |
12 | | cress 17117 |
. . . . . . 7
class
βΎs |
13 | 3, 11, 12 | co 7358 |
. . . . . 6
class (π βΎs
(Baseβπ)) |
14 | 7, 13 | wceq 1542 |
. . . . 5
wff π = (π βΎs (Baseβπ)) |
15 | | csubrg 20232 |
. . . . . . 7
class
SubRing |
16 | 3, 15 | cfv 6497 |
. . . . . 6
class
(SubRingβπ) |
17 | 11, 16 | wcel 2107 |
. . . . 5
wff
(Baseβπ)
β (SubRingβπ) |
18 | 14, 17 | wa 397 |
. . . 4
wff (π = (π βΎs (Baseβπ)) β§ (Baseβπ) β (SubRingβπ)) |
19 | 9, 18 | wa 397 |
. . 3
wff ((π β Field β§ π β Field) β§ (π = (π βΎs (Baseβπ)) β§ (Baseβπ) β (SubRingβπ))) |
20 | 19, 2, 6 | copab 5168 |
. 2
class
{β¨π, πβ© β£ ((π β Field β§ π β Field) β§ (π = (π βΎs (Baseβπ)) β§ (Baseβπ) β (SubRingβπ)))} |
21 | 1, 20 | wceq 1542 |
1
wff
/FldExt = {β¨π, πβ© β£ ((π β Field β§ π β Field) β§ (π = (π βΎs (Baseβπ)) β§ (Baseβπ) β (SubRingβπ)))} |