Detailed syntax breakdown of Definition df-algext
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | calgext 33698 |
. 2
class
/AlgExt |
| 2 | | ve |
. . . . . 6
setvar 𝑒 |
| 3 | 2 | cv 1540 |
. . . . 5
class 𝑒 |
| 4 | | vf |
. . . . . 6
setvar 𝑓 |
| 5 | 4 | cv 1540 |
. . . . 5
class 𝑓 |
| 6 | | cfldext 33641 |
. . . . 5
class
/FldExt |
| 7 | 3, 5, 6 | wbr 5089 |
. . . 4
wff 𝑒/FldExt𝑓 |
| 8 | | cbs 17112 |
. . . . . . 7
class
Base |
| 9 | 5, 8 | cfv 6477 |
. . . . . 6
class
(Base‘𝑓) |
| 10 | | cirng 33686 |
. . . . . 6
class
IntgRing |
| 11 | 3, 9, 10 | co 7341 |
. . . . 5
class (𝑒 IntgRing (Base‘𝑓)) |
| 12 | 3, 8 | cfv 6477 |
. . . . 5
class
(Base‘𝑒) |
| 13 | 11, 12 | wceq 1541 |
. . . 4
wff (𝑒 IntgRing (Base‘𝑓)) = (Base‘𝑒) |
| 14 | 7, 13 | wa 395 |
. . 3
wff (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing (Base‘𝑓)) = (Base‘𝑒)) |
| 15 | 14, 2, 4 | copab 5151 |
. 2
class
{⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing (Base‘𝑓)) = (Base‘𝑒))} |
| 16 | 1, 15 | wceq 1541 |
1
wff
/AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing (Base‘𝑓)) = (Base‘𝑒))} |
