Detailed syntax breakdown of Definition df-trkg
| Step | Hyp | Ref
| Expression |
| 1 | | cstrkg 28435 |
. 2
class
TarskiG |
| 2 | | cstrkgc 28436 |
. . . 4
class
TarskiGC |
| 3 | | cstrkgb 28437 |
. . . 4
class
TarskiGB |
| 4 | 2, 3 | cin 3950 |
. . 3
class
(TarskiGC ∩ TarskiGB) |
| 5 | | cstrkgcb 28438 |
. . . 4
class
TarskiGCB |
| 6 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
| 7 | 6 | cv 1539 |
. . . . . . . . 9
class 𝑓 |
| 8 | | clng 28442 |
. . . . . . . . 9
class
LineG |
| 9 | 7, 8 | cfv 6561 |
. . . . . . . 8
class
(LineG‘𝑓) |
| 10 | | vx |
. . . . . . . . 9
setvar 𝑥 |
| 11 | | vy |
. . . . . . . . 9
setvar 𝑦 |
| 12 | | vp |
. . . . . . . . . 10
setvar 𝑝 |
| 13 | 12 | cv 1539 |
. . . . . . . . 9
class 𝑝 |
| 14 | 10 | cv 1539 |
. . . . . . . . . . 11
class 𝑥 |
| 15 | 14 | csn 4626 |
. . . . . . . . . 10
class {𝑥} |
| 16 | 13, 15 | cdif 3948 |
. . . . . . . . 9
class (𝑝 ∖ {𝑥}) |
| 17 | | vz |
. . . . . . . . . . . . 13
setvar 𝑧 |
| 18 | 17 | cv 1539 |
. . . . . . . . . . . 12
class 𝑧 |
| 19 | 11 | cv 1539 |
. . . . . . . . . . . . 13
class 𝑦 |
| 20 | | vi |
. . . . . . . . . . . . . 14
setvar 𝑖 |
| 21 | 20 | cv 1539 |
. . . . . . . . . . . . 13
class 𝑖 |
| 22 | 14, 19, 21 | co 7431 |
. . . . . . . . . . . 12
class (𝑥𝑖𝑦) |
| 23 | 18, 22 | wcel 2108 |
. . . . . . . . . . 11
wff 𝑧 ∈ (𝑥𝑖𝑦) |
| 24 | 18, 19, 21 | co 7431 |
. . . . . . . . . . . 12
class (𝑧𝑖𝑦) |
| 25 | 14, 24 | wcel 2108 |
. . . . . . . . . . 11
wff 𝑥 ∈ (𝑧𝑖𝑦) |
| 26 | 14, 18, 21 | co 7431 |
. . . . . . . . . . . 12
class (𝑥𝑖𝑧) |
| 27 | 19, 26 | wcel 2108 |
. . . . . . . . . . 11
wff 𝑦 ∈ (𝑥𝑖𝑧) |
| 28 | 23, 25, 27 | w3o 1086 |
. . . . . . . . . 10
wff (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) |
| 29 | 28, 17, 13 | crab 3436 |
. . . . . . . . 9
class {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} |
| 30 | 10, 11, 13, 16, 29 | cmpo 7433 |
. . . . . . . 8
class (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) |
| 31 | 9, 30 | wceq 1540 |
. . . . . . 7
wff
(LineG‘𝑓) =
(𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) |
| 32 | | citv 28441 |
. . . . . . . 8
class
Itv |
| 33 | 7, 32 | cfv 6561 |
. . . . . . 7
class
(Itv‘𝑓) |
| 34 | 31, 20, 33 | wsbc 3788 |
. . . . . 6
wff
[(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) |
| 35 | | cbs 17247 |
. . . . . . 7
class
Base |
| 36 | 7, 35 | cfv 6561 |
. . . . . 6
class
(Base‘𝑓) |
| 37 | 34, 12, 36 | wsbc 3788 |
. . . . 5
wff
[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) |
| 38 | 37, 6 | cab 2714 |
. . . 4
class {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} |
| 39 | 5, 38 | cin 3950 |
. . 3
class
(TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) |
| 40 | 4, 39 | cin 3950 |
. 2
class
((TarskiGC ∩ TarskiGB) ∩
(TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) |
| 41 | 1, 40 | wceq 1540 |
1
wff TarskiG =
((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB
∩ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) |