Step | Hyp | Ref
| Expression |
1 | | fvexd 6900 |
. . . . . 6
β’ (π β β β
(EEGβπ) β
V) |
2 | | simpl 482 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β π β β) |
3 | | simprl 768 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β π₯ β (Baseβ(EEGβπ))) |
4 | | eengbas 28747 |
. . . . . . . . . . 11
β’ (π β β β
(πΌβπ) =
(Baseβ(EEGβπ))) |
5 | 4 | adantr 480 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (πΌβπ) = (Baseβ(EEGβπ))) |
6 | 3, 5 | eleqtrrd 2830 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β π₯ β (πΌβπ)) |
7 | | simprr 770 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β π¦ β (Baseβ(EEGβπ))) |
8 | 7, 5 | eleqtrrd 2830 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β π¦ β (πΌβπ)) |
9 | | axcgrrflx 28680 |
. . . . . . . . 9
β’ ((π β β β§ π₯ β (πΌβπ) β§ π¦ β (πΌβπ)) β β¨π₯, π¦β©Cgrβ¨π¦, π₯β©) |
10 | 2, 6, 8, 9 | syl3anc 1368 |
. . . . . . . 8
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β β¨π₯, π¦β©Cgrβ¨π¦, π₯β©) |
11 | | eqid 2726 |
. . . . . . . . 9
β’
(Baseβ(EEGβπ)) = (Baseβ(EEGβπ)) |
12 | | eqid 2726 |
. . . . . . . . 9
β’
(distβ(EEGβπ)) = (distβ(EEGβπ)) |
13 | 2, 11, 12, 3, 7, 7,
3 | ecgrtg 28749 |
. . . . . . . 8
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (β¨π₯, π¦β©Cgrβ¨π¦, π₯β© β (π₯(distβ(EEGβπ))π¦) = (π¦(distβ(EEGβπ))π₯))) |
14 | 10, 13 | mpbid 231 |
. . . . . . 7
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (π₯(distβ(EEGβπ))π¦) = (π¦(distβ(EEGβπ))π₯)) |
15 | 14 | ralrimivva 3194 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))(π₯(distβ(EEGβπ))π¦) = (π¦(distβ(EEGβπ))π₯)) |
16 | | simpl 482 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π β β) |
17 | | simpr1 1191 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π₯ β (Baseβ(EEGβπ))) |
18 | | simpr2 1192 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π¦ β (Baseβ(EEGβπ))) |
19 | | simpr3 1193 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π§ β (Baseβ(EEGβπ))) |
20 | 16, 11, 12, 17, 18, 19, 19 | ecgrtg 28749 |
. . . . . . . 8
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β (β¨π₯, π¦β©Cgrβ¨π§, π§β© β (π₯(distβ(EEGβπ))π¦) = (π§(distβ(EEGβπ))π§))) |
21 | 6 | 3adantr3 1168 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π₯ β (πΌβπ)) |
22 | 8 | 3adantr3 1168 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π¦ β (πΌβπ)) |
23 | 4 | adantr 480 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β (πΌβπ) = (Baseβ(EEGβπ))) |
24 | 19, 23 | eleqtrrd 2830 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π§ β (πΌβπ)) |
25 | | axcgrid 28682 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β (β¨π₯, π¦β©Cgrβ¨π§, π§β© β π₯ = π¦)) |
26 | 16, 21, 22, 24, 25 | syl13anc 1369 |
. . . . . . . 8
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β (β¨π₯, π¦β©Cgrβ¨π§, π§β© β π₯ = π¦)) |
27 | 20, 26 | sylbird 260 |
. . . . . . 7
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β ((π₯(distβ(EEGβπ))π¦) = (π§(distβ(EEGβπ))π§) β π₯ = π¦)) |
28 | 27 | ralrimivvva 3197 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))((π₯(distβ(EEGβπ))π¦) = (π§(distβ(EEGβπ))π§) β π₯ = π¦)) |
29 | 1, 15, 28 | jca32 515 |
. . . . 5
β’ (π β β β
((EEGβπ) β V
β§ (βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))(π₯(distβ(EEGβπ))π¦) = (π¦(distβ(EEGβπ))π₯) β§ βπ₯ β (Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))((π₯(distβ(EEGβπ))π¦) = (π§(distβ(EEGβπ))π§) β π₯ = π¦)))) |
30 | | eqid 2726 |
. . . . . 6
β’
(Itvβ(EEGβπ)) = (Itvβ(EEGβπ)) |
31 | 11, 12, 30 | istrkgc 28213 |
. . . . 5
β’
((EEGβπ)
β TarskiGC β ((EEGβπ) β V β§ (βπ₯ β (Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))(π₯(distβ(EEGβπ))π¦) = (π¦(distβ(EEGβπ))π₯) β§ βπ₯ β (Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))((π₯(distβ(EEGβπ))π¦) = (π§(distβ(EEGβπ))π§) β π₯ = π¦)))) |
32 | 29, 31 | sylibr 233 |
. . . 4
β’ (π β β β
(EEGβπ) β
TarskiGC) |
33 | 2, 11, 30, 3, 3, 7 | ebtwntg 28748 |
. . . . . . . . . . 11
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (π¦ Btwn β¨π₯, π₯β© β π¦ β (π₯(Itvβ(EEGβπ))π₯))) |
34 | | axbtwnid 28705 |
. . . . . . . . . . . 12
β’ ((π β β β§ π¦ β (πΌβπ) β§ π₯ β (πΌβπ)) β (π¦ Btwn β¨π₯, π₯β© β π¦ = π₯)) |
35 | 2, 8, 6, 34 | syl3anc 1368 |
. . . . . . . . . . 11
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (π¦ Btwn β¨π₯, π₯β© β π¦ = π₯)) |
36 | 33, 35 | sylbird 260 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (π¦ β (π₯(Itvβ(EEGβπ))π₯) β π¦ = π₯)) |
37 | 36 | imp 406 |
. . . . . . . . 9
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ π¦ β (π₯(Itvβ(EEGβπ))π₯)) β π¦ = π₯) |
38 | 37 | equcomd 2014 |
. . . . . . . 8
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ π¦ β (π₯(Itvβ(EEGβπ))π₯)) β π₯ = π¦) |
39 | 38 | ex 412 |
. . . . . . 7
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (π¦ β (π₯(Itvβ(EEGβπ))π₯) β π₯ = π¦)) |
40 | 39 | ralrimivva 3194 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π₯) β π₯ = π¦)) |
41 | | simpll 764 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β β) |
42 | 6 | adantr 480 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π₯ β (πΌβπ)) |
43 | 8 | adantr 480 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π¦ β (πΌβπ)) |
44 | 3 | adantr 480 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π₯ β (Baseβ(EEGβπ))) |
45 | 7 | adantr 480 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π¦ β (Baseβ(EEGβπ))) |
46 | | simpr1 1191 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π§ β (Baseβ(EEGβπ))) |
47 | 41, 44, 45, 46, 24 | syl13anc 1369 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π§ β (πΌβπ)) |
48 | | simpr2 1192 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π’ β (Baseβ(EEGβπ))) |
49 | 41, 4 | syl 17 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β
(πΌβπ) =
(Baseβ(EEGβπ))) |
50 | 48, 49 | eleqtrrd 2830 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π’ β (πΌβπ)) |
51 | | simpr3 1193 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π£ β (Baseβ(EEGβπ))) |
52 | 51, 49 | eleqtrrd 2830 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π£ β (πΌβπ)) |
53 | | axpasch 28707 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ) β§ π§ β (πΌβπ)) β§ (π’ β (πΌβπ) β§ π£ β (πΌβπ))) β ((π’ Btwn β¨π₯, π§β© β§ π£ Btwn β¨π¦, π§β©) β βπ β (πΌβπ)(π Btwn β¨π’, π¦β© β§ π Btwn β¨π£, π₯β©))) |
54 | 41, 42, 43, 47, 50, 52, 53 | syl132anc 1385 |
. . . . . . . . 9
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β ((π’ Btwn β¨π₯, π§β© β§ π£ Btwn β¨π¦, π§β©) β βπ β (πΌβπ)(π Btwn β¨π’, π¦β© β§ π Btwn β¨π£, π₯β©))) |
55 | 41, 11, 30, 44, 46, 48 | ebtwntg 28748 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (π’ Btwn β¨π₯, π§β© β π’ β (π₯(Itvβ(EEGβπ))π§))) |
56 | 41, 11, 30, 45, 46, 51 | ebtwntg 28748 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (π£ Btwn β¨π¦, π§β© β π£ β (π¦(Itvβ(EEGβπ))π§))) |
57 | 55, 56 | anbi12d 630 |
. . . . . . . . 9
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β ((π’ Btwn β¨π₯, π§β© β§ π£ Btwn β¨π¦, π§β©) β (π’ β (π₯(Itvβ(EEGβπ))π§) β§ π£ β (π¦(Itvβ(EEGβπ))π§)))) |
58 | | simplll 772 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π β β) |
59 | 48 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π’ β (Baseβ(EEGβπ))) |
60 | 45 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π¦ β (Baseβ(EEGβπ))) |
61 | | simpr 484 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π β (πΌβπ)) |
62 | 49 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β (πΌβπ) = (Baseβ(EEGβπ))) |
63 | 61, 62 | eleqtrd 2829 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π β (Baseβ(EEGβπ))) |
64 | 58, 11, 30, 59, 60, 63 | ebtwntg 28748 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β (π Btwn β¨π’, π¦β© β π β (π’(Itvβ(EEGβπ))π¦))) |
65 | 51 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π£ β (Baseβ(EEGβπ))) |
66 | 44 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π₯ β (Baseβ(EEGβπ))) |
67 | 58, 11, 30, 65, 66, 63 | ebtwntg 28748 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β (π Btwn β¨π£, π₯β© β π β (π£(Itvβ(EEGβπ))π₯))) |
68 | 64, 67 | anbi12d 630 |
. . . . . . . . . 10
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β ((π Btwn β¨π’, π¦β© β§ π Btwn β¨π£, π₯β©) β (π β (π’(Itvβ(EEGβπ))π¦) β§ π β (π£(Itvβ(EEGβπ))π₯)))) |
69 | 49, 68 | rexeqbidva 3322 |
. . . . . . . . 9
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (βπ β (πΌβπ)(π Btwn β¨π’, π¦β© β§ π Btwn β¨π£, π₯β©) β βπ β (Baseβ(EEGβπ))(π β (π’(Itvβ(EEGβπ))π¦) β§ π β (π£(Itvβ(EEGβπ))π₯)))) |
70 | 54, 57, 69 | 3imtr3d 293 |
. . . . . . . 8
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β ((π’ β (π₯(Itvβ(EEGβπ))π§) β§ π£ β (π¦(Itvβ(EEGβπ))π§)) β βπ β (Baseβ(EEGβπ))(π β (π’(Itvβ(EEGβπ))π¦) β§ π β (π£(Itvβ(EEGβπ))π₯)))) |
71 | 70 | ralrimivvva 3197 |
. . . . . . 7
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β βπ§ β (Baseβ(EEGβπ))βπ’ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))((π’ β (π₯(Itvβ(EEGβπ))π§) β§ π£ β (π¦(Itvβ(EEGβπ))π§)) β βπ β (Baseβ(EEGβπ))(π β (π’(Itvβ(EEGβπ))π¦) β§ π β (π£(Itvβ(EEGβπ))π₯)))) |
72 | 71 | ralrimivva 3194 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))βπ’ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))((π’ β (π₯(Itvβ(EEGβπ))π§) β§ π£ β (π¦(Itvβ(EEGβπ))π§)) β βπ β (Baseβ(EEGβπ))(π β (π’(Itvβ(EEGβπ))π¦) β§ π β (π£(Itvβ(EEGβπ))π₯)))) |
73 | | simpl 482 |
. . . . . . . . 9
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β π β β) |
74 | | elpwi 4604 |
. . . . . . . . . . 11
β’ (π β π«
(Baseβ(EEGβπ))
β π β
(Baseβ(EEGβπ))) |
75 | 74 | ad2antrl 725 |
. . . . . . . . . 10
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
76 | 4 | adantr 480 |
. . . . . . . . . 10
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β (πΌβπ) = (Baseβ(EEGβπ))) |
77 | 75, 76 | sseqtrrd 4018 |
. . . . . . . . 9
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β π β (πΌβπ)) |
78 | | elpwi 4604 |
. . . . . . . . . . 11
β’ (π‘ β π«
(Baseβ(EEGβπ))
β π‘ β
(Baseβ(EEGβπ))) |
79 | 78 | ad2antll 726 |
. . . . . . . . . 10
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β π‘ β (Baseβ(EEGβπ))) |
80 | 79, 76 | sseqtrrd 4018 |
. . . . . . . . 9
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β π‘ β (πΌβπ)) |
81 | | simpll 764 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) β π β β) |
82 | | simplrl 774 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) β π β (πΌβπ)) |
83 | | simplrr 775 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) β π‘ β (πΌβπ)) |
84 | | simpr 484 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) β βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) |
85 | | axcont 28742 |
. . . . . . . . . . 11
β’ ((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©)) β βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β©) |
86 | 81, 82, 83, 84, 85 | syl13anc 1369 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) β βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β©) |
87 | 86 | ex 412 |
. . . . . . . . 9
β’ ((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β (βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β© β βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β©)) |
88 | 73, 77, 80, 87 | syl12anc 834 |
. . . . . . . 8
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β (βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β© β βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β©)) |
89 | | simplll 772 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β β) |
90 | | simplr 766 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (πΌβπ)) |
91 | 76 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β (πΌβπ) = (Baseβ(EEGβπ))) |
92 | 90, 91 | eleqtrd 2829 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (Baseβ(EEGβπ))) |
93 | 79 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π‘ β (Baseβ(EEGβπ))) |
94 | | simprr 770 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π¦ β π‘) |
95 | 93, 94 | sseldd 3978 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π¦ β (Baseβ(EEGβπ))) |
96 | 75 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (Baseβ(EEGβπ))) |
97 | | simprl 768 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π₯ β π ) |
98 | 96, 97 | sseldd 3978 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π₯ β (Baseβ(EEGβπ))) |
99 | 89, 11, 30, 92, 95, 98 | ebtwntg 28748 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β (π₯ Btwn β¨π, π¦β© β π₯ β (π(Itvβ(EEGβπ))π¦))) |
100 | 99 | 2ralbidva 3210 |
. . . . . . . . 9
β’ (((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β (βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β© β βπ₯ β π βπ¦ β π‘ π₯ β (π(Itvβ(EEGβπ))π¦))) |
101 | 76, 100 | rexeqbidva 3322 |
. . . . . . . 8
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β (βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β© β βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π₯ β (π(Itvβ(EEGβπ))π¦))) |
102 | | simplll 772 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β β) |
103 | 75 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (Baseβ(EEGβπ))) |
104 | | simprl 768 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π₯ β π ) |
105 | 103, 104 | sseldd 3978 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π₯ β (Baseβ(EEGβπ))) |
106 | 79 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π‘ β (Baseβ(EEGβπ))) |
107 | | simprr 770 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π¦ β π‘) |
108 | 106, 107 | sseldd 3978 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π¦ β (Baseβ(EEGβπ))) |
109 | | simplr 766 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (πΌβπ)) |
110 | 76 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β (πΌβπ) = (Baseβ(EEGβπ))) |
111 | 109, 110 | eleqtrd 2829 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (Baseβ(EEGβπ))) |
112 | 102, 11, 30, 105, 108, 111 | ebtwntg 28748 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β (π Btwn β¨π₯, π¦β© β π β (π₯(Itvβ(EEGβπ))π¦))) |
113 | 112 | 2ralbidva 3210 |
. . . . . . . . 9
β’ (((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β (βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β© β βπ₯ β π βπ¦ β π‘ π β (π₯(Itvβ(EEGβπ))π¦))) |
114 | 76, 113 | rexeqbidva 3322 |
. . . . . . . 8
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β (βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β© β βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π β (π₯(Itvβ(EEGβπ))π¦))) |
115 | 88, 101, 114 | 3imtr3d 293 |
. . . . . . 7
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β (βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π₯ β (π(Itvβ(EEGβπ))π¦) β βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π β (π₯(Itvβ(EEGβπ))π¦))) |
116 | 115 | ralrimivva 3194 |
. . . . . 6
β’ (π β β β
βπ β π«
(Baseβ(EEGβπ))βπ‘ β π«
(Baseβ(EEGβπ))(βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π₯ β (π(Itvβ(EEGβπ))π¦) β βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π β (π₯(Itvβ(EEGβπ))π¦))) |
117 | 40, 72, 116 | 3jca 1125 |
. . . . 5
β’ (π β β β
(βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π₯) β π₯ = π¦) β§ βπ₯ β (Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))βπ’ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))((π’ β (π₯(Itvβ(EEGβπ))π§) β§ π£ β (π¦(Itvβ(EEGβπ))π§)) β βπ β (Baseβ(EEGβπ))(π β (π’(Itvβ(EEGβπ))π¦) β§ π β (π£(Itvβ(EEGβπ))π₯))) β§ βπ β π«
(Baseβ(EEGβπ))βπ‘ β π«
(Baseβ(EEGβπ))(βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π₯ β (π(Itvβ(EEGβπ))π¦) β βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π β (π₯(Itvβ(EEGβπ))π¦)))) |
118 | 11, 12, 30 | istrkgb 28214 |
. . . . 5
β’
((EEGβπ)
β TarskiGB β ((EEGβπ) β V β§ (βπ₯ β (Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π₯) β π₯ = π¦) β§ βπ₯ β (Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))βπ’ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))((π’ β (π₯(Itvβ(EEGβπ))π§) β§ π£ β (π¦(Itvβ(EEGβπ))π§)) β βπ β (Baseβ(EEGβπ))(π β (π’(Itvβ(EEGβπ))π¦) β§ π β (π£(Itvβ(EEGβπ))π₯))) β§ βπ β π«
(Baseβ(EEGβπ))βπ‘ β π«
(Baseβ(EEGβπ))(βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π₯ β (π(Itvβ(EEGβπ))π¦) β βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π β (π₯(Itvβ(EEGβπ))π¦))))) |
119 | 1, 117, 118 | sylanbrc 582 |
. . . 4
β’ (π β β β
(EEGβπ) β
TarskiGB) |
120 | 32, 119 | elind 4189 |
. . 3
β’ (π β β β
(EEGβπ) β
(TarskiGC β© TarskiGB)) |
121 | | simplll 772 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β β) |
122 | 3 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π₯ β (Baseβ(EEGβπ))) |
123 | 121, 4 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β
(πΌβπ) =
(Baseβ(EEGβπ))) |
124 | 122, 123 | eleqtrrd 2830 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π₯ β (πΌβπ)) |
125 | 7 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π¦ β (Baseβ(EEGβπ))) |
126 | 125, 123 | eleqtrrd 2830 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π¦ β (πΌβπ)) |
127 | | simplr1 1212 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π§ β (Baseβ(EEGβπ))) |
128 | 127, 123 | eleqtrrd 2830 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π§ β (πΌβπ)) |
129 | | simplr2 1213 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π’ β (Baseβ(EEGβπ))) |
130 | 129, 123 | eleqtrrd 2830 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π’ β (πΌβπ)) |
131 | | simplr3 1214 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
132 | 131, 123 | eleqtrrd 2830 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (πΌβπ)) |
133 | | simpr1 1191 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
134 | 133, 123 | eleqtrrd 2830 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (πΌβπ)) |
135 | | simpr2 1192 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
136 | 135, 123 | eleqtrrd 2830 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (πΌβπ)) |
137 | | simpr3 1193 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π£ β (Baseβ(EEGβπ))) |
138 | 137, 123 | eleqtrrd 2830 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π£ β (πΌβπ)) |
139 | | 3anass 1092 |
. . . . . . . . . . . 12
β’ (((π₯ β π¦ β§ π¦ Btwn β¨π₯, π§β© β§ π Btwn β¨π, πβ©) β§ (β¨π₯, π¦β©Cgrβ¨π, πβ© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β§ (β¨π₯, π’β©Cgrβ¨π, π£β© β§ β¨π¦, π’β©Cgrβ¨π, π£β©)) β ((π₯ β π¦ β§ π¦ Btwn β¨π₯, π§β© β§ π Btwn β¨π, πβ©) β§ ((β¨π₯, π¦β©Cgrβ¨π, πβ© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β§ (β¨π₯, π’β©Cgrβ¨π, π£β© β§ β¨π¦, π’β©Cgrβ¨π, π£β©)))) |
140 | | ax5seg 28704 |
. . . . . . . . . . . 12
β’ (((π β β β§ π₯ β (πΌβπ) β§ π¦ β (πΌβπ)) β§ (π§ β (πΌβπ) β§ π’ β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π£ β (πΌβπ))) β (((π₯ β π¦ β§ π¦ Btwn β¨π₯, π§β© β§ π Btwn β¨π, πβ©) β§ (β¨π₯, π¦β©Cgrβ¨π, πβ© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β§ (β¨π₯, π’β©Cgrβ¨π, π£β© β§ β¨π¦, π’β©Cgrβ¨π, π£β©)) β β¨π§, π’β©Cgrβ¨π, π£β©)) |
141 | 139, 140 | biimtrrid 242 |
. . . . . . . . . . 11
β’ (((π β β β§ π₯ β (πΌβπ) β§ π¦ β (πΌβπ)) β§ (π§ β (πΌβπ) β§ π’ β (πΌβπ) β§ π β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π£ β (πΌβπ))) β (((π₯ β π¦ β§ π¦ Btwn β¨π₯, π§β© β§ π Btwn β¨π, πβ©) β§ ((β¨π₯, π¦β©Cgrβ¨π, πβ© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β§ (β¨π₯, π’β©Cgrβ¨π, π£β© β§ β¨π¦, π’β©Cgrβ¨π, π£β©))) β β¨π§, π’β©Cgrβ¨π, π£β©)) |
142 | 121, 124,
126, 128, 130, 132, 134, 136, 138, 141 | syl333anc 1399 |
. . . . . . . . . 10
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (((π₯ β π¦ β§ π¦ Btwn β¨π₯, π§β© β§ π Btwn β¨π, πβ©) β§ ((β¨π₯, π¦β©Cgrβ¨π, πβ© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β§ (β¨π₯, π’β©Cgrβ¨π, π£β© β§ β¨π¦, π’β©Cgrβ¨π, π£β©))) β β¨π§, π’β©Cgrβ¨π, π£β©)) |
143 | 121, 11, 30, 122, 127, 125 | ebtwntg 28748 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (π¦ Btwn β¨π₯, π§β© β π¦ β (π₯(Itvβ(EEGβπ))π§))) |
144 | 121, 11, 30, 131, 135, 133 | ebtwntg 28748 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (π Btwn β¨π, πβ© β π β (π(Itvβ(EEGβπ))π))) |
145 | 143, 144 | 3anbi23d 1435 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β ((π₯ β π¦ β§ π¦ Btwn β¨π₯, π§β© β§ π Btwn β¨π, πβ©) β (π₯ β π¦ β§ π¦ β (π₯(Itvβ(EEGβπ))π§) β§ π β (π(Itvβ(EEGβπ))π)))) |
146 | 121, 11, 12, 122, 125, 131, 133 | ecgrtg 28749 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (β¨π₯, π¦β©Cgrβ¨π, πβ© β (π₯(distβ(EEGβπ))π¦) = (π(distβ(EEGβπ))π))) |
147 | 121, 11, 12, 125, 127, 133, 135 | ecgrtg 28749 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (β¨π¦, π§β©Cgrβ¨π, πβ© β (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π))) |
148 | 146, 147 | anbi12d 630 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β ((β¨π₯, π¦β©Cgrβ¨π, πβ© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β ((π₯(distβ(EEGβπ))π¦) = (π(distβ(EEGβπ))π) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)))) |
149 | 121, 11, 12, 122, 129, 131, 137 | ecgrtg 28749 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (β¨π₯, π’β©Cgrβ¨π, π£β© β (π₯(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£))) |
150 | 121, 11, 12, 125, 129, 133, 137 | ecgrtg 28749 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (β¨π¦, π’β©Cgrβ¨π, π£β© β (π¦(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£))) |
151 | 149, 150 | anbi12d 630 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β ((β¨π₯, π’β©Cgrβ¨π, π£β© β§ β¨π¦, π’β©Cgrβ¨π, π£β©) β ((π₯(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£) β§ (π¦(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£)))) |
152 | 148, 151 | anbi12d 630 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (((β¨π₯, π¦β©Cgrβ¨π, πβ© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β§ (β¨π₯, π’β©Cgrβ¨π, π£β© β§ β¨π¦, π’β©Cgrβ¨π, π£β©)) β (((π₯(distβ(EEGβπ))π¦) = (π(distβ(EEGβπ))π) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)) β§ ((π₯(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£) β§ (π¦(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£))))) |
153 | 145, 152 | anbi12d 630 |
. . . . . . . . . 10
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (((π₯ β π¦ β§ π¦ Btwn β¨π₯, π§β© β§ π Btwn β¨π, πβ©) β§ ((β¨π₯, π¦β©Cgrβ¨π, πβ© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β§ (β¨π₯, π’β©Cgrβ¨π, π£β© β§ β¨π¦, π’β©Cgrβ¨π, π£β©))) β ((π₯ β π¦ β§ π¦ β (π₯(Itvβ(EEGβπ))π§) β§ π β (π(Itvβ(EEGβπ))π)) β§ (((π₯(distβ(EEGβπ))π¦) = (π(distβ(EEGβπ))π) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)) β§ ((π₯(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£) β§ (π¦(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£)))))) |
154 | 121, 11, 12, 127, 129, 135, 137 | ecgrtg 28749 |
. . . . . . . . . 10
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (β¨π§, π’β©Cgrβ¨π, π£β© β (π§(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£))) |
155 | 142, 153,
154 | 3imtr3d 293 |
. . . . . . . . 9
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (((π₯ β π¦ β§ π¦ β (π₯(Itvβ(EEGβπ))π§) β§ π β (π(Itvβ(EEGβπ))π)) β§ (((π₯(distβ(EEGβπ))π¦) = (π(distβ(EEGβπ))π) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)) β§ ((π₯(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£) β§ (π¦(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£)))) β (π§(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£))) |
156 | 155 | ralrimivvva 3197 |
. . . . . . . 8
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β βπ β
(Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))(((π₯ β π¦ β§ π¦ β (π₯(Itvβ(EEGβπ))π§) β§ π β (π(Itvβ(EEGβπ))π)) β§ (((π₯(distβ(EEGβπ))π¦) = (π(distβ(EEGβπ))π) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)) β§ ((π₯(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£) β§ (π¦(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£)))) β (π§(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£))) |
157 | 156 | ralrimivvva 3197 |
. . . . . . 7
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β βπ§ β (Baseβ(EEGβπ))βπ’ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))(((π₯ β π¦ β§ π¦ β (π₯(Itvβ(EEGβπ))π§) β§ π β (π(Itvβ(EEGβπ))π)) β§ (((π₯(distβ(EEGβπ))π¦) = (π(distβ(EEGβπ))π) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)) β§ ((π₯(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£) β§ (π¦(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£)))) β (π§(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£))) |
158 | 157 | ralrimivva 3194 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))βπ’ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))(((π₯ β π¦ β§ π¦ β (π₯(Itvβ(EEGβπ))π§) β§ π β (π(Itvβ(EEGβπ))π)) β§ (((π₯(distβ(EEGβπ))π¦) = (π(distβ(EEGβπ))π) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)) β§ ((π₯(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£) β§ (π¦(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£)))) β (π§(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£))) |
159 | | simpll 764 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π β β) |
160 | 6 | adantr 480 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π₯ β (πΌβπ)) |
161 | 8 | adantr 480 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π¦ β (πΌβπ)) |
162 | | simprl 768 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
163 | 159, 4 | syl 17 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β
(πΌβπ) =
(Baseβ(EEGβπ))) |
164 | 162, 163 | eleqtrrd 2830 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π β (πΌβπ)) |
165 | | simprr 770 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
166 | 165, 163 | eleqtrrd 2830 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π β (πΌβπ)) |
167 | | axsegcon 28693 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ))) β βπ§ β (πΌβπ)(π¦ Btwn β¨π₯, π§β© β§ β¨π¦, π§β©Cgrβ¨π, πβ©)) |
168 | 159, 160,
161, 164, 166, 167 | syl122anc 1376 |
. . . . . . . . 9
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β βπ§ β (πΌβπ)(π¦ Btwn β¨π₯, π§β© β§ β¨π¦, π§β©Cgrβ¨π, πβ©)) |
169 | | simplll 772 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π β β) |
170 | 3 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π₯ β (Baseβ(EEGβπ))) |
171 | | simpr 484 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π§ β (πΌβπ)) |
172 | 163 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β (πΌβπ) = (Baseβ(EEGβπ))) |
173 | 171, 172 | eleqtrd 2829 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π§ β (Baseβ(EEGβπ))) |
174 | 7 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π¦ β (Baseβ(EEGβπ))) |
175 | 169, 11, 30, 170, 173, 174 | ebtwntg 28748 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β (π¦ Btwn β¨π₯, π§β© β π¦ β (π₯(Itvβ(EEGβπ))π§))) |
176 | | simplrl 774 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π β (Baseβ(EEGβπ))) |
177 | | simplrr 775 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π β (Baseβ(EEGβπ))) |
178 | 169, 11, 12, 174, 173, 176, 177 | ecgrtg 28749 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β (β¨π¦, π§β©Cgrβ¨π, πβ© β (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π))) |
179 | 175, 178 | anbi12d 630 |
. . . . . . . . . 10
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β ((π¦ Btwn β¨π₯, π§β© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β (π¦ β (π₯(Itvβ(EEGβπ))π§) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)))) |
180 | 163, 179 | rexeqbidva 3322 |
. . . . . . . . 9
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β (βπ§ β (πΌβπ)(π¦ Btwn β¨π₯, π§β© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β βπ§ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π§) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)))) |
181 | 168, 180 | mpbid 231 |
. . . . . . . 8
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β βπ§ β
(Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π§) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π))) |
182 | 181 | ralrimivva 3194 |
. . . . . . 7
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π§) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π))) |
183 | 182 | ralrimivva 3194 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π§) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π))) |
184 | 1, 158, 183 | jca32 515 |
. . . . 5
β’ (π β β β
((EEGβπ) β V
β§ (βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))βπ’ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))(((π₯ β π¦ β§ π¦ β (π₯(Itvβ(EEGβπ))π§) β§ π β (π(Itvβ(EEGβπ))π)) β§ (((π₯(distβ(EEGβπ))π¦) = (π(distβ(EEGβπ))π) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)) β§ ((π₯(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£) β§ (π¦(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£)))) β (π§(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£)) β§ βπ₯ β (Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π§) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π))))) |
185 | 11, 12, 30 | istrkgcb 28215 |
. . . . 5
β’
((EEGβπ)
β TarskiGCB β ((EEGβπ) β V β§ (βπ₯ β (Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))βπ’ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))(((π₯ β π¦ β§ π¦ β (π₯(Itvβ(EEGβπ))π§) β§ π β (π(Itvβ(EEGβπ))π)) β§ (((π₯(distβ(EEGβπ))π¦) = (π(distβ(EEGβπ))π) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)) β§ ((π₯(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£) β§ (π¦(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£)))) β (π§(distβ(EEGβπ))π’) = (π(distβ(EEGβπ))π£)) β§ βπ₯ β (Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π§) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π))))) |
186 | 184, 185 | sylibr 233 |
. . . 4
β’ (π β β β
(EEGβπ) β
TarskiGCB) |
187 | 11, 30 | elntg 28750 |
. . . . 5
β’ (π β β β
(LineGβ(EEGβπ))
= (π₯ β
(Baseβ(EEGβπ)),
π¦ β
((Baseβ(EEGβπ))
β {π₯}) β¦ {π§ β
(Baseβ(EEGβπ))
β£ (π§ β (π₯(Itvβ(EEGβπ))π¦) β¨ π₯ β (π§(Itvβ(EEGβπ))π¦) β¨ π¦ β (π₯(Itvβ(EEGβπ))π§))})) |
188 | 11, 12, 30 | istrkgl 28217 |
. . . . 5
β’
((EEGβπ)
β {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})} β ((EEGβπ) β V β§
(LineGβ(EEGβπ))
= (π₯ β
(Baseβ(EEGβπ)),
π¦ β
((Baseβ(EEGβπ))
β {π₯}) β¦ {π§ β
(Baseβ(EEGβπ))
β£ (π§ β (π₯(Itvβ(EEGβπ))π¦) β¨ π₯ β (π§(Itvβ(EEGβπ))π¦) β¨ π¦ β (π₯(Itvβ(EEGβπ))π§))}))) |
189 | 1, 187, 188 | sylanbrc 582 |
. . . 4
β’ (π β β β
(EEGβπ) β {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})}) |
190 | 186, 189 | elind 4189 |
. . 3
β’ (π β β β
(EEGβπ) β
(TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) |
191 | 120, 190 | elind 4189 |
. 2
β’ (π β β β
(EEGβπ) β
((TarskiGC β© TarskiGB) β© (TarskiGCB
β© {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})}))) |
192 | | df-trkg 28212 |
. 2
β’ TarskiG =
((TarskiGC β© TarskiGB) β© (TarskiGCB
β© {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) |
193 | 191, 192 | eleqtrrdi 2838 |
1
β’ (π β β β
(EEGβπ) β
TarskiG) |