Step | Hyp | Ref
| Expression |
1 | | df-trkg 27395 |
. . . . 5
β’ TarskiG =
((TarskiGC β© TarskiGB) β© (TarskiGCB
β© {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) |
2 | | inss1 4188 |
. . . . . 6
β’
((TarskiGC β© TarskiGB) β©
(TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) β (TarskiGC β©
TarskiGB) |
3 | | inss2 4189 |
. . . . . 6
β’
(TarskiGC β© TarskiGB) β
TarskiGB |
4 | 2, 3 | sstri 3953 |
. . . . 5
β’
((TarskiGC β© TarskiGB) β©
(TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) β
TarskiGB |
5 | 1, 4 | eqsstri 3978 |
. . . 4
β’ TarskiG
β TarskiGB |
6 | | axtrkg.g |
. . . 4
β’ (π β πΊ β TarskiG) |
7 | 5, 6 | sselid 3942 |
. . 3
β’ (π β πΊ β
TarskiGB) |
8 | | axtrkg.p |
. . . . . 6
β’ π = (BaseβπΊ) |
9 | | axtrkg.d |
. . . . . 6
β’ β =
(distβπΊ) |
10 | | axtrkg.i |
. . . . . 6
β’ πΌ = (ItvβπΊ) |
11 | 8, 9, 10 | istrkgb 27397 |
. . . . 5
β’ (πΊ β TarskiGB
β (πΊ β V β§
(βπ₯ β π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦))))) |
12 | 11 | simprbi 497 |
. . . 4
β’ (πΊ β TarskiGB
β (βπ₯ β
π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦)))) |
13 | 12 | simp1d 1142 |
. . 3
β’ (πΊ β TarskiGB
β βπ₯ β
π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦)) |
14 | 7, 13 | syl 17 |
. 2
β’ (π β βπ₯ β π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦)) |
15 | | axtgbtwnid.3 |
. 2
β’ (π β π β (ππΌπ)) |
16 | | axtgbtwnid.1 |
. . 3
β’ (π β π β π) |
17 | | axtgbtwnid.2 |
. . 3
β’ (π β π β π) |
18 | | id 22 |
. . . . . . 7
β’ (π₯ = π β π₯ = π) |
19 | 18, 18 | oveq12d 7375 |
. . . . . 6
β’ (π₯ = π β (π₯πΌπ₯) = (ππΌπ)) |
20 | 19 | eleq2d 2823 |
. . . . 5
β’ (π₯ = π β (π¦ β (π₯πΌπ₯) β π¦ β (ππΌπ))) |
21 | | eqeq1 2740 |
. . . . 5
β’ (π₯ = π β (π₯ = π¦ β π = π¦)) |
22 | 20, 21 | imbi12d 344 |
. . . 4
β’ (π₯ = π β ((π¦ β (π₯πΌπ₯) β π₯ = π¦) β (π¦ β (ππΌπ) β π = π¦))) |
23 | | eleq1 2825 |
. . . . 5
β’ (π¦ = π β (π¦ β (ππΌπ) β π β (ππΌπ))) |
24 | | eqeq2 2748 |
. . . . 5
β’ (π¦ = π β (π = π¦ β π = π)) |
25 | 23, 24 | imbi12d 344 |
. . . 4
β’ (π¦ = π β ((π¦ β (ππΌπ) β π = π¦) β (π β (ππΌπ) β π = π))) |
26 | 22, 25 | rspc2v 3590 |
. . 3
β’ ((π β π β§ π β π) β (βπ₯ β π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦) β (π β (ππΌπ) β π = π))) |
27 | 16, 17, 26 | syl2anc 584 |
. 2
β’ (π β (βπ₯ β π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦) β (π β (ππΌπ) β π = π))) |
28 | 14, 15, 27 | mp2d 49 |
1
β’ (π β π = π) |