Step | Hyp | Ref
| Expression |
1 | | 3z 12541 |
. . . 4
β’ 3 β
β€ |
2 | | 2re 12232 |
. . . . 5
β’ 2 β
β |
3 | | 3re 12238 |
. . . . 5
β’ 3 β
β |
4 | | 2lt3 12330 |
. . . . 5
β’ 2 <
3 |
5 | 2, 3, 4 | ltleii 11283 |
. . . 4
β’ 2 β€
3 |
6 | | 2z 12540 |
. . . . 5
β’ 2 β
β€ |
7 | 6 | eluz1i 12776 |
. . . 4
β’ (3 β
(β€β₯β2) β (3 β β€ β§ 2 β€
3)) |
8 | 1, 5, 7 | mpbir2an 710 |
. . 3
β’ 3 β
(β€β₯β2) |
9 | | istrkg.p |
. . . 4
β’ π = (BaseβπΊ) |
10 | | istrkg.d |
. . . 4
β’ β =
(distβπΊ) |
11 | | istrkg.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
12 | 9, 10, 11 | istrkgld 27443 |
. . 3
β’ ((πΊ β π β§ 3 β
(β€β₯β2)) β (πΊDimTarskiGβ₯3 β
βπ(π:(1..^3)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
13 | 8, 12 | mpan2 690 |
. 2
β’ (πΊ β π β (πΊDimTarskiGβ₯3 β
βπ(π:(1..^3)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
14 | | fzo13pr 13662 |
. . . . . 6
β’ (1..^3) =
{1, 2} |
15 | | f1eq2 6735 |
. . . . . 6
β’ ((1..^3)
= {1, 2} β (π:(1..^3)β1-1βπ β π:{1, 2}β1-1βπ)) |
16 | 14, 15 | ax-mp 5 |
. . . . 5
β’ (π:(1..^3)β1-1βπ β π:{1, 2}β1-1βπ) |
17 | 16 | anbi1i 625 |
. . . 4
β’ ((π:(1..^3)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β (π:{1, 2}β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
18 | 17 | exbii 1851 |
. . 3
β’
(βπ(π:(1..^3)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ(π:{1, 2}β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
19 | 18 | a1i 11 |
. 2
β’ (πΊ β π β (βπ(π:(1..^3)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ(π:{1, 2}β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
20 | | 1z 12538 |
. . . 4
β’ 1 β
β€ |
21 | | 1ne2 12366 |
. . . 4
β’ 1 β
2 |
22 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π’ = (πβ1) β (π’ β π₯) = ((πβ1) β π₯)) |
23 | 22 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π’ = (πβ1) β ((π’ β π₯) = (π£ β π₯) β ((πβ1) β π₯) = (π£ β π₯))) |
24 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π’ = (πβ1) β (π’ β π¦) = ((πβ1) β π¦)) |
25 | 24 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π’ = (πβ1) β ((π’ β π¦) = (π£ β π¦) β ((πβ1) β π¦) = (π£ β π¦))) |
26 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π’ = (πβ1) β (π’ β π§) = ((πβ1) β π§)) |
27 | 26 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π’ = (πβ1) β ((π’ β π§) = (π£ β π§) β ((πβ1) β π§) = (π£ β π§))) |
28 | 23, 25, 27 | 3anbi123d 1437 |
. . . . . . . 8
β’ (π’ = (πβ1) β (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β (((πβ1) β π₯) = (π£ β π₯) β§ ((πβ1) β π¦) = (π£ β π¦) β§ ((πβ1) β π§) = (π£ β π§)))) |
29 | 28 | anbi1d 631 |
. . . . . . 7
β’ (π’ = (πβ1) β ((((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β ((((πβ1) β π₯) = (π£ β π₯) β§ ((πβ1) β π¦) = (π£ β π¦) β§ ((πβ1) β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
30 | 29 | rexbidv 3172 |
. . . . . 6
β’ (π’ = (πβ1) β (βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ§ β π ((((πβ1) β π₯) = (π£ β π₯) β§ ((πβ1) β π¦) = (π£ β π¦) β§ ((πβ1) β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
31 | 30 | 2rexbidv 3210 |
. . . . 5
β’ (π’ = (πβ1) β (βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ₯ β π βπ¦ β π βπ§ β π ((((πβ1) β π₯) = (π£ β π₯) β§ ((πβ1) β π¦) = (π£ β π¦) β§ ((πβ1) β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
32 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π£ = (πβ2) β (π£ β π₯) = ((πβ2) β π₯)) |
33 | 32 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π£ = (πβ2) β (((πβ1) β π₯) = (π£ β π₯) β ((πβ1) β π₯) = ((πβ2) β π₯))) |
34 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π£ = (πβ2) β (π£ β π¦) = ((πβ2) β π¦)) |
35 | 34 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π£ = (πβ2) β (((πβ1) β π¦) = (π£ β π¦) β ((πβ1) β π¦) = ((πβ2) β π¦))) |
36 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π£ = (πβ2) β (π£ β π§) = ((πβ2) β π§)) |
37 | 36 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π£ = (πβ2) β (((πβ1) β π§) = (π£ β π§) β ((πβ1) β π§) = ((πβ2) β π§))) |
38 | 33, 35, 37 | 3anbi123d 1437 |
. . . . . . . . 9
β’ (π£ = (πβ2) β ((((πβ1) β π₯) = (π£ β π₯) β§ ((πβ1) β π¦) = (π£ β π¦) β§ ((πβ1) β π§) = (π£ β π§)) β (((πβ1) β π₯) = ((πβ2) β π₯) β§ ((πβ1) β π¦) = ((πβ2) β π¦) β§ ((πβ1) β π§) = ((πβ2) β π§)))) |
39 | | 2p1e3 12300 |
. . . . . . . . . . . . 13
β’ (2 + 1) =
3 |
40 | 39 | oveq2i 7369 |
. . . . . . . . . . . 12
β’ (2..^(2 +
1)) = (2..^3) |
41 | | fzosn 13649 |
. . . . . . . . . . . . 13
β’ (2 β
β€ β (2..^(2 + 1)) = {2}) |
42 | 6, 41 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (2..^(2 +
1)) = {2} |
43 | 40, 42 | eqtr3i 2763 |
. . . . . . . . . . 11
β’ (2..^3) =
{2} |
44 | 43 | raleqi 3310 |
. . . . . . . . . 10
β’
(βπ β
(2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β βπ β {2} (((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§))) |
45 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
β’ (π = 2 β (πβπ) = (πβ2)) |
46 | 45 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π = 2 β ((πβπ) β π₯) = ((πβ2) β π₯)) |
47 | 46 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π = 2 β (((πβ1) β π₯) = ((πβπ) β π₯) β ((πβ1) β π₯) = ((πβ2) β π₯))) |
48 | 45 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π = 2 β ((πβπ) β π¦) = ((πβ2) β π¦)) |
49 | 48 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π = 2 β (((πβ1) β π¦) = ((πβπ) β π¦) β ((πβ1) β π¦) = ((πβ2) β π¦))) |
50 | 45 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π = 2 β ((πβπ) β π§) = ((πβ2) β π§)) |
51 | 50 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π = 2 β (((πβ1) β π§) = ((πβπ) β π§) β ((πβ1) β π§) = ((πβ2) β π§))) |
52 | 47, 49, 51 | 3anbi123d 1437 |
. . . . . . . . . . . 12
β’ (π = 2 β ((((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β (((πβ1) β π₯) = ((πβ2) β π₯) β§ ((πβ1) β π¦) = ((πβ2) β π¦) β§ ((πβ1) β π§) = ((πβ2) β π§)))) |
53 | 52 | ralsng 4635 |
. . . . . . . . . . 11
β’ (2 β
β€ β (βπ
β {2} (((πβ1)
β
π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β (((πβ1) β π₯) = ((πβ2) β π₯) β§ ((πβ1) β π¦) = ((πβ2) β π¦) β§ ((πβ1) β π§) = ((πβ2) β π§)))) |
54 | 6, 53 | ax-mp 5 |
. . . . . . . . . 10
β’
(βπ β
{2} (((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β (((πβ1) β π₯) = ((πβ2) β π₯) β§ ((πβ1) β π¦) = ((πβ2) β π¦) β§ ((πβ1) β π§) = ((πβ2) β π§))) |
55 | 44, 54 | bitri 275 |
. . . . . . . . 9
β’
(βπ β
(2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β (((πβ1) β π₯) = ((πβ2) β π₯) β§ ((πβ1) β π¦) = ((πβ2) β π¦) β§ ((πβ1) β π§) = ((πβ2) β π§))) |
56 | 38, 55 | bitr4di 289 |
. . . . . . . 8
β’ (π£ = (πβ2) β ((((πβ1) β π₯) = (π£ β π₯) β§ ((πβ1) β π¦) = (π£ β π¦) β§ ((πβ1) β π§) = (π£ β π§)) β βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)))) |
57 | 56 | anbi1d 631 |
. . . . . . 7
β’ (π£ = (πβ2) β (((((πβ1) β π₯) = (π£ β π₯) β§ ((πβ1) β π¦) = (π£ β π¦) β§ ((πβ1) β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
58 | 57 | rexbidv 3172 |
. . . . . 6
β’ (π£ = (πβ2) β (βπ§ β π ((((πβ1) β π₯) = (π£ β π₯) β§ ((πβ1) β π¦) = (π£ β π¦) β§ ((πβ1) β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
59 | 58 | 2rexbidv 3210 |
. . . . 5
β’ (π£ = (πβ2) β (βπ₯ β π βπ¦ β π βπ§ β π ((((πβ1) β π₯) = (π£ β π₯) β§ ((πβ1) β π¦) = (π£ β π¦) β§ ((πβ1) β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
60 | 31, 59 | f1prex 7231 |
. . . 4
β’ ((1
β β€ β§ 2 β β€ β§ 1 β 2) β (βπ(π:{1, 2}β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ’ β π βπ£ β π (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
61 | 20, 6, 21, 60 | mp3an 1462 |
. . 3
β’
(βπ(π:{1, 2}β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ’ β π βπ£ β π (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
62 | 61 | a1i 11 |
. 2
β’ (πΊ β π β (βπ(π:{1, 2}β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^3)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ’ β π βπ£ β π (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
63 | 13, 19, 62 | 3bitrd 305 |
1
β’ (πΊ β π β (πΊDimTarskiGβ₯3 β
βπ’ β π βπ£ β π (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |