Step | Hyp | Ref
| Expression |
1 | | iscgra.p |
. . 3
β’ π = (BaseβπΊ) |
2 | | iscgra.i |
. . 3
β’ πΌ = (ItvβπΊ) |
3 | | iscgra.k |
. . 3
β’ πΎ = (hlGβπΊ) |
4 | | iscgra.g |
. . . 4
β’ (π β πΊ β TarskiG) |
5 | 4 | ad3antrrr 729 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β πΊ β TarskiG) |
6 | | iscgra.a |
. . . 4
β’ (π β π΄ β π) |
7 | 6 | ad3antrrr 729 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π΄ β π) |
8 | | iscgra.b |
. . . 4
β’ (π β π΅ β π) |
9 | 8 | ad3antrrr 729 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π΅ β π) |
10 | | iscgra.c |
. . . 4
β’ (π β πΆ β π) |
11 | 10 | ad3antrrr 729 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β πΆ β π) |
12 | | cgrahl1.x |
. . . 4
β’ (π β π β π) |
13 | 12 | ad3antrrr 729 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π β π) |
14 | | iscgra.e |
. . . 4
β’ (π β πΈ β π) |
15 | 14 | ad3antrrr 729 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β πΈ β π) |
16 | | iscgra.f |
. . . 4
β’ (π β πΉ β π) |
17 | 16 | ad3antrrr 729 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β πΉ β π) |
18 | | simpllr 775 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π₯ β π) |
19 | | simplr 768 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π¦ β π) |
20 | | simpr1 1195 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ©) |
21 | | iscgra.d |
. . . . 5
β’ (π β π· β π) |
22 | 21 | ad3antrrr 729 |
. . . 4
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π· β π) |
23 | | simpr2 1196 |
. . . 4
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π₯(πΎβπΈ)π·) |
24 | | cgrahl1.1 |
. . . . . 6
β’ (π β π(πΎβπΈ)π·) |
25 | 24 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π(πΎβπΈ)π·) |
26 | 1, 2, 3, 13, 22, 15, 5, 25 | hlcomd 27588 |
. . . 4
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π·(πΎβπΈ)π) |
27 | 1, 2, 3, 18, 22, 13, 5, 15, 23, 26 | hltr 27594 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π₯(πΎβπΈ)π) |
28 | | simpr3 1197 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β π¦(πΎβπΈ)πΉ) |
29 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18, 19, 20, 27, 28 | iscgrad 27795 |
. 2
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βππΈπΉββ©) |
30 | | cgrahl1.2 |
. . 3
β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) |
31 | 1, 2, 3, 4, 6, 8, 10, 21, 14, 16 | iscgra 27793 |
. . 3
β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ))) |
32 | 30, 31 | mpbid 231 |
. 2
β’ (π β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯πΈπ¦ββ© β§ π₯(πΎβπΈ)π· β§ π¦(πΎβπΈ)πΉ)) |
33 | 29, 32 | r19.29vva 3208 |
1
β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βππΈπΉββ©) |