Step | Hyp | Ref
| Expression |
1 | | mirreu.a |
. . . . . 6
β’ (π β π΄ β π) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ = π) β π΄ β π) |
3 | | eqidd 2734 |
. . . . 5
β’ ((π β§ π΄ = π) β (π β π΄) = (π β π΄)) |
4 | | simpr 486 |
. . . . . 6
β’ ((π β§ π΄ = π) β π΄ = π) |
5 | | mirreu.p |
. . . . . . 7
β’ π = (BaseβπΊ) |
6 | | mirreu.d |
. . . . . . 7
β’ β =
(distβπΊ) |
7 | | mirreu.i |
. . . . . . 7
β’ πΌ = (ItvβπΊ) |
8 | | mirreu.g |
. . . . . . . 8
β’ (π β πΊ β TarskiG) |
9 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ = π) β πΊ β TarskiG) |
10 | 5, 6, 7, 9, 2, 2 | tgbtwntriv2 27471 |
. . . . . 6
β’ ((π β§ π΄ = π) β π΄ β (π΄πΌπ΄)) |
11 | 4, 10 | eqeltrrd 2835 |
. . . . 5
β’ ((π β§ π΄ = π) β π β (π΄πΌπ΄)) |
12 | | oveq2 7366 |
. . . . . . . 8
β’ (π = π΄ β (π β π) = (π β π΄)) |
13 | 12 | eqeq1d 2735 |
. . . . . . 7
β’ (π = π΄ β ((π β π) = (π β π΄) β (π β π΄) = (π β π΄))) |
14 | | oveq1 7365 |
. . . . . . . 8
β’ (π = π΄ β (ππΌπ΄) = (π΄πΌπ΄)) |
15 | 14 | eleq2d 2820 |
. . . . . . 7
β’ (π = π΄ β (π β (ππΌπ΄) β π β (π΄πΌπ΄))) |
16 | 13, 15 | anbi12d 632 |
. . . . . 6
β’ (π = π΄ β (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β ((π β π΄) = (π β π΄) β§ π β (π΄πΌπ΄)))) |
17 | 16 | rspcev 3580 |
. . . . 5
β’ ((π΄ β π β§ ((π β π΄) = (π β π΄) β§ π β (π΄πΌπ΄))) β βπ β π ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) |
18 | 2, 3, 11, 17 | syl12anc 836 |
. . . 4
β’ ((π β§ π΄ = π) β βπ β π ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) |
19 | 8 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β πΊ β TarskiG) |
20 | | mirreu.m |
. . . . . . . . 9
β’ (π β π β π) |
21 | 20 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π β π) |
22 | | simplrl 776 |
. . . . . . . 8
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π β π) |
23 | | simprll 778 |
. . . . . . . . 9
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β (π β π) = (π β π΄)) |
24 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π΄ = π) |
25 | 24 | oveq2d 7374 |
. . . . . . . . 9
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β (π β π΄) = (π β π)) |
26 | 23, 25 | eqtrd 2773 |
. . . . . . . 8
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β (π β π) = (π β π)) |
27 | 5, 6, 7, 19, 21, 22, 21, 26 | axtgcgrid 27447 |
. . . . . . 7
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π = π) |
28 | | simplrr 777 |
. . . . . . . 8
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π β π) |
29 | | simprrl 780 |
. . . . . . . . 9
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β (π β π) = (π β π΄)) |
30 | 29, 25 | eqtrd 2773 |
. . . . . . . 8
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β (π β π) = (π β π)) |
31 | 5, 6, 7, 19, 21, 28, 21, 30 | axtgcgrid 27447 |
. . . . . . 7
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π = π) |
32 | 27, 31 | eqtr3d 2775 |
. . . . . 6
β’ ((((π β§ π΄ = π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π = π) |
33 | 32 | ex 414 |
. . . . 5
β’ (((π β§ π΄ = π) β§ (π β π β§ π β π)) β ((((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) β π = π)) |
34 | 33 | ralrimivva 3194 |
. . . 4
β’ ((π β§ π΄ = π) β βπ β π βπ β π ((((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) β π = π)) |
35 | 18, 34 | jca 513 |
. . 3
β’ ((π β§ π΄ = π) β (βπ β π ((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ βπ β π βπ β π ((((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) β π = π))) |
36 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β π) β πΊ β TarskiG) |
37 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β π) β π΄ β π) |
38 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β π) β π β π) |
39 | 5, 6, 7, 36, 37, 38, 38, 37 | axtgsegcon 27448 |
. . . . 5
β’ ((π β§ π΄ β π) β βπ β π (π β (π΄πΌπ) β§ (π β π) = (π β π΄))) |
40 | | ancom 462 |
. . . . . . . 8
β’ ((π β (π΄πΌπ) β§ (π β π) = (π β π΄)) β ((π β π) = (π β π΄) β§ π β (π΄πΌπ))) |
41 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β πΊ β TarskiG) |
42 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π΄ β π) |
43 | 20 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
44 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
45 | 5, 6, 7, 41, 42, 43, 44 | tgbtwncomb 27473 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π β (π΄πΌπ) β π β (ππΌπ΄))) |
46 | 45 | anbi2d 630 |
. . . . . . . 8
β’ ((π β§ π β π) β (((π β π) = (π β π΄) β§ π β (π΄πΌπ)) β ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) |
47 | 40, 46 | bitrid 283 |
. . . . . . 7
β’ ((π β§ π β π) β ((π β (π΄πΌπ) β§ (π β π) = (π β π΄)) β ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) |
48 | 47 | rexbidva 3170 |
. . . . . 6
β’ (π β (βπ β π (π β (π΄πΌπ) β§ (π β π) = (π β π΄)) β βπ β π ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) |
49 | 48 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ β π) β (βπ β π (π β (π΄πΌπ) β§ (π β π) = (π β π΄)) β βπ β π ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) |
50 | 39, 49 | mpbid 231 |
. . . 4
β’ ((π β§ π΄ β π) β βπ β π ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) |
51 | 8 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β πΊ β TarskiG) |
52 | 20 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π β π) |
53 | 1 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π΄ β π) |
54 | | simplrl 776 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π β π) |
55 | | simplrr 777 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π β π) |
56 | | simpllr 775 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π΄ β π) |
57 | | simprlr 779 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π β (ππΌπ΄)) |
58 | 5, 6, 7, 51, 54, 52, 53, 57 | tgbtwncom 27472 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π β (π΄πΌπ)) |
59 | | simprrr 781 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π β (ππΌπ΄)) |
60 | 5, 6, 7, 51, 55, 52, 53, 59 | tgbtwncom 27472 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π β (π΄πΌπ)) |
61 | | simprll 778 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β (π β π) = (π β π΄)) |
62 | | simprrl 780 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β (π β π) = (π β π΄)) |
63 | 5, 6, 7, 51, 52, 52, 53, 53, 54, 55, 56, 58, 60, 61, 62 | tgsegconeq 27470 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π β π β§ π β π)) β§ (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) β π = π) |
64 | 63 | ex 414 |
. . . . 5
β’ (((π β§ π΄ β π) β§ (π β π β§ π β π)) β ((((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) β π = π)) |
65 | 64 | ralrimivva 3194 |
. . . 4
β’ ((π β§ π΄ β π) β βπ β π βπ β π ((((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) β π = π)) |
66 | 50, 65 | jca 513 |
. . 3
β’ ((π β§ π΄ β π) β (βπ β π ((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ βπ β π βπ β π ((((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) β π = π))) |
67 | 35, 66 | pm2.61dane 3029 |
. 2
β’ (π β (βπ β π ((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ βπ β π βπ β π ((((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) β π = π))) |
68 | | oveq2 7366 |
. . . . 5
β’ (π = π β (π β π) = (π β π)) |
69 | 68 | eqeq1d 2735 |
. . . 4
β’ (π = π β ((π β π) = (π β π΄) β (π β π) = (π β π΄))) |
70 | | oveq1 7365 |
. . . . 5
β’ (π = π β (ππΌπ΄) = (ππΌπ΄)) |
71 | 70 | eleq2d 2820 |
. . . 4
β’ (π = π β (π β (ππΌπ΄) β π β (ππΌπ΄))) |
72 | 69, 71 | anbi12d 632 |
. . 3
β’ (π = π β (((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β ((π β π) = (π β π΄) β§ π β (ππΌπ΄)))) |
73 | 72 | reu4 3690 |
. 2
β’
(β!π β
π ((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β (βπ β π ((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ βπ β π βπ β π ((((π β π) = (π β π΄) β§ π β (ππΌπ΄)) β§ ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) β π = π))) |
74 | 67, 73 | sylibr 233 |
1
β’ (π β β!π β π ((π β π) = (π β π΄) β§ π β (ππΌπ΄))) |