Step | Hyp | Ref
| Expression |
1 | | trgcopy.p |
. . 3
β’ π = (BaseβπΊ) |
2 | | trgcopy.m |
. . 3
β’ β =
(distβπΊ) |
3 | | trgcopy.i |
. . 3
β’ πΌ = (ItvβπΊ) |
4 | | trgcopy.l |
. . 3
β’ πΏ = (LineGβπΊ) |
5 | | trgcopy.k |
. . 3
β’ πΎ = (hlGβπΊ) |
6 | | trgcopy.g |
. . 3
β’ (π β πΊ β TarskiG) |
7 | | trgcopy.a |
. . 3
β’ (π β π΄ β π) |
8 | | trgcopy.b |
. . 3
β’ (π β π΅ β π) |
9 | | trgcopy.c |
. . 3
β’ (π β πΆ β π) |
10 | | trgcopy.d |
. . 3
β’ (π β π· β π) |
11 | | trgcopy.e |
. . 3
β’ (π β πΈ β π) |
12 | | trgcopy.f |
. . 3
β’ (π β πΉ β π) |
13 | | trgcopy.1 |
. . 3
β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) |
14 | | trgcopy.2 |
. . 3
β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) |
15 | | trgcopy.3 |
. . 3
β’ (π β (π΄ β π΅) = (π· β πΈ)) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | trgcopy 27788 |
. 2
β’ (π β βπ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) |
17 | 6 | ad5antr 733 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β πΊ β TarskiG) |
18 | 7 | ad5antr 733 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β π΄ β π) |
19 | 8 | ad5antr 733 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β π΅ β π) |
20 | 9 | ad5antr 733 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β πΆ β π) |
21 | 10 | ad5antr 733 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β π· β π) |
22 | 11 | ad5antr 733 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β πΈ β π) |
23 | 12 | ad5antr 733 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β πΉ β π) |
24 | 13 | ad5antr 733 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) |
25 | 14 | ad5antr 733 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) |
26 | 15 | ad5antr 733 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β (π΄ β π΅) = (π· β πΈ)) |
27 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π₯ = π β§ π¦ = π) β π₯ = π) |
28 | 27 | eleq1d 2823 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = π) β (π₯ β (π β (π·πΏπΈ)) β π β (π β (π·πΏπΈ)))) |
29 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π₯ = π β§ π¦ = π) β π¦ = π) |
30 | 29 | eleq1d 2823 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = π) β (π¦ β (π β (π·πΏπΈ)) β π β (π β (π·πΏπΈ)))) |
31 | 28, 30 | anbi12d 632 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π) β ((π₯ β (π β (π·πΏπΈ)) β§ π¦ β (π β (π·πΏπΈ))) β (π β (π β (π·πΏπΈ)) β§ π β (π β (π·πΏπΈ))))) |
32 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π₯ = π β§ π¦ = π) β§ π§ = π‘) β π§ = π‘) |
33 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((π₯ = π β§ π¦ = π) β§ π§ = π‘) β π₯ = π) |
34 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π₯ = π β§ π¦ = π) β§ π§ = π‘) β π¦ = π) |
35 | 33, 34 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (((π₯ = π β§ π¦ = π) β§ π§ = π‘) β (π₯πΌπ¦) = (ππΌπ)) |
36 | 32, 35 | eleq12d 2832 |
. . . . . . . . . 10
β’ (((π₯ = π β§ π¦ = π) β§ π§ = π‘) β (π§ β (π₯πΌπ¦) β π‘ β (ππΌπ))) |
37 | 36 | cbvrexdva 3330 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π) β (βπ§ β (π·πΏπΈ)π§ β (π₯πΌπ¦) β βπ‘ β (π·πΏπΈ)π‘ β (ππΌπ))) |
38 | 31, 37 | anbi12d 632 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π) β (((π₯ β (π β (π·πΏπΈ)) β§ π¦ β (π β (π·πΏπΈ))) β§ βπ§ β (π·πΏπΈ)π§ β (π₯πΌπ¦)) β ((π β (π β (π·πΏπΈ)) β§ π β (π β (π·πΏπΈ))) β§ βπ‘ β (π·πΏπΈ)π‘ β (ππΌπ)))) |
39 | 38 | cbvopabv 5183 |
. . . . . . 7
β’
{β¨π₯, π¦β© β£ ((π₯ β (π β (π·πΏπΈ)) β§ π¦ β (π β (π·πΏπΈ))) β§ βπ§ β (π·πΏπΈ)π§ β (π₯πΌπ¦))} = {β¨π, πβ© β£ ((π β (π β (π·πΏπΈ)) β§ π β (π β (π·πΏπΈ))) β§ βπ‘ β (π·πΏπΈ)π‘ β (ππΌπ))} |
40 | | simp-5r 785 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β π β π) |
41 | | simp-4r 783 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β π β π) |
42 | | simpllr 775 |
. . . . . . . 8
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) |
43 | 42 | simpld 496 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) |
44 | | simplr 768 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) |
45 | 42 | simprd 497 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β π((hpGβπΊ)β(π·πΏπΈ))πΉ) |
46 | | simpr 486 |
. . . . . . 7
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β π((hpGβπΊ)β(π·πΏπΈ))πΉ) |
47 | 1, 2, 3, 4, 5, 17,
18, 19, 20, 21, 22, 23, 24, 25, 26, 39, 40, 41, 43, 44, 45, 46 | trgcopyeulem 27789 |
. . . . . 6
β’
((((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β π = π) |
48 | 47 | anasss 468 |
. . . . 5
β’
(((((π β§ π β π) β§ π β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β π = π) |
49 | 48 | expl 459 |
. . . 4
β’ (((π β§ π β π) β§ π β π) β (((β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β π = π)) |
50 | 49 | anasss 468 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β (((β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β π = π)) |
51 | 50 | ralrimivva 3198 |
. 2
β’ (π β βπ β π βπ β π (((β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β π = π)) |
52 | | eqidd 2738 |
. . . . . 6
β’ (π = π β π· = π·) |
53 | | eqidd 2738 |
. . . . . 6
β’ (π = π β πΈ = πΈ) |
54 | | id 22 |
. . . . . 6
β’ (π = π β π = π) |
55 | 52, 53, 54 | s3eqd 14760 |
. . . . 5
β’ (π = π β β¨βπ·πΈπββ© = β¨βπ·πΈπββ©) |
56 | 55 | breq2d 5122 |
. . . 4
β’ (π = π β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©)) |
57 | | breq1 5113 |
. . . 4
β’ (π = π β (π((hpGβπΊ)β(π·πΏπΈ))πΉ β π((hpGβπΊ)β(π·πΏπΈ))πΉ)) |
58 | 56, 57 | anbi12d 632 |
. . 3
β’ (π = π β ((β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ))) |
59 | 58 | reu4 3694 |
. 2
β’
(β!π β
π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β (βπ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β§ βπ β π βπ β π (((β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) β π = π))) |
60 | 16, 51, 59 | sylanbrc 584 |
1
β’ (π β β!π β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ© β§ π((hpGβπΊ)β(π·πΏπΈ))πΉ)) |