Step | Hyp | Ref
| Expression |
1 | | axtgupdim2ALTV.1 |
. . 3
β’ (π β (π β π) = (π β π)) |
2 | | axtgupdim2ALTV.2 |
. . 3
β’ (π β (π β π) = (π β π)) |
3 | | axtgupdim2ALTV.3 |
. . 3
β’ (π β (π β π) = (π β π)) |
4 | 1, 2, 3 | 3jca 1129 |
. 2
β’ (π β ((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π))) |
5 | | axtgupdim2ALTV.0 |
. 2
β’ (π β π β π) |
6 | | axtgupdim2ALTV.g |
. . . . . 6
β’ (π β πΊ β
TarskiG2D) |
7 | | istrkg2d.p |
. . . . . . 7
β’ π = (BaseβπΊ) |
8 | | istrkg2d.d |
. . . . . . 7
β’ β =
(distβπΊ) |
9 | | istrkg2d.i |
. . . . . . 7
β’ πΌ = (ItvβπΊ) |
10 | 7, 8, 9 | istrkg2d 33678 |
. . . . . 6
β’ (πΊ β TarskiG2D
β (πΊ β V β§
(βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ β π’) = (π₯ β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
11 | 6, 10 | sylib 217 |
. . . . 5
β’ (π β (πΊ β V β§ (βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ β π’) = (π₯ β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
12 | 11 | simprrd 773 |
. . . 4
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ β π’) = (π₯ β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
13 | | axtgupdim2ALTV.x |
. . . . 5
β’ (π β π β π) |
14 | | axtgupdim2ALTV.y |
. . . . 5
β’ (π β π β π) |
15 | | axtgupdim2ALTV.z |
. . . . 5
β’ (π β π β π) |
16 | | oveq1 7416 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯ β π’) = (π β π’)) |
17 | | oveq1 7416 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯ β π£) = (π β π£)) |
18 | 16, 17 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π₯ = π β ((π₯ β π’) = (π₯ β π£) β (π β π’) = (π β π£))) |
19 | 18 | 3anbi1d 1441 |
. . . . . . . . 9
β’ (π₯ = π β (((π₯ β π’) = (π₯ β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β ((π β π’) = (π β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)))) |
20 | 19 | anbi1d 631 |
. . . . . . . 8
β’ (π₯ = π β ((((π₯ β π’) = (π₯ β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (((π β π’) = (π β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£))) |
21 | | oveq1 7416 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯πΌπ¦) = (ππΌπ¦)) |
22 | 21 | eleq2d 2820 |
. . . . . . . . 9
β’ (π₯ = π β (π§ β (π₯πΌπ¦) β π§ β (ππΌπ¦))) |
23 | | eleq1 2822 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ β (π§πΌπ¦) β π β (π§πΌπ¦))) |
24 | | oveq1 7416 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯πΌπ§) = (ππΌπ§)) |
25 | 24 | eleq2d 2820 |
. . . . . . . . 9
β’ (π₯ = π β (π¦ β (π₯πΌπ§) β π¦ β (ππΌπ§))) |
26 | 22, 23, 25 | 3orbi123d 1436 |
. . . . . . . 8
β’ (π₯ = π β ((π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§)))) |
27 | 20, 26 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = π β (((((π₯ β π’) = (π₯ β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β ((((π β π’) = (π β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§))))) |
28 | 27 | 2ralbidv 3219 |
. . . . . 6
β’ (π₯ = π β (βπ’ β π βπ£ β π ((((π₯ β π’) = (π₯ β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ’ β π βπ£ β π ((((π β π’) = (π β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§))))) |
29 | | oveq1 7416 |
. . . . . . . . . . 11
β’ (π¦ = π β (π¦ β π’) = (π β π’)) |
30 | | oveq1 7416 |
. . . . . . . . . . 11
β’ (π¦ = π β (π¦ β π£) = (π β π£)) |
31 | 29, 30 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π¦ = π β ((π¦ β π’) = (π¦ β π£) β (π β π’) = (π β π£))) |
32 | 31 | 3anbi2d 1442 |
. . . . . . . . 9
β’ (π¦ = π β (((π β π’) = (π β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β ((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π§ β π’) = (π§ β π£)))) |
33 | 32 | anbi1d 631 |
. . . . . . . 8
β’ (π¦ = π β ((((π β π’) = (π β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£))) |
34 | | oveq2 7417 |
. . . . . . . . . 10
β’ (π¦ = π β (ππΌπ¦) = (ππΌπ)) |
35 | 34 | eleq2d 2820 |
. . . . . . . . 9
β’ (π¦ = π β (π§ β (ππΌπ¦) β π§ β (ππΌπ))) |
36 | | oveq2 7417 |
. . . . . . . . . 10
β’ (π¦ = π β (π§πΌπ¦) = (π§πΌπ)) |
37 | 36 | eleq2d 2820 |
. . . . . . . . 9
β’ (π¦ = π β (π β (π§πΌπ¦) β π β (π§πΌπ))) |
38 | | eleq1 2822 |
. . . . . . . . 9
β’ (π¦ = π β (π¦ β (ππΌπ§) β π β (ππΌπ§))) |
39 | 35, 37, 38 | 3orbi123d 1436 |
. . . . . . . 8
β’ (π¦ = π β ((π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§)) β (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§)))) |
40 | 33, 39 | imbi12d 345 |
. . . . . . 7
β’ (π¦ = π β (((((π β π’) = (π β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§))) β ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))))) |
41 | 40 | 2ralbidv 3219 |
. . . . . 6
β’ (π¦ = π β (βπ’ β π βπ£ β π ((((π β π’) = (π β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§))) β βπ’ β π βπ£ β π ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))))) |
42 | | oveq1 7416 |
. . . . . . . . . . 11
β’ (π§ = π β (π§ β π’) = (π β π’)) |
43 | | oveq1 7416 |
. . . . . . . . . . 11
β’ (π§ = π β (π§ β π£) = (π β π£)) |
44 | 42, 43 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π§ = π β ((π§ β π’) = (π§ β π£) β (π β π’) = (π β π£))) |
45 | 44 | 3anbi3d 1443 |
. . . . . . . . 9
β’ (π§ = π β (((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π§ β π’) = (π§ β π£)) β ((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)))) |
46 | 45 | anbi1d 631 |
. . . . . . . 8
β’ (π§ = π β ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β§ π’ β π£))) |
47 | | eleq1 2822 |
. . . . . . . . 9
β’ (π§ = π β (π§ β (ππΌπ) β π β (ππΌπ))) |
48 | | oveq1 7416 |
. . . . . . . . . 10
β’ (π§ = π β (π§πΌπ) = (ππΌπ)) |
49 | 48 | eleq2d 2820 |
. . . . . . . . 9
β’ (π§ = π β (π β (π§πΌπ) β π β (ππΌπ))) |
50 | | oveq2 7417 |
. . . . . . . . . 10
β’ (π§ = π β (ππΌπ§) = (ππΌπ)) |
51 | 50 | eleq2d 2820 |
. . . . . . . . 9
β’ (π§ = π β (π β (ππΌπ§) β π β (ππΌπ))) |
52 | 47, 49, 51 | 3orbi123d 1436 |
. . . . . . . 8
β’ (π§ = π β ((π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§)) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
53 | 46, 52 | imbi12d 345 |
. . . . . . 7
β’ (π§ = π β (((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))) β ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β§ π’ β π£) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
54 | 53 | 2ralbidv 3219 |
. . . . . 6
β’ (π§ = π β (βπ’ β π βπ£ β π ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))) β βπ’ β π βπ£ β π ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β§ π’ β π£) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
55 | 28, 41, 54 | rspc3v 3628 |
. . . . 5
β’ ((π β π β§ π β π β§ π β π) β (βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ β π’) = (π₯ β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ’ β π βπ£ β π ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β§ π’ β π£) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
56 | 13, 14, 15, 55 | syl3anc 1372 |
. . . 4
β’ (π β (βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ β π’) = (π₯ β π£) β§ (π¦ β π’) = (π¦ β π£) β§ (π§ β π’) = (π§ β π£)) β§ π’ β π£) β (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ’ β π βπ£ β π ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β§ π’ β π£) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
57 | 12, 56 | mpd 15 |
. . 3
β’ (π β βπ’ β π βπ£ β π ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β§ π’ β π£) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
58 | | axtgupdim2ALTV.u |
. . . 4
β’ (π β π β π) |
59 | | axtgupdim2ALTV.v |
. . . 4
β’ (π β π β π) |
60 | | oveq2 7417 |
. . . . . . . . 9
β’ (π’ = π β (π β π’) = (π β π)) |
61 | 60 | eqeq1d 2735 |
. . . . . . . 8
β’ (π’ = π β ((π β π’) = (π β π£) β (π β π) = (π β π£))) |
62 | | oveq2 7417 |
. . . . . . . . 9
β’ (π’ = π β (π β π’) = (π β π)) |
63 | 62 | eqeq1d 2735 |
. . . . . . . 8
β’ (π’ = π β ((π β π’) = (π β π£) β (π β π) = (π β π£))) |
64 | | oveq2 7417 |
. . . . . . . . 9
β’ (π’ = π β (π β π’) = (π β π)) |
65 | 64 | eqeq1d 2735 |
. . . . . . . 8
β’ (π’ = π β ((π β π’) = (π β π£) β (π β π) = (π β π£))) |
66 | 61, 63, 65 | 3anbi123d 1437 |
. . . . . . 7
β’ (π’ = π β (((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β ((π β π) = (π β π£) β§ (π β π) = (π β π£) β§ (π β π) = (π β π£)))) |
67 | | neeq1 3004 |
. . . . . . 7
β’ (π’ = π β (π’ β π£ β π β π£)) |
68 | 66, 67 | anbi12d 632 |
. . . . . 6
β’ (π’ = π β ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β§ π’ β π£) β (((π β π) = (π β π£) β§ (π β π) = (π β π£) β§ (π β π) = (π β π£)) β§ π β π£))) |
69 | 68 | imbi1d 342 |
. . . . 5
β’ (π’ = π β (((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β§ π’ β π£) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) β ((((π β π) = (π β π£) β§ (π β π) = (π β π£) β§ (π β π) = (π β π£)) β§ π β π£) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
70 | | oveq2 7417 |
. . . . . . . . 9
β’ (π£ = π β (π β π£) = (π β π)) |
71 | 70 | eqeq2d 2744 |
. . . . . . . 8
β’ (π£ = π β ((π β π) = (π β π£) β (π β π) = (π β π))) |
72 | | oveq2 7417 |
. . . . . . . . 9
β’ (π£ = π β (π β π£) = (π β π)) |
73 | 72 | eqeq2d 2744 |
. . . . . . . 8
β’ (π£ = π β ((π β π) = (π β π£) β (π β π) = (π β π))) |
74 | | oveq2 7417 |
. . . . . . . . 9
β’ (π£ = π β (π β π£) = (π β π)) |
75 | 74 | eqeq2d 2744 |
. . . . . . . 8
β’ (π£ = π β ((π β π) = (π β π£) β (π β π) = (π β π))) |
76 | 71, 73, 75 | 3anbi123d 1437 |
. . . . . . 7
β’ (π£ = π β (((π β π) = (π β π£) β§ (π β π) = (π β π£) β§ (π β π) = (π β π£)) β ((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)))) |
77 | | neeq2 3005 |
. . . . . . 7
β’ (π£ = π β (π β π£ β π β π)) |
78 | 76, 77 | anbi12d 632 |
. . . . . 6
β’ (π£ = π β ((((π β π) = (π β π£) β§ (π β π) = (π β π£) β§ (π β π) = (π β π£)) β§ π β π£) β (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ π β π))) |
79 | 78 | imbi1d 342 |
. . . . 5
β’ (π£ = π β (((((π β π) = (π β π£) β§ (π β π) = (π β π£) β§ (π β π) = (π β π£)) β§ π β π£) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) β ((((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ π β π) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
80 | 69, 79 | rspc2v 3623 |
. . . 4
β’ ((π β π β§ π β π) β (βπ’ β π βπ£ β π ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β§ π’ β π£) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) β ((((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ π β π) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
81 | 58, 59, 80 | syl2anc 585 |
. . 3
β’ (π β (βπ’ β π βπ£ β π ((((π β π’) = (π β π£) β§ (π β π’) = (π β π£) β§ (π β π’) = (π β π£)) β§ π’ β π£) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) β ((((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ π β π) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
82 | 57, 81 | mpd 15 |
. 2
β’ (π β ((((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ π β π) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
83 | 4, 5, 82 | mp2and 698 |
1
β’ (π β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) |