Step | Hyp | Ref
| Expression |
1 | | hpgid.p |
. . . . . . . 8
β’ π = (BaseβπΊ) |
2 | | hpgid.i |
. . . . . . . 8
β’ πΌ = (ItvβπΊ) |
3 | | hpgid.l |
. . . . . . . 8
β’ πΏ = (LineGβπΊ) |
4 | | hpgid.g |
. . . . . . . . 9
β’ (π β πΊ β TarskiG) |
5 | 4 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β πΊ β TarskiG) |
6 | | hpgid.a |
. . . . . . . . . 10
β’ (π β π΄ β π) |
7 | 6 | ad3antrrr 728 |
. . . . . . . . 9
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π΄ β π) |
8 | | colopp.b |
. . . . . . . . . 10
β’ (π β π΅ β π) |
9 | 8 | ad3antrrr 728 |
. . . . . . . . 9
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π΅ β π) |
10 | | eqid 2731 |
. . . . . . . . . 10
β’
(distβπΊ) =
(distβπΊ) |
11 | | hpgid.o |
. . . . . . . . . 10
β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} |
12 | | hpgid.d |
. . . . . . . . . . 11
β’ (π β π· β ran πΏ) |
13 | 12 | ad3antrrr 728 |
. . . . . . . . . 10
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π· β ran πΏ) |
14 | | simpllr 774 |
. . . . . . . . . . 11
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) |
15 | | simplr 767 |
. . . . . . . . . . . 12
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π¦ β π·) |
16 | | eleq1w 2815 |
. . . . . . . . . . . . 13
β’ (π‘ = π¦ β (π‘ β (π΄πΌπ΅) β π¦ β (π΄πΌπ΅))) |
17 | 16 | adantl 482 |
. . . . . . . . . . . 12
β’
(((((π β§ (Β¬
π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β§ π‘ = π¦) β (π‘ β (π΄πΌπ΅) β π¦ β (π΄πΌπ΅))) |
18 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π¦ β (π΄πΌπ΅)) |
19 | 15, 17, 18 | rspcedvd 3597 |
. . . . . . . . . . 11
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β βπ‘ β π· π‘ β (π΄πΌπ΅)) |
20 | 1, 10, 2, 11, 6, 8 | islnopp 27778 |
. . . . . . . . . . . 12
β’ (π β (π΄ππ΅ β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)))) |
21 | 20 | ad3antrrr 728 |
. . . . . . . . . . 11
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β (π΄ππ΅ β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)))) |
22 | 14, 19, 21 | mpbir2and 711 |
. . . . . . . . . 10
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π΄ππ΅) |
23 | 1, 10, 2, 11, 3, 13, 5, 7, 9,
22 | oppne3 27782 |
. . . . . . . . 9
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π΄ β π΅) |
24 | 1, 2, 3, 5, 7, 9, 23 | tgelrnln 27669 |
. . . . . . . 8
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β (π΄πΏπ΅) β ran πΏ) |
25 | 1, 2, 3, 5, 7, 9, 23 | tglinerflx1 27672 |
. . . . . . . . 9
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π΄ β (π΄πΏπ΅)) |
26 | 14 | simpld 495 |
. . . . . . . . 9
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β Β¬ π΄ β π·) |
27 | | nelne1 3038 |
. . . . . . . . 9
β’ ((π΄ β (π΄πΏπ΅) β§ Β¬ π΄ β π·) β (π΄πΏπ΅) β π·) |
28 | 25, 26, 27 | syl2anc 584 |
. . . . . . . 8
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β (π΄πΏπ΅) β π·) |
29 | 23 | neneqd 2944 |
. . . . . . . . . 10
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β Β¬ π΄ = π΅) |
30 | | colopp.1 |
. . . . . . . . . . . . 13
β’ (π β (πΆ β (π΄πΏπ΅) β¨ π΄ = π΅)) |
31 | 30 | orcomd 869 |
. . . . . . . . . . . 12
β’ (π β (π΄ = π΅ β¨ πΆ β (π΄πΏπ΅))) |
32 | 31 | ord 862 |
. . . . . . . . . . 11
β’ (π β (Β¬ π΄ = π΅ β πΆ β (π΄πΏπ΅))) |
33 | 32 | ad3antrrr 728 |
. . . . . . . . . 10
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β (Β¬ π΄ = π΅ β πΆ β (π΄πΏπ΅))) |
34 | 29, 33 | mpd 15 |
. . . . . . . . 9
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β πΆ β (π΄πΏπ΅)) |
35 | | colopp.p |
. . . . . . . . . 10
β’ (π β πΆ β π·) |
36 | 35 | ad3antrrr 728 |
. . . . . . . . 9
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β πΆ β π·) |
37 | 34, 36 | elind 4174 |
. . . . . . . 8
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β πΆ β ((π΄πΏπ΅) β© π·)) |
38 | 1, 3, 2, 5, 13, 15 | tglnpt 27588 |
. . . . . . . . . 10
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π¦ β π) |
39 | 1, 2, 3, 5, 7, 9, 38, 23, 18 | btwnlng1 27658 |
. . . . . . . . 9
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π¦ β (π΄πΏπ΅)) |
40 | 39, 15 | elind 4174 |
. . . . . . . 8
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β π¦ β ((π΄πΏπ΅) β© π·)) |
41 | 1, 2, 3, 5, 24, 13, 28, 37, 40 | tglineineq 27682 |
. . . . . . 7
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β πΆ = π¦) |
42 | 41, 18 | eqeltrd 2832 |
. . . . . 6
β’ ((((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β πΆ β (π΄πΌπ΅)) |
43 | 42 | adantllr 717 |
. . . . 5
β’
(((((π β§ (Β¬
π΄ β π· β§ Β¬ π΅ β π·)) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)) β§ π¦ β π·) β§ π¦ β (π΄πΌπ΅)) β πΆ β (π΄πΌπ΅)) |
44 | | simpr 485 |
. . . . . 6
β’ (((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)) β βπ‘ β π· π‘ β (π΄πΌπ΅)) |
45 | 16 | cbvrexvw 3234 |
. . . . . 6
β’
(βπ‘ β
π· π‘ β (π΄πΌπ΅) β βπ¦ β π· π¦ β (π΄πΌπ΅)) |
46 | 44, 45 | sylib 217 |
. . . . 5
β’ (((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)) β βπ¦ β π· π¦ β (π΄πΌπ΅)) |
47 | 43, 46 | r19.29a 3161 |
. . . 4
β’ (((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)) β πΆ β (π΄πΌπ΅)) |
48 | 35 | adantr 481 |
. . . . . 6
β’ ((π β§ πΆ β (π΄πΌπ΅)) β πΆ β π·) |
49 | | simpr 485 |
. . . . . . 7
β’ (((π β§ πΆ β (π΄πΌπ΅)) β§ π‘ = πΆ) β π‘ = πΆ) |
50 | 49 | eleq1d 2817 |
. . . . . 6
β’ (((π β§ πΆ β (π΄πΌπ΅)) β§ π‘ = πΆ) β (π‘ β (π΄πΌπ΅) β πΆ β (π΄πΌπ΅))) |
51 | | simpr 485 |
. . . . . 6
β’ ((π β§ πΆ β (π΄πΌπ΅)) β πΆ β (π΄πΌπ΅)) |
52 | 48, 50, 51 | rspcedvd 3597 |
. . . . 5
β’ ((π β§ πΆ β (π΄πΌπ΅)) β βπ‘ β π· π‘ β (π΄πΌπ΅)) |
53 | 52 | adantlr 713 |
. . . 4
β’ (((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β§ πΆ β (π΄πΌπ΅)) β βπ‘ β π· π‘ β (π΄πΌπ΅)) |
54 | 47, 53 | impbida 799 |
. . 3
β’ ((π β§ (Β¬ π΄ β π· β§ Β¬ π΅ β π·)) β (βπ‘ β π· π‘ β (π΄πΌπ΅) β πΆ β (π΄πΌπ΅))) |
55 | 54 | pm5.32da 579 |
. 2
β’ (π β (((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)) β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ πΆ β (π΄πΌπ΅)))) |
56 | | 3anrot 1100 |
. . . 4
β’ ((πΆ β (π΄πΌπ΅) β§ Β¬ π΄ β π· β§ Β¬ π΅ β π·) β (Β¬ π΄ β π· β§ Β¬ π΅ β π· β§ πΆ β (π΄πΌπ΅))) |
57 | | df-3an 1089 |
. . . 4
β’ ((Β¬
π΄ β π· β§ Β¬ π΅ β π· β§ πΆ β (π΄πΌπ΅)) β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ πΆ β (π΄πΌπ΅))) |
58 | 56, 57 | bitri 274 |
. . 3
β’ ((πΆ β (π΄πΌπ΅) β§ Β¬ π΄ β π· β§ Β¬ π΅ β π·) β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ πΆ β (π΄πΌπ΅))) |
59 | 58 | a1i 11 |
. 2
β’ (π β ((πΆ β (π΄πΌπ΅) β§ Β¬ π΄ β π· β§ Β¬ π΅ β π·) β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ πΆ β (π΄πΌπ΅)))) |
60 | 55, 20, 59 | 3bitr4d 310 |
1
β’ (π β (π΄ππ΅ β (πΆ β (π΄πΌπ΅) β§ Β¬ π΄ β π· β§ Β¬ π΅ β π·))) |