Step | Hyp | Ref
| Expression |
1 | | 2z 12542 |
. . . 4
β’ 2 β
β€ |
2 | | uzid 12785 |
. . . 4
β’ (2 β
β€ β 2 β (β€β₯β2)) |
3 | 1, 2 | ax-mp 5 |
. . 3
β’ 2 β
(β€β₯β2) |
4 | | istrkg.p |
. . . 4
β’ π = (BaseβπΊ) |
5 | | istrkg.d |
. . . 4
β’ β =
(distβπΊ) |
6 | | istrkg.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
7 | 4, 5, 6 | istrkgld 27443 |
. . 3
β’ ((πΊ β π β§ 2 β
(β€β₯β2)) β (πΊDimTarskiGβ₯2 β
βπ(π:(1..^2)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
8 | 3, 7 | mpan2 690 |
. 2
β’ (πΊ β π β (πΊDimTarskiGβ₯2 β
βπ(π:(1..^2)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
9 | | r19.41v 3186 |
. . . . 5
β’
(βπ₯ β
π (βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β§ π:(1..^2)β1-1βπ) β (βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β§ π:(1..^2)β1-1βπ)) |
10 | | ancom 462 |
. . . . . 6
β’
((βπ¦ β
π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β§ π:(1..^2)β1-1βπ) β (π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
11 | 10 | rexbii 3098 |
. . . . 5
β’
(βπ₯ β
π (βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β§ π:(1..^2)β1-1βπ) β βπ₯ β π (π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
12 | | ancom 462 |
. . . . 5
β’
((βπ₯ β
π βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β§ π:(1..^2)β1-1βπ) β (π:(1..^2)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
13 | 9, 11, 12 | 3bitr3ri 302 |
. . . 4
β’ ((π:(1..^2)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ₯ β π (π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
14 | 13 | exbii 1851 |
. . 3
β’
(βπ(π:(1..^2)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπβπ₯ β π (π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
15 | | rexcom4 3274 |
. . 3
β’
(βπ₯ β
π βπ(π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπβπ₯ β π (π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
16 | | simpr 486 |
. . . . . . . . . 10
β’
((βπ β
(2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
17 | 16 | reximi 3088 |
. . . . . . . . 9
β’
(βπ§ β
π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
18 | 17 | reximi 3088 |
. . . . . . . 8
β’
(βπ¦ β
π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
19 | 18 | adantl 483 |
. . . . . . 7
β’ ((π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
20 | 19 | exlimiv 1934 |
. . . . . 6
β’
(βπ(π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
21 | 20 | adantl 483 |
. . . . 5
β’ ((π₯ β π β§ βπ(π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) β βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
22 | | 1ex 11158 |
. . . . . . . . . 10
β’ 1 β
V |
23 | | vex 3452 |
. . . . . . . . . 10
β’ π₯ β V |
24 | 22, 23 | f1osn 6829 |
. . . . . . . . 9
β’ {β¨1,
π₯β©}:{1}β1-1-ontoβ{π₯} |
25 | | f1of1 6788 |
. . . . . . . . 9
β’
({β¨1, π₯β©}:{1}β1-1-ontoβ{π₯} β {β¨1, π₯β©}:{1}β1-1β{π₯}) |
26 | 24, 25 | mp1i 13 |
. . . . . . . 8
β’ (π₯ β π β {β¨1, π₯β©}:{1}β1-1β{π₯}) |
27 | | snssi 4773 |
. . . . . . . 8
β’ (π₯ β π β {π₯} β π) |
28 | | f1ss 6749 |
. . . . . . . 8
β’
(({β¨1, π₯β©}:{1}β1-1β{π₯} β§ {π₯} β π) β {β¨1, π₯β©}:{1}β1-1βπ) |
29 | 26, 27, 28 | syl2anc 585 |
. . . . . . 7
β’ (π₯ β π β {β¨1, π₯β©}:{1}β1-1βπ) |
30 | | fzo12sn 13662 |
. . . . . . . . . . . 12
β’ (1..^2) =
{1} |
31 | 30 | mpteq1i 5206 |
. . . . . . . . . . 11
β’ (π β (1..^2) β¦ π₯) = (π β {1} β¦ π₯) |
32 | | fmptsn 7118 |
. . . . . . . . . . . 12
β’ ((1
β V β§ π₯ β V)
β {β¨1, π₯β©} =
(π β {1} β¦ π₯)) |
33 | 22, 23, 32 | mp2an 691 |
. . . . . . . . . . 11
β’ {β¨1,
π₯β©} = (π β {1} β¦ π₯) |
34 | 31, 33 | eqtr4i 2768 |
. . . . . . . . . 10
β’ (π β (1..^2) β¦ π₯) = {β¨1, π₯β©} |
35 | 34 | a1i 11 |
. . . . . . . . 9
β’ (β€
β (π β (1..^2)
β¦ π₯) = {β¨1,
π₯β©}) |
36 | 30 | a1i 11 |
. . . . . . . . 9
β’ (β€
β (1..^2) = {1}) |
37 | | eqidd 2738 |
. . . . . . . . 9
β’ (β€
β π = π) |
38 | 35, 36, 37 | f1eq123d 6781 |
. . . . . . . 8
β’ (β€
β ((π β (1..^2)
β¦ π₯):(1..^2)β1-1βπ β {β¨1, π₯β©}:{1}β1-1βπ)) |
39 | 38 | mptru 1549 |
. . . . . . 7
β’ ((π β (1..^2) β¦ π₯):(1..^2)β1-1βπ β {β¨1, π₯β©}:{1}β1-1βπ) |
40 | 29, 39 | sylibr 233 |
. . . . . 6
β’ (π₯ β π β (π β (1..^2) β¦ π₯):(1..^2)β1-1βπ) |
41 | | ral0 4475 |
. . . . . . . . . 10
β’
βπ β
β
((((π β
(1..^2) β¦ π₯)β1)
β
π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) |
42 | | fzo0 13603 |
. . . . . . . . . . 11
β’ (2..^2) =
β
|
43 | 42 | raleqi 3314 |
. . . . . . . . . 10
β’
(βπ β
(2..^2)((((π β (1..^2)
β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) β βπ β β
((((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§))) |
44 | 41, 43 | mpbir 230 |
. . . . . . . . 9
β’
βπ β
(2..^2)((((π β (1..^2)
β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) |
45 | 44 | jctl 525 |
. . . . . . . 8
β’ (Β¬
(π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β (βπ β (2..^2)((((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
46 | 45 | reximi 3088 |
. . . . . . 7
β’
(βπ§ β
π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β βπ§ β π (βπ β (2..^2)((((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
47 | 46 | reximi 3088 |
. . . . . 6
β’
(βπ¦ β
π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β βπ¦ β π βπ§ β π (βπ β (2..^2)((((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
48 | | ovex 7395 |
. . . . . . . 8
β’ (1..^2)
β V |
49 | 48 | mptex 7178 |
. . . . . . 7
β’ (π β (1..^2) β¦ π₯) β V |
50 | | f1eq1 6738 |
. . . . . . . 8
β’ (π = (π β (1..^2) β¦ π₯) β (π:(1..^2)β1-1βπ β (π β (1..^2) β¦ π₯):(1..^2)β1-1βπ)) |
51 | | nfmpt1 5218 |
. . . . . . . . . . . . 13
β’
β²π(π β (1..^2) β¦ π₯) |
52 | 51 | nfeq2 2925 |
. . . . . . . . . . . 12
β’
β²π π = (π β (1..^2) β¦ π₯) |
53 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π(π¦ β π β§ π§ β π) |
54 | 52, 53 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π(π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) |
55 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β π = (π β (1..^2) β¦ π₯)) |
56 | 55 | fveq1d 6849 |
. . . . . . . . . . . . . 14
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β (πβ1) = ((π β (1..^2) β¦ π₯)β1)) |
57 | 56 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β ((πβ1) β π₯) = (((π β (1..^2) β¦ π₯)β1) β π₯)) |
58 | 55 | fveq1d 6849 |
. . . . . . . . . . . . . 14
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β (πβπ) = ((π β (1..^2) β¦ π₯)βπ)) |
59 | 58 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β ((πβπ) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯)) |
60 | 57, 59 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β (((πβ1) β π₯) = ((πβπ) β π₯) β (((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯))) |
61 | 56 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β ((πβ1) β π¦) = (((π β (1..^2) β¦ π₯)β1) β π¦)) |
62 | 58 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β ((πβπ) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦)) |
63 | 61, 62 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β (((πβ1) β π¦) = ((πβπ) β π¦) β (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦))) |
64 | 56 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β ((πβ1) β π§) = (((π β (1..^2) β¦ π₯)β1) β π§)) |
65 | 58 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β ((πβπ) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) |
66 | 64, 65 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β (((πβ1) β π§) = ((πβπ) β π§) β (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§))) |
67 | 60, 63, 66 | 3anbi123d 1437 |
. . . . . . . . . . 11
β’ (((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β§ π β (2..^2)) β ((((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β ((((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)))) |
68 | 54, 67 | ralbida 3256 |
. . . . . . . . . 10
β’ ((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β βπ β (2..^2)((((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)))) |
69 | 68 | anbi1d 631 |
. . . . . . . . 9
β’ ((π = (π β (1..^2) β¦ π₯) β§ (π¦ β π β§ π§ β π)) β ((βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β (βπ β (2..^2)((((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
70 | 69 | 2rexbidva 3212 |
. . . . . . . 8
β’ (π = (π β (1..^2) β¦ π₯) β (βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ¦ β π βπ§ β π (βπ β (2..^2)((((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
71 | 50, 70 | anbi12d 632 |
. . . . . . 7
β’ (π = (π β (1..^2) β¦ π₯) β ((π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β ((π β (1..^2) β¦ π₯):(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)((((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
72 | 49, 71 | spcev 3568 |
. . . . . 6
β’ (((π β (1..^2) β¦ π₯):(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)((((π β (1..^2) β¦ π₯)β1) β π₯) = (((π β (1..^2) β¦ π₯)βπ) β π₯) β§ (((π β (1..^2) β¦ π₯)β1) β π¦) = (((π β (1..^2) β¦ π₯)βπ) β π¦) β§ (((π β (1..^2) β¦ π₯)β1) β π§) = (((π β (1..^2) β¦ π₯)βπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ(π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
73 | 40, 47, 72 | syl2an 597 |
. . . . 5
β’ ((π₯ β π β§ βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ(π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
74 | 21, 73 | impbida 800 |
. . . 4
β’ (π₯ β π β (βπ(π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
75 | 74 | rexbiia 3096 |
. . 3
β’
(βπ₯ β
π βπ(π:(1..^2)β1-1βπ β§ βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
76 | 14, 15, 75 | 3bitr2i 299 |
. 2
β’
(βπ(π:(1..^2)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^2)(((πβ1) β π₯) = ((πβπ) β π₯) β§ ((πβ1) β π¦) = ((πβπ) β π¦) β§ ((πβ1) β π§) = ((πβπ) β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) |
77 | 8, 76 | bitrdi 287 |
1
β’ (πΊ β π β (πΊDimTarskiGβ₯2 β
βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |