Step | Hyp | Ref
| Expression |
1 | | tgdim01.x |
. 2
β’ (π β π β π) |
2 | | tgdim01.y |
. 2
β’ (π β π β π) |
3 | | tgdim01.z |
. 2
β’ (π β π β π) |
4 | | tgdim01.1 |
. . . 4
β’ (π β Β¬ πΊDimTarskiGβ₯2) |
5 | | tgdim01.g |
. . . . 5
β’ (π β πΊ β π) |
6 | | tgdim01.p |
. . . . . 6
β’ π = (BaseβπΊ) |
7 | | eqid 2733 |
. . . . . 6
β’
(distβπΊ) =
(distβπΊ) |
8 | | tgdim01.i |
. . . . . 6
β’ πΌ = (ItvβπΊ) |
9 | 6, 7, 8 | istrkg2ld 27444 |
. . . . 5
β’ (πΊ β π β (πΊDimTarskiGβ₯2 β
βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
10 | 5, 9 | syl 17 |
. . . 4
β’ (π β (πΊDimTarskiGβ₯2 β
βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
11 | 4, 10 | mtbid 324 |
. . 3
β’ (π β Β¬ βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
12 | | rexnal3 3130 |
. . . 4
β’
(βπ₯ β
π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β Β¬ βπ₯ β π βπ¦ β π βπ§ β π (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
13 | 12 | con2bii 358 |
. . 3
β’
(βπ₯ β
π βπ¦ β π βπ§ β π (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β Β¬ βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
14 | 11, 13 | sylibr 233 |
. 2
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
15 | | oveq1 7365 |
. . . . . 6
β’ (π₯ = π β (π₯πΌπ¦) = (ππΌπ¦)) |
16 | 15 | eleq2d 2820 |
. . . . 5
β’ (π₯ = π β (π§ β (π₯πΌπ¦) β π§ β (ππΌπ¦))) |
17 | | eleq1 2822 |
. . . . 5
β’ (π₯ = π β (π₯ β (π§πΌπ¦) β π β (π§πΌπ¦))) |
18 | | oveq1 7365 |
. . . . . 6
β’ (π₯ = π β (π₯πΌπ§) = (ππΌπ§)) |
19 | 18 | eleq2d 2820 |
. . . . 5
β’ (π₯ = π β (π¦ β (π₯πΌπ§) β π¦ β (ππΌπ§))) |
20 | 16, 17, 19 | 3orbi123d 1436 |
. . . 4
β’ (π₯ = π β ((π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§)))) |
21 | | oveq2 7366 |
. . . . . 6
β’ (π¦ = π β (ππΌπ¦) = (ππΌπ)) |
22 | 21 | eleq2d 2820 |
. . . . 5
β’ (π¦ = π β (π§ β (ππΌπ¦) β π§ β (ππΌπ))) |
23 | | oveq2 7366 |
. . . . . 6
β’ (π¦ = π β (π§πΌπ¦) = (π§πΌπ)) |
24 | 23 | eleq2d 2820 |
. . . . 5
β’ (π¦ = π β (π β (π§πΌπ¦) β π β (π§πΌπ))) |
25 | | eleq1 2822 |
. . . . 5
β’ (π¦ = π β (π¦ β (ππΌπ§) β π β (ππΌπ§))) |
26 | 22, 24, 25 | 3orbi123d 1436 |
. . . 4
β’ (π¦ = π β ((π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§)) β (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§)))) |
27 | | eleq1 2822 |
. . . . 5
β’ (π§ = π β (π§ β (ππΌπ) β π β (ππΌπ))) |
28 | | oveq1 7365 |
. . . . . 6
β’ (π§ = π β (π§πΌπ) = (ππΌπ)) |
29 | 28 | eleq2d 2820 |
. . . . 5
β’ (π§ = π β (π β (π§πΌπ) β π β (ππΌπ))) |
30 | | oveq2 7366 |
. . . . . 6
β’ (π§ = π β (ππΌπ§) = (ππΌπ)) |
31 | 30 | eleq2d 2820 |
. . . . 5
β’ (π§ = π β (π β (ππΌπ§) β π β (ππΌπ))) |
32 | 27, 29, 31 | 3orbi123d 1436 |
. . . 4
β’ (π§ = π β ((π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§)) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
33 | 20, 26, 32 | rspc3v 3592 |
. . 3
β’ ((π β π β§ π β π β§ π β π) β (βπ₯ β π βπ¦ β π βπ§ β π (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
34 | 33 | imp 408 |
. 2
β’ (((π β π β§ π β π β§ π β π) β§ βπ₯ β π βπ¦ β π βπ§ β π (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) |
35 | 1, 2, 3, 14, 34 | syl31anc 1374 |
1
β’ (π β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) |