Step | Hyp | Ref
| Expression |
1 | | fvexd 6862 |
. . . . . 6
β’ (π β β β
(EEGβπ) β
V) |
2 | | simpl 484 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β π β β) |
3 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β π₯ β (Baseβ(EEGβπ))) |
4 | | eengbas 27972 |
. . . . . . . . . . 11
β’ (π β β β
(πΌβπ) =
(Baseβ(EEGβπ))) |
5 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (πΌβπ) = (Baseβ(EEGβπ))) |
6 | 3, 5 | eleqtrrd 2841 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β π₯ β (πΌβπ)) |
7 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β π¦ β (Baseβ(EEGβπ))) |
8 | 7, 5 | eleqtrrd 2841 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β π¦ β (πΌβπ)) |
9 | | axcgrrflx 27905 |
. . . . . . . . 9
β’ ((π β β β§ π₯ β (πΌβπ) β§ π¦ β (πΌβπ)) β β¨π₯, π¦β©Cgrβ¨π¦, π₯β©) |
10 | 2, 6, 8, 9 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β β¨π₯, π¦β©Cgrβ¨π¦, π₯β©) |
11 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβ(EEGβπ)) = (Baseβ(EEGβπ)) |
12 | | eqid 2737 |
. . . . . . . . 9
β’
(distβ(EEGβπ)) = (distβ(EEGβπ)) |
13 | 2, 11, 12, 3, 7, 7,
3 | ecgrtg 27974 |
. . . . . . . 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 3198 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))(π₯(distβ(EEGβπ))π¦) = (π¦(distβ(EEGβπ))π₯)) |
16 | | simpl 484 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π β β) |
17 | | simpr1 1195 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π₯ β (Baseβ(EEGβπ))) |
18 | | simpr2 1196 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π¦ β (Baseβ(EEGβπ))) |
19 | | simpr3 1197 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π§ β (Baseβ(EEGβπ))) |
20 | 16, 11, 12, 17, 18, 19, 19 | ecgrtg 27974 |
. . . . . . . 8
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β (β¨π₯, π¦β©Cgrβ¨π§, π§β© β (π₯(distβ(EEGβπ))π¦) = (π§(distβ(EEGβπ))π§))) |
21 | 6 | 3adantr3 1172 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π₯ β (πΌβπ)) |
22 | 8 | 3adantr3 1172 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π¦ β (πΌβπ)) |
23 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β (πΌβπ) = (Baseβ(EEGβπ))) |
24 | 19, 23 | eleqtrrd 2841 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ))
β§ π§ β
(Baseβ(EEGβπ)))) β π§ β (πΌβπ)) |
25 | | axcgrid 27907 |
. . . . . . . . 9
β’ ((π β β β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ) β§ π§ β (πΌβπ))) β (β¨π₯, π¦β©Cgrβ¨π§, π§β© β π₯ = π¦)) |
26 | 16, 21, 22, 24, 25 | syl13anc 1373 |
. . . . . . . 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 3201 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))((π₯(distβ(EEGβπ))π¦) = (π§(distβ(EEGβπ))π§) β π₯ = π¦)) |
29 | 1, 15, 28 | jca32 517 |
. . . . 5
β’ (π β β β
((EEGβπ) β V
β§ (βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))(π₯(distβ(EEGβπ))π¦) = (π¦(distβ(EEGβπ))π₯) β§ βπ₯ β (Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))((π₯(distβ(EEGβπ))π¦) = (π§(distβ(EEGβπ))π§) β π₯ = π¦)))) |
30 | | eqid 2737 |
. . . . . 6
β’
(Itvβ(EEGβπ)) = (Itvβ(EEGβπ)) |
31 | 11, 12, 30 | istrkgc 27438 |
. . . . 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 27973 |
. . . . . . . . . . 11
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (π¦ Btwn β¨π₯, π₯β© β π¦ β (π₯(Itvβ(EEGβπ))π₯))) |
34 | | axbtwnid 27930 |
. . . . . . . . . . . 12
β’ ((π β β β§ π¦ β (πΌβπ) β§ π₯ β (πΌβπ)) β (π¦ Btwn β¨π₯, π₯β© β π¦ = π₯)) |
35 | 2, 8, 6, 34 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (π¦ Btwn β¨π₯, π₯β© β π¦ = π₯)) |
36 | 33, 35 | sylbird 260 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (π¦ β (π₯(Itvβ(EEGβπ))π₯) β π¦ = π₯)) |
37 | 36 | imp 408 |
. . . . . . . . 9
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ π¦ β (π₯(Itvβ(EEGβπ))π₯)) β π¦ = π₯) |
38 | 37 | equcomd 2023 |
. . . . . . . 8
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ π¦ β (π₯(Itvβ(EEGβπ))π₯)) β π₯ = π¦) |
39 | 38 | ex 414 |
. . . . . . 7
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β (π¦ β (π₯(Itvβ(EEGβπ))π₯) β π₯ = π¦)) |
40 | 39 | ralrimivva 3198 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π₯) β π₯ = π¦)) |
41 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β β) |
42 | 6 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π₯ β (πΌβπ)) |
43 | 8 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π¦ β (πΌβπ)) |
44 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π₯ β (Baseβ(EEGβπ))) |
45 | 7 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π¦ β (Baseβ(EEGβπ))) |
46 | | simpr1 1195 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π§ β (Baseβ(EEGβπ))) |
47 | 41, 44, 45, 46, 24 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π§ β (πΌβπ)) |
48 | | simpr2 1196 |
. . . . . . . . . . 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 2841 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π’ β (πΌβπ)) |
51 | | simpr3 1197 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π£ β (Baseβ(EEGβπ))) |
52 | 51, 49 | eleqtrrd 2841 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π£ β (πΌβπ)) |
53 | | axpasch 27932 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ) β§ π§ β (πΌβπ)) β§ (π’ β (πΌβπ) β§ π£ β (πΌβπ))) β ((π’ Btwn β¨π₯, π§β© β§ π£ Btwn β¨π¦, π§β©) β βπ β (πΌβπ)(π Btwn β¨π’, π¦β© β§ π Btwn β¨π£, π₯β©))) |
54 | 41, 42, 43, 47, 50, 52, 53 | syl132anc 1389 |
. . . . . . . . 9
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β ((π’ Btwn β¨π₯, π§β© β§ π£ Btwn β¨π¦, π§β©) β βπ β (πΌβπ)(π Btwn β¨π’, π¦β© β§ π Btwn β¨π£, π₯β©))) |
55 | 41, 11, 30, 44, 46, 48 | ebtwntg 27973 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (π’ Btwn β¨π₯, π§β© β π’ β (π₯(Itvβ(EEGβπ))π§))) |
56 | 41, 11, 30, 45, 46, 51 | ebtwntg 27973 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (π£ Btwn β¨π¦, π§β© β π£ β (π¦(Itvβ(EEGβπ))π§))) |
57 | 55, 56 | anbi12d 632 |
. . . . . . . . 9
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β ((π’ Btwn β¨π₯, π§β© β§ π£ Btwn β¨π¦, π§β©) β (π’ β (π₯(Itvβ(EEGβπ))π§) β§ π£ β (π¦(Itvβ(EEGβπ))π§)))) |
58 | | simplll 774 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π β β) |
59 | 48 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π’ β (Baseβ(EEGβπ))) |
60 | 45 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π¦ β (Baseβ(EEGβπ))) |
61 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π β (πΌβπ)) |
62 | 49 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β (πΌβπ) = (Baseβ(EEGβπ))) |
63 | 61, 62 | eleqtrd 2840 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π β (Baseβ(EEGβπ))) |
64 | 58, 11, 30, 59, 60, 63 | ebtwntg 27973 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β (π Btwn β¨π’, π¦β© β π β (π’(Itvβ(EEGβπ))π¦))) |
65 | 51 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π£ β (Baseβ(EEGβπ))) |
66 | 44 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β π₯ β (Baseβ(EEGβπ))) |
67 | 58, 11, 30, 65, 66, 63 | ebtwntg 27973 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β (π Btwn β¨π£, π₯β© β π β (π£(Itvβ(EEGβπ))π₯))) |
68 | 64, 67 | anbi12d 632 |
. . . . . . . . . 10
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β ((π Btwn β¨π’, π¦β© β§ π Btwn β¨π£, π₯β©) β (π β (π’(Itvβ(EEGβπ))π¦) β§ π β (π£(Itvβ(EEGβπ))π₯)))) |
69 | 49, 68 | rexeqbidva 3325 |
. . . . . . . . 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 3201 |
. . . . . . 7
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β βπ§ β (Baseβ(EEGβπ))βπ’ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))((π’ β (π₯(Itvβ(EEGβπ))π§) β§ π£ β (π¦(Itvβ(EEGβπ))π§)) β βπ β (Baseβ(EEGβπ))(π β (π’(Itvβ(EEGβπ))π¦) β§ π β (π£(Itvβ(EEGβπ))π₯)))) |
72 | 71 | ralrimivva 3198 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))βπ’ β (Baseβ(EEGβπ))βπ£ β (Baseβ(EEGβπ))((π’ β (π₯(Itvβ(EEGβπ))π§) β§ π£ β (π¦(Itvβ(EEGβπ))π§)) β βπ β (Baseβ(EEGβπ))(π β (π’(Itvβ(EEGβπ))π¦) β§ π β (π£(Itvβ(EEGβπ))π₯)))) |
73 | | simpl 484 |
. . . . . . . . 9
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β π β β) |
74 | | elpwi 4572 |
. . . . . . . . . . 11
β’ (π β π«
(Baseβ(EEGβπ))
β π β
(Baseβ(EEGβπ))) |
75 | 74 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
76 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β (πΌβπ) = (Baseβ(EEGβπ))) |
77 | 75, 76 | sseqtrrd 3990 |
. . . . . . . . 9
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β π β (πΌβπ)) |
78 | | elpwi 4572 |
. . . . . . . . . . 11
β’ (π‘ β π«
(Baseβ(EEGβπ))
β π‘ β
(Baseβ(EEGβπ))) |
79 | 78 | ad2antll 728 |
. . . . . . . . . 10
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β π‘ β (Baseβ(EEGβπ))) |
80 | 79, 76 | sseqtrrd 3990 |
. . . . . . . . 9
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β π‘ β (πΌβπ)) |
81 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) β π β β) |
82 | | simplrl 776 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) β π β (πΌβπ)) |
83 | | simplrr 777 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) β π‘ β (πΌβπ)) |
84 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) β βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) |
85 | | axcont 27967 |
. . . . . . . . . . 11
β’ ((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©)) β βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β©) |
86 | 81, 82, 83, 84, 85 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β§ βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β©) β βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β©) |
87 | 86 | ex 414 |
. . . . . . . . 9
β’ ((π β β β§ (π β (πΌβπ) β§ π‘ β (πΌβπ))) β (βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β© β βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β©)) |
88 | 73, 77, 80, 87 | syl12anc 836 |
. . . . . . . 8
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β (βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β© β βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β©)) |
89 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β β) |
90 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (πΌβπ)) |
91 | 76 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β (πΌβπ) = (Baseβ(EEGβπ))) |
92 | 90, 91 | eleqtrd 2840 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (Baseβ(EEGβπ))) |
93 | 79 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π‘ β (Baseβ(EEGβπ))) |
94 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π¦ β π‘) |
95 | 93, 94 | sseldd 3950 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π¦ β (Baseβ(EEGβπ))) |
96 | 75 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (Baseβ(EEGβπ))) |
97 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π₯ β π ) |
98 | 96, 97 | sseldd 3950 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π₯ β (Baseβ(EEGβπ))) |
99 | 89, 11, 30, 92, 95, 98 | ebtwntg 27973 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β (π₯ Btwn β¨π, π¦β© β π₯ β (π(Itvβ(EEGβπ))π¦))) |
100 | 99 | 2ralbidva 3211 |
. . . . . . . . 9
β’ (((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β (βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β© β βπ₯ β π βπ¦ β π‘ π₯ β (π(Itvβ(EEGβπ))π¦))) |
101 | 76, 100 | rexeqbidva 3325 |
. . . . . . . 8
β’ ((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β (βπ β (πΌβπ)βπ₯ β π βπ¦ β π‘ π₯ Btwn β¨π, π¦β© β βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π₯ β (π(Itvβ(EEGβπ))π¦))) |
102 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β β) |
103 | 75 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (Baseβ(EEGβπ))) |
104 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π₯ β π ) |
105 | 103, 104 | sseldd 3950 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π₯ β (Baseβ(EEGβπ))) |
106 | 79 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π‘ β (Baseβ(EEGβπ))) |
107 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π¦ β π‘) |
108 | 106, 107 | sseldd 3950 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π¦ β (Baseβ(EEGβπ))) |
109 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (πΌβπ)) |
110 | 76 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β (πΌβπ) = (Baseβ(EEGβπ))) |
111 | 109, 110 | eleqtrd 2840 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β π β (Baseβ(EEGβπ))) |
112 | 102, 11, 30, 105, 108, 111 | ebtwntg 27973 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β§ (π₯ β π β§ π¦ β π‘)) β (π Btwn β¨π₯, π¦β© β π β (π₯(Itvβ(EEGβπ))π¦))) |
113 | 112 | 2ralbidva 3211 |
. . . . . . . . 9
β’ (((π β β β§ (π β π«
(Baseβ(EEGβπ))
β§ π‘ β π«
(Baseβ(EEGβπ)))) β§ π β (πΌβπ)) β (βπ₯ β π βπ¦ β π‘ π Btwn β¨π₯, π¦β© β βπ₯ β π βπ¦ β π‘ π β (π₯(Itvβ(EEGβπ))π¦))) |
114 | 76, 113 | rexeqbidva 3325 |
. . . . . . . 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 3198 |
. . . . . 6
β’ (π β β β
βπ β π«
(Baseβ(EEGβπ))βπ‘ β π«
(Baseβ(EEGβπ))(βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π₯ β (π(Itvβ(EEGβπ))π¦) β βπ β (Baseβ(EEGβπ))βπ₯ β π βπ¦ β π‘ π β (π₯(Itvβ(EEGβπ))π¦))) |
117 | 40, 72, 116 | 3jca 1129 |
. . . . 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 27439 |
. . . . 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 584 |
. . . 4
β’ (π β β β
(EEGβπ) β
TarskiGB) |
120 | 32, 119 | elind 4159 |
. . 3
β’ (π β β β
(EEGβπ) β
(TarskiGC β© TarskiGB)) |
121 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β β) |
122 | 3 | ad2antrr 725 |
. . . . . . . . . . . 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 2841 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π₯ β (πΌβπ)) |
125 | 7 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π¦ β (Baseβ(EEGβπ))) |
126 | 125, 123 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π¦ β (πΌβπ)) |
127 | | simplr1 1216 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π§ β (Baseβ(EEGβπ))) |
128 | 127, 123 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π§ β (πΌβπ)) |
129 | | simplr2 1217 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π’ β (Baseβ(EEGβπ))) |
130 | 129, 123 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π’ β (πΌβπ)) |
131 | | simplr3 1218 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
132 | 131, 123 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (πΌβπ)) |
133 | | simpr1 1195 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
134 | 133, 123 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (πΌβπ)) |
135 | | simpr2 1196 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
136 | 135, 123 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π β (πΌβπ)) |
137 | | simpr3 1197 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π£ β (Baseβ(EEGβπ))) |
138 | 137, 123 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β π£ β (πΌβπ)) |
139 | | 3anass 1096 |
. . . . . . . . . . . 12
β’ (((π₯ β π¦ β§ π¦ Btwn β¨π₯, π§β© β§ π Btwn β¨π, πβ©) β§ (β¨π₯, π¦β©Cgrβ¨π, πβ© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β§ (β¨π₯, π’β©Cgrβ¨π, π£β© β§ β¨π¦, π’β©Cgrβ¨π, π£β©)) β ((π₯ β π¦ β§ π¦ Btwn β¨π₯, π§β© β§ π Btwn β¨π, πβ©) β§ ((β¨π₯, π¦β©Cgrβ¨π, πβ© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β§ (β¨π₯, π’β©Cgrβ¨π, π£β© β§ β¨π¦, π’β©Cgrβ¨π, π£β©)))) |
140 | | ax5seg 27929 |
. . . . . . . . . . . 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 1403 |
. . . . . . . . . 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 27973 |
. . . . . . . . . . . 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 27973 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π§ β (Baseβ(EEGβπ)) β§ π’ β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)) β§ π£ β (Baseβ(EEGβπ)))) β (π Btwn β¨π, πβ© β π β (π(Itvβ(EEGβπ))π))) |
145 | 143, 144 | 3anbi23d 1440 |
. . . . . . . . . . 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 27974 |
. . . . . . . . . . . . 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 27974 |
. . . . . . . . . . . . 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 632 |
. . . . . . . . . . . 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 27974 |
. . . . . . . . . . . . 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 27974 |
. . . . . . . . . . . . 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 632 |
. . . . . . . . . . . 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 632 |
. . . . . . . . . . 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 632 |
. . . . . . . . . 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 27974 |
. . . . . . . . . 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 3201 |
. . . . . . . 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 3201 |
. . . . . . 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 3198 |
. . . . . 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 766 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π β β) |
160 | 6 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π₯ β (πΌβπ)) |
161 | 8 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π¦ β (πΌβπ)) |
162 | | simprl 770 |
. . . . . . . . . . 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 2841 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π β (πΌβπ)) |
165 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π β (Baseβ(EEGβπ))) |
166 | 165, 163 | eleqtrrd 2841 |
. . . . . . . . . 10
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β π β (πΌβπ)) |
167 | | axsegcon 27918 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ))) β βπ§ β (πΌβπ)(π¦ Btwn β¨π₯, π§β© β§ β¨π¦, π§β©Cgrβ¨π, πβ©)) |
168 | 159, 160,
161, 164, 166, 167 | syl122anc 1380 |
. . . . . . . . 9
β’ (((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β βπ§ β (πΌβπ)(π¦ Btwn β¨π₯, π§β© β§ β¨π¦, π§β©Cgrβ¨π, πβ©)) |
169 | | simplll 774 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π β β) |
170 | 3 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π₯ β (Baseβ(EEGβπ))) |
171 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π§ β (πΌβπ)) |
172 | 163 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β (πΌβπ) = (Baseβ(EEGβπ))) |
173 | 171, 172 | eleqtrd 2840 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π§ β (Baseβ(EEGβπ))) |
174 | 7 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π¦ β (Baseβ(EEGβπ))) |
175 | 169, 11, 30, 170, 173, 174 | ebtwntg 27973 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β (π¦ Btwn β¨π₯, π§β© β π¦ β (π₯(Itvβ(EEGβπ))π§))) |
176 | | simplrl 776 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π β (Baseβ(EEGβπ))) |
177 | | simplrr 777 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β π β (Baseβ(EEGβπ))) |
178 | 169, 11, 12, 174, 173, 176, 177 | ecgrtg 27974 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β (β¨π¦, π§β©Cgrβ¨π, πβ© β (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π))) |
179 | 175, 178 | anbi12d 632 |
. . . . . . . . . 10
β’ ((((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β§ (π β (Baseβ(EEGβπ)) β§ π β (Baseβ(EEGβπ)))) β§ π§ β (πΌβπ)) β ((π¦ Btwn β¨π₯, π§β© β§ β¨π¦, π§β©Cgrβ¨π, πβ©) β (π¦ β (π₯(Itvβ(EEGβπ))π§) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π)))) |
180 | 163, 179 | rexeqbidva 3325 |
. . . . . . . . 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 3198 |
. . . . . . 7
β’ ((π β β β§ (π₯ β
(Baseβ(EEGβπ))
β§ π¦ β
(Baseβ(EEGβπ)))) β βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π§) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π))) |
183 | 182 | ralrimivva 3198 |
. . . . . 6
β’ (π β β β
βπ₯ β
(Baseβ(EEGβπ))βπ¦ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ β (Baseβ(EEGβπ))βπ§ β (Baseβ(EEGβπ))(π¦ β (π₯(Itvβ(EEGβπ))π§) β§ (π¦(distβ(EEGβπ))π§) = (π(distβ(EEGβπ))π))) |
184 | 1, 158, 183 | jca32 517 |
. . . . 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 27440 |
. . . . 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 27975 |
. . . . 5
β’ (π β β β
(LineGβ(EEGβπ))
= (π₯ β
(Baseβ(EEGβπ)),
π¦ β
((Baseβ(EEGβπ))
β {π₯}) β¦ {π§ β
(Baseβ(EEGβπ))
β£ (π§ β (π₯(Itvβ(EEGβπ))π¦) β¨ π₯ β (π§(Itvβ(EEGβπ))π¦) β¨ π¦ β (π₯(Itvβ(EEGβπ))π§))})) |
188 | 11, 12, 30 | istrkgl 27442 |
. . . . 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 584 |
. . . 4
β’ (π β β β
(EEGβπ) β {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})}) |
190 | 186, 189 | elind 4159 |
. . 3
β’ (π β β β
(EEGβπ) β
(TarskiGCB β© {π β£ [(Baseβπ) / π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) |
191 | 120, 190 | elind 4159 |
. 2
β’ (π β β β
(EEGβπ) β
((TarskiGC β© TarskiGB) β© (TarskiGCB
β© {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})}))) |
192 | | df-trkg 27437 |
. 2
β’ TarskiG =
((TarskiGC β© TarskiGB) β© (TarskiGCB
β© {π β£
[(Baseβπ) /
π][(Itvβπ) / π](LineGβπ) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))})})) |
193 | 191, 192 | eleqtrrdi 2849 |
1
β’ (π β β β
(EEGβπ) β
TarskiG) |