Step | Hyp | Ref
| Expression |
1 | | df-trkg 27444 |
. . . . 5
β’ TarskiG =
((TarskiGC β© TarskiGB) β© (TarskiGCB
β© {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) |
2 | | inss1 4192 |
. . . . . 6
β’
((TarskiGC β© TarskiGB) β©
(TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) β (TarskiGC β©
TarskiGB) |
3 | | inss2 4193 |
. . . . . 6
β’
(TarskiGC β© TarskiGB) β
TarskiGB |
4 | 2, 3 | sstri 3957 |
. . . . 5
β’
((TarskiGC β© TarskiGB) β©
(TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) β
TarskiGB |
5 | 1, 4 | eqsstri 3982 |
. . . 4
β’ TarskiG
β TarskiGB |
6 | | axtrkg.g |
. . . 4
β’ (π β πΊ β TarskiG) |
7 | 5, 6 | sselid 3946 |
. . 3
β’ (π β πΊ β
TarskiGB) |
8 | | axtrkg.p |
. . . . . 6
β’ π = (BaseβπΊ) |
9 | | axtrkg.d |
. . . . . 6
β’ β =
(distβπΊ) |
10 | | axtrkg.i |
. . . . . 6
β’ πΌ = (ItvβπΊ) |
11 | 8, 9, 10 | istrkgb 27446 |
. . . . 5
β’ (πΊ β TarskiGB
β (πΊ β V β§
(βπ₯ β π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦))))) |
12 | 11 | simprbi 498 |
. . . 4
β’ (πΊ β TarskiGB
β (βπ₯ β
π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦)))) |
13 | 12 | simp3d 1145 |
. . 3
β’ (πΊ β TarskiGB
β βπ β
π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦))) |
14 | 7, 13 | syl 17 |
. 2
β’ (π β βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦))) |
15 | | axtgcont.1 |
. . . 4
β’ (π β π β π) |
16 | 8 | fvexi 6860 |
. . . . . 6
β’ π β V |
17 | 16 | ssex 5282 |
. . . . 5
β’ (π β π β π β V) |
18 | | elpwg 4567 |
. . . . 5
β’ (π β V β (π β π« π β π β π)) |
19 | 15, 17, 18 | 3syl 18 |
. . . 4
β’ (π β (π β π« π β π β π)) |
20 | 15, 19 | mpbird 257 |
. . 3
β’ (π β π β π« π) |
21 | | axtgcont.2 |
. . . 4
β’ (π β π β π) |
22 | 16 | ssex 5282 |
. . . . 5
β’ (π β π β π β V) |
23 | | elpwg 4567 |
. . . . 5
β’ (π β V β (π β π« π β π β π)) |
24 | 21, 22, 23 | 3syl 18 |
. . . 4
β’ (π β (π β π« π β π β π)) |
25 | 21, 24 | mpbird 257 |
. . 3
β’ (π β π β π« π) |
26 | | raleq 3308 |
. . . . . 6
β’ (π = π β (βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦))) |
27 | 26 | rexbidv 3172 |
. . . . 5
β’ (π = π β (βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦))) |
28 | | raleq 3308 |
. . . . . 6
β’ (π = π β (βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦) β βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦))) |
29 | 28 | rexbidv 3172 |
. . . . 5
β’ (π = π β (βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦))) |
30 | 27, 29 | imbi12d 345 |
. . . 4
β’ (π = π β ((βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦)) β (βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦)))) |
31 | | raleq 3308 |
. . . . . 6
β’ (π‘ = π β (βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ¦ β π π₯ β (ππΌπ¦))) |
32 | 31 | rexralbidv 3211 |
. . . . 5
β’ (π‘ = π β (βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π π₯ β (ππΌπ¦))) |
33 | | raleq 3308 |
. . . . . 6
β’ (π‘ = π β (βπ¦ β π‘ π β (π₯πΌπ¦) β βπ¦ β π π β (π₯πΌπ¦))) |
34 | 33 | rexralbidv 3211 |
. . . . 5
β’ (π‘ = π β (βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦) β βπ β π βπ₯ β π βπ¦ β π π β (π₯πΌπ¦))) |
35 | 32, 34 | imbi12d 345 |
. . . 4
β’ (π‘ = π β ((βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦)) β (βπ β π βπ₯ β π βπ¦ β π π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π π β (π₯πΌπ¦)))) |
36 | 30, 35 | rspc2v 3592 |
. . 3
β’ ((π β π« π β§ π β π« π) β (βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦)) β (βπ β π βπ₯ β π βπ¦ β π π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π π β (π₯πΌπ¦)))) |
37 | 20, 25, 36 | syl2anc 585 |
. 2
β’ (π β (βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦)) β (βπ β π βπ₯ β π βπ¦ β π π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π π β (π₯πΌπ¦)))) |
38 | 14, 37 | mpd 15 |
1
β’ (π β (βπ β π βπ₯ β π βπ¦ β π π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π π β (π₯πΌπ¦))) |