Step | Hyp | Ref
| Expression |
1 | | axtgpasch.6 |
. 2
β’ (π β π β (ππΌπ)) |
2 | | axtgpasch.7 |
. 2
β’ (π β π β (ππΌπ)) |
3 | | df-trkg 27704 |
. . . . . . 7
β’ TarskiG =
((TarskiGC β© TarskiGB) β© (TarskiGCB
β© {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) |
4 | | inss1 4229 |
. . . . . . . 8
β’
((TarskiGC β© TarskiGB) β©
(TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) β (TarskiGC β©
TarskiGB) |
5 | | inss2 4230 |
. . . . . . . 8
β’
(TarskiGC β© TarskiGB) β
TarskiGB |
6 | 4, 5 | sstri 3992 |
. . . . . . 7
β’
((TarskiGC β© TarskiGB) β©
(TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) β
TarskiGB |
7 | 3, 6 | eqsstri 4017 |
. . . . . 6
β’ TarskiG
β TarskiGB |
8 | | axtrkg.g |
. . . . . 6
β’ (π β πΊ β TarskiG) |
9 | 7, 8 | sselid 3981 |
. . . . 5
β’ (π β πΊ β
TarskiGB) |
10 | | axtrkg.p |
. . . . . . . 8
β’ π = (BaseβπΊ) |
11 | | axtrkg.d |
. . . . . . . 8
β’ β =
(distβπΊ) |
12 | | axtrkg.i |
. . . . . . . 8
β’ πΌ = (ItvβπΊ) |
13 | 10, 11, 12 | istrkgb 27706 |
. . . . . . 7
β’ (πΊ β TarskiGB
β (πΊ β V β§
(βπ₯ β π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦))))) |
14 | 13 | simprbi 498 |
. . . . . 6
β’ (πΊ β TarskiGB
β (βπ₯ β
π βπ¦ β π (π¦ β (π₯πΌπ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (ππΌπ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯πΌπ¦)))) |
15 | 14 | simp2d 1144 |
. . . . 5
β’ (πΊ β TarskiGB
β βπ₯ β
π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯)))) |
16 | 9, 15 | syl 17 |
. . . 4
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯)))) |
17 | | axtgpasch.1 |
. . . . 5
β’ (π β π β π) |
18 | | axtgpasch.2 |
. . . . 5
β’ (π β π β π) |
19 | | axtgpasch.3 |
. . . . 5
β’ (π β π β π) |
20 | | oveq1 7416 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯πΌπ§) = (ππΌπ§)) |
21 | 20 | eleq2d 2820 |
. . . . . . . . 9
β’ (π₯ = π β (π’ β (π₯πΌπ§) β π’ β (ππΌπ§))) |
22 | 21 | anbi1d 631 |
. . . . . . . 8
β’ (π₯ = π β ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β (π’ β (ππΌπ§) β§ π£ β (π¦πΌπ§)))) |
23 | | oveq2 7417 |
. . . . . . . . . . 11
β’ (π₯ = π β (π£πΌπ₯) = (π£πΌπ)) |
24 | 23 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π₯ = π β (π β (π£πΌπ₯) β π β (π£πΌπ))) |
25 | 24 | anbi2d 630 |
. . . . . . . . 9
β’ (π₯ = π β ((π β (π’πΌπ¦) β§ π β (π£πΌπ₯)) β (π β (π’πΌπ¦) β§ π β (π£πΌπ)))) |
26 | 25 | rexbidv 3179 |
. . . . . . . 8
β’ (π₯ = π β (βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ)))) |
27 | 22, 26 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = π β (((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β ((π’ β (ππΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ))))) |
28 | 27 | 2ralbidv 3219 |
. . . . . 6
β’ (π₯ = π β (βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β βπ’ β π βπ£ β π ((π’ β (ππΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ))))) |
29 | | oveq1 7416 |
. . . . . . . . . 10
β’ (π¦ = π β (π¦πΌπ§) = (ππΌπ§)) |
30 | 29 | eleq2d 2820 |
. . . . . . . . 9
β’ (π¦ = π β (π£ β (π¦πΌπ§) β π£ β (ππΌπ§))) |
31 | 30 | anbi2d 630 |
. . . . . . . 8
β’ (π¦ = π β ((π’ β (ππΌπ§) β§ π£ β (π¦πΌπ§)) β (π’ β (ππΌπ§) β§ π£ β (ππΌπ§)))) |
32 | | oveq2 7417 |
. . . . . . . . . . 11
β’ (π¦ = π β (π’πΌπ¦) = (π’πΌπ)) |
33 | 32 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π¦ = π β (π β (π’πΌπ¦) β π β (π’πΌπ))) |
34 | 33 | anbi1d 631 |
. . . . . . . . 9
β’ (π¦ = π β ((π β (π’πΌπ¦) β§ π β (π£πΌπ)) β (π β (π’πΌπ) β§ π β (π£πΌπ)))) |
35 | 34 | rexbidv 3179 |
. . . . . . . 8
β’ (π¦ = π β (βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ)))) |
36 | 31, 35 | imbi12d 345 |
. . . . . . 7
β’ (π¦ = π β (((π’ β (ππΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ))) β ((π’ β (ππΌπ§) β§ π£ β (ππΌπ§)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))))) |
37 | 36 | 2ralbidv 3219 |
. . . . . 6
β’ (π¦ = π β (βπ’ β π βπ£ β π ((π’ β (ππΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ))) β βπ’ β π βπ£ β π ((π’ β (ππΌπ§) β§ π£ β (ππΌπ§)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))))) |
38 | | oveq2 7417 |
. . . . . . . . . 10
β’ (π§ = π β (ππΌπ§) = (ππΌπ)) |
39 | 38 | eleq2d 2820 |
. . . . . . . . 9
β’ (π§ = π β (π’ β (ππΌπ§) β π’ β (ππΌπ))) |
40 | | oveq2 7417 |
. . . . . . . . . 10
β’ (π§ = π β (ππΌπ§) = (ππΌπ)) |
41 | 40 | eleq2d 2820 |
. . . . . . . . 9
β’ (π§ = π β (π£ β (ππΌπ§) β π£ β (ππΌπ))) |
42 | 39, 41 | anbi12d 632 |
. . . . . . . 8
β’ (π§ = π β ((π’ β (ππΌπ§) β§ π£ β (ππΌπ§)) β (π’ β (ππΌπ) β§ π£ β (ππΌπ)))) |
43 | 42 | imbi1d 342 |
. . . . . . 7
β’ (π§ = π β (((π’ β (ππΌπ§) β§ π£ β (ππΌπ§)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))) β ((π’ β (ππΌπ) β§ π£ β (ππΌπ)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))))) |
44 | 43 | 2ralbidv 3219 |
. . . . . 6
β’ (π§ = π β (βπ’ β π βπ£ β π ((π’ β (ππΌπ§) β§ π£ β (ππΌπ§)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))) β βπ’ β π βπ£ β π ((π’ β (ππΌπ) β§ π£ β (ππΌπ)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))))) |
45 | 28, 37, 44 | rspc3v 3628 |
. . . . 5
β’ ((π β π β§ π β π β§ π β π) β (βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β βπ’ β π βπ£ β π ((π’ β (ππΌπ) β§ π£ β (ππΌπ)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))))) |
46 | 17, 18, 19, 45 | syl3anc 1372 |
. . . 4
β’ (π β (βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯πΌπ§) β§ π£ β (π¦πΌπ§)) β βπ β π (π β (π’πΌπ¦) β§ π β (π£πΌπ₯))) β βπ’ β π βπ£ β π ((π’ β (ππΌπ) β§ π£ β (ππΌπ)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))))) |
47 | 16, 46 | mpd 15 |
. . 3
β’ (π β βπ’ β π βπ£ β π ((π’ β (ππΌπ) β§ π£ β (ππΌπ)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ)))) |
48 | | axtgpasch.4 |
. . . 4
β’ (π β π β π) |
49 | | axtgpasch.5 |
. . . 4
β’ (π β π β π) |
50 | | eleq1 2822 |
. . . . . . 7
β’ (π’ = π β (π’ β (ππΌπ) β π β (ππΌπ))) |
51 | 50 | anbi1d 631 |
. . . . . 6
β’ (π’ = π β ((π’ β (ππΌπ) β§ π£ β (ππΌπ)) β (π β (ππΌπ) β§ π£ β (ππΌπ)))) |
52 | | oveq1 7416 |
. . . . . . . . 9
β’ (π’ = π β (π’πΌπ) = (ππΌπ)) |
53 | 52 | eleq2d 2820 |
. . . . . . . 8
β’ (π’ = π β (π β (π’πΌπ) β π β (ππΌπ))) |
54 | 53 | anbi1d 631 |
. . . . . . 7
β’ (π’ = π β ((π β (π’πΌπ) β§ π β (π£πΌπ)) β (π β (ππΌπ) β§ π β (π£πΌπ)))) |
55 | 54 | rexbidv 3179 |
. . . . . 6
β’ (π’ = π β (βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ)) β βπ β π (π β (ππΌπ) β§ π β (π£πΌπ)))) |
56 | 51, 55 | imbi12d 345 |
. . . . 5
β’ (π’ = π β (((π’ β (ππΌπ) β§ π£ β (ππΌπ)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))) β ((π β (ππΌπ) β§ π£ β (ππΌπ)) β βπ β π (π β (ππΌπ) β§ π β (π£πΌπ))))) |
57 | | eleq1 2822 |
. . . . . . 7
β’ (π£ = π β (π£ β (ππΌπ) β π β (ππΌπ))) |
58 | 57 | anbi2d 630 |
. . . . . 6
β’ (π£ = π β ((π β (ππΌπ) β§ π£ β (ππΌπ)) β (π β (ππΌπ) β§ π β (ππΌπ)))) |
59 | | oveq1 7416 |
. . . . . . . . 9
β’ (π£ = π β (π£πΌπ) = (ππΌπ)) |
60 | 59 | eleq2d 2820 |
. . . . . . . 8
β’ (π£ = π β (π β (π£πΌπ) β π β (ππΌπ))) |
61 | 60 | anbi2d 630 |
. . . . . . 7
β’ (π£ = π β ((π β (ππΌπ) β§ π β (π£πΌπ)) β (π β (ππΌπ) β§ π β (ππΌπ)))) |
62 | 61 | rexbidv 3179 |
. . . . . 6
β’ (π£ = π β (βπ β π (π β (ππΌπ) β§ π β (π£πΌπ)) β βπ β π (π β (ππΌπ) β§ π β (ππΌπ)))) |
63 | 58, 62 | imbi12d 345 |
. . . . 5
β’ (π£ = π β (((π β (ππΌπ) β§ π£ β (ππΌπ)) β βπ β π (π β (ππΌπ) β§ π β (π£πΌπ))) β ((π β (ππΌπ) β§ π β (ππΌπ)) β βπ β π (π β (ππΌπ) β§ π β (ππΌπ))))) |
64 | 56, 63 | rspc2v 3623 |
. . . 4
β’ ((π β π β§ π β π) β (βπ’ β π βπ£ β π ((π’ β (ππΌπ) β§ π£ β (ππΌπ)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))) β ((π β (ππΌπ) β§ π β (ππΌπ)) β βπ β π (π β (ππΌπ) β§ π β (ππΌπ))))) |
65 | 48, 49, 64 | syl2anc 585 |
. . 3
β’ (π β (βπ’ β π βπ£ β π ((π’ β (ππΌπ) β§ π£ β (ππΌπ)) β βπ β π (π β (π’πΌπ) β§ π β (π£πΌπ))) β ((π β (ππΌπ) β§ π β (ππΌπ)) β βπ β π (π β (ππΌπ) β§ π β (ππΌπ))))) |
66 | 47, 65 | mpd 15 |
. 2
β’ (π β ((π β (ππΌπ) β§ π β (ππΌπ)) β βπ β π (π β (ππΌπ) β§ π β (ππΌπ)))) |
67 | 1, 2, 66 | mp2and 698 |
1
β’ (π β βπ β π (π β (ππΌπ) β§ π β (ππΌπ))) |