Step | Hyp | Ref
| Expression |
1 | | axtgupdim2.1 |
. . 3
β’ (π β (π β π) = (π β π)) |
2 | | axtgupdim2.2 |
. . 3
β’ (π β (π β π) = (π β π)) |
3 | | axtgupdim2.3 |
. . 3
β’ (π β (π β π) = (π β π)) |
4 | | axtgupdim2.0 |
. . . . . . 7
β’ (π β π β π) |
5 | | axtgupdim2.g |
. . . . . . . . . . 11
β’ (π β Β¬ πΊDimTarskiGβ₯3) |
6 | | axtgupdim2.w |
. . . . . . . . . . . 12
β’ (π β πΊ β π) |
7 | | axtrkge.p |
. . . . . . . . . . . . 13
β’ π = (BaseβπΊ) |
8 | | axtrkge.d |
. . . . . . . . . . . . 13
β’ β =
(distβπΊ) |
9 | | axtrkge.i |
. . . . . . . . . . . . 13
β’ πΌ = (ItvβπΊ) |
10 | 7, 8, 9 | istrkg3ld 27445 |
. . . . . . . . . . . 12
β’ (πΊ β π β (πΊDimTarskiGβ₯3 β
βπ’ β π βπ£ β π (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
11 | 6, 10 | syl 17 |
. . . . . . . . . . 11
β’ (π β (πΊDimTarskiGβ₯3 β
βπ’ β π βπ£ β π (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
12 | 5, 11 | mtbid 324 |
. . . . . . . . . 10
β’ (π β Β¬ βπ’ β π βπ£ β π (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
13 | | ralnex2 3127 |
. . . . . . . . . 10
β’
(βπ’ β
π βπ£ β π Β¬ (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β Β¬ βπ’ β π βπ£ β π (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
14 | 12, 13 | sylibr 233 |
. . . . . . . . 9
β’ (π β βπ’ β π βπ£ β π Β¬ (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
15 | | axtgupdim2.u |
. . . . . . . . . 10
β’ (π β π β π) |
16 | | axtgupdim2.v |
. . . . . . . . . 10
β’ (π β π β π) |
17 | | neeq1 3003 |
. . . . . . . . . . . . 13
β’ (π’ = π β (π’ β π£ β π β π£)) |
18 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = π β (π’ β π₯) = (π β π₯)) |
19 | 18 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π β ((π’ β π₯) = (π£ β π₯) β (π β π₯) = (π£ β π₯))) |
20 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = π β (π’ β π¦) = (π β π¦)) |
21 | 20 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π β ((π’ β π¦) = (π£ β π¦) β (π β π¦) = (π£ β π¦))) |
22 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = π β (π’ β π§) = (π β π§)) |
23 | 22 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π β ((π’ β π§) = (π£ β π§) β (π β π§) = (π£ β π§))) |
24 | 19, 21, 23 | 3anbi123d 1437 |
. . . . . . . . . . . . . . . 16
β’ (π’ = π β (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β ((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)))) |
25 | 24 | anbi1d 631 |
. . . . . . . . . . . . . . 15
β’ (π’ = π β ((((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β (((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
26 | 25 | rexbidv 3172 |
. . . . . . . . . . . . . 14
β’ (π’ = π β (βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ§ β π (((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
27 | 26 | 2rexbidv 3210 |
. . . . . . . . . . . . 13
β’ (π’ = π β (βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
28 | 17, 27 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π’ = π β ((π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β (π β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
29 | 28 | notbid 318 |
. . . . . . . . . . 11
β’ (π’ = π β (Β¬ (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β Β¬ (π β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
30 | | neeq2 3004 |
. . . . . . . . . . . . 13
β’ (π£ = π β (π β π£ β π β π)) |
31 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ = π β (π£ β π₯) = (π β π₯)) |
32 | 31 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = π β ((π β π₯) = (π£ β π₯) β (π β π₯) = (π β π₯))) |
33 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ = π β (π£ β π¦) = (π β π¦)) |
34 | 33 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = π β ((π β π¦) = (π£ β π¦) β (π β π¦) = (π β π¦))) |
35 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ = π β (π£ β π§) = (π β π§)) |
36 | 35 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = π β ((π β π§) = (π£ β π§) β (π β π§) = (π β π§))) |
37 | 32, 34, 36 | 3anbi123d 1437 |
. . . . . . . . . . . . . . . 16
β’ (π£ = π β (((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β ((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)))) |
38 | 37 | anbi1d 631 |
. . . . . . . . . . . . . . 15
β’ (π£ = π β ((((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
39 | 38 | rexbidv 3172 |
. . . . . . . . . . . . . 14
β’ (π£ = π β (βπ§ β π (((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
40 | 39 | 2rexbidv 3210 |
. . . . . . . . . . . . 13
β’ (π£ = π β (βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
41 | 30, 40 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π£ = π β ((π β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β (π β π β§ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
42 | 41 | notbid 318 |
. . . . . . . . . . 11
β’ (π£ = π β (Β¬ (π β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π£ β π₯) β§ (π β π¦) = (π£ β π¦) β§ (π β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β Β¬ (π β π β§ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
43 | 29, 42 | rspc2v 3589 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β (βπ’ β π βπ£ β π Β¬ (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β Β¬ (π β π β§ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
44 | 15, 16, 43 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (βπ’ β π βπ£ β π Β¬ (π’ β π£ β§ βπ₯ β π βπ¦ β π βπ§ β π (((π’ β π₯) = (π£ β π₯) β§ (π’ β π¦) = (π£ β π¦) β§ (π’ β π§) = (π£ β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β Β¬ (π β π β§ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))))) |
45 | 14, 44 | mpd 15 |
. . . . . . . 8
β’ (π β Β¬ (π β π β§ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
46 | | imnan 401 |
. . . . . . . 8
β’ ((π β π β Β¬ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) β Β¬ (π β π β§ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
47 | 45, 46 | sylibr 233 |
. . . . . . 7
β’ (π β (π β π β Β¬ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))))) |
48 | 4, 47 | mpd 15 |
. . . . . 6
β’ (π β Β¬ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
49 | | ralnex3 3128 |
. . . . . 6
β’
(βπ₯ β
π βπ¦ β π βπ§ β π Β¬ (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β Β¬ βπ₯ β π βπ¦ β π βπ§ β π (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
50 | 48, 49 | sylibr 233 |
. . . . 5
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π Β¬ (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
51 | | axtgupdim2.x |
. . . . . 6
β’ (π β π β π) |
52 | | axtgupdim2.y |
. . . . . 6
β’ (π β π β π) |
53 | | axtgupdim2.z |
. . . . . 6
β’ (π β π β π) |
54 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π₯ = π β (π β π₯) = (π β π)) |
55 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π₯ = π β (π β π₯) = (π β π)) |
56 | 54, 55 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π₯ = π β ((π β π₯) = (π β π₯) β (π β π) = (π β π))) |
57 | 56 | 3anbi1d 1441 |
. . . . . . . . 9
β’ (π₯ = π β (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β ((π β π) = (π β π) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)))) |
58 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯πΌπ¦) = (ππΌπ¦)) |
59 | 58 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π₯ = π β (π§ β (π₯πΌπ¦) β π§ β (ππΌπ¦))) |
60 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯ β (π§πΌπ¦) β π β (π§πΌπ¦))) |
61 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯πΌπ§) = (ππΌπ§)) |
62 | 61 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π₯ = π β (π¦ β (π₯πΌπ§) β π¦ β (ππΌπ§))) |
63 | 59, 60, 62 | 3orbi123d 1436 |
. . . . . . . . . 10
β’ (π₯ = π β ((π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§)))) |
64 | 63 | notbid 318 |
. . . . . . . . 9
β’ (π₯ = π β (Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)) β Β¬ (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§)))) |
65 | 57, 64 | anbi12d 632 |
. . . . . . . 8
β’ (π₯ = π β ((((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β (((π β π) = (π β π) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§))))) |
66 | 65 | notbid 318 |
. . . . . . 7
β’ (π₯ = π β (Β¬ (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β Β¬ (((π β π) = (π β π) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§))))) |
67 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π¦ = π β (π β π¦) = (π β π)) |
68 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π¦ = π β (π β π¦) = (π β π)) |
69 | 67, 68 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π¦ = π β ((π β π¦) = (π β π¦) β (π β π) = (π β π))) |
70 | 69 | 3anbi2d 1442 |
. . . . . . . . 9
β’ (π¦ = π β (((π β π) = (π β π) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β ((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π§) = (π β π§)))) |
71 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π¦ = π β (ππΌπ¦) = (ππΌπ)) |
72 | 71 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π¦ = π β (π§ β (ππΌπ¦) β π§ β (ππΌπ))) |
73 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π¦ = π β (π§πΌπ¦) = (π§πΌπ)) |
74 | 73 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π¦ = π β (π β (π§πΌπ¦) β π β (π§πΌπ))) |
75 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π¦ = π β (π¦ β (ππΌπ§) β π β (ππΌπ§))) |
76 | 72, 74, 75 | 3orbi123d 1436 |
. . . . . . . . . 10
β’ (π¦ = π β ((π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§)) β (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§)))) |
77 | 76 | notbid 318 |
. . . . . . . . 9
β’ (π¦ = π β (Β¬ (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§)) β Β¬ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§)))) |
78 | 70, 77 | anbi12d 632 |
. . . . . . . 8
β’ (π¦ = π β ((((π β π) = (π β π) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§))) β (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))))) |
79 | 78 | notbid 318 |
. . . . . . 7
β’ (π¦ = π β (Β¬ (((π β π) = (π β π) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (ππΌπ¦) β¨ π β (π§πΌπ¦) β¨ π¦ β (ππΌπ§))) β Β¬ (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))))) |
80 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π§ = π β (π β π§) = (π β π)) |
81 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π§ = π β (π β π§) = (π β π)) |
82 | 80, 81 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π§ = π β ((π β π§) = (π β π§) β (π β π) = (π β π))) |
83 | 82 | 3anbi3d 1443 |
. . . . . . . . 9
β’ (π§ = π β (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π§) = (π β π§)) β ((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)))) |
84 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π§ = π β (π§ β (ππΌπ) β π β (ππΌπ))) |
85 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π§ = π β (π§πΌπ) = (ππΌπ)) |
86 | 85 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π§ = π β (π β (π§πΌπ) β π β (ππΌπ))) |
87 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π§ = π β (ππΌπ§) = (ππΌπ)) |
88 | 87 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π§ = π β (π β (ππΌπ§) β π β (ππΌπ))) |
89 | 84, 86, 88 | 3orbi123d 1436 |
. . . . . . . . . 10
β’ (π§ = π β ((π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§)) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
90 | 89 | notbid 318 |
. . . . . . . . 9
β’ (π§ = π β (Β¬ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§)) β Β¬ (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
91 | 83, 90 | anbi12d 632 |
. . . . . . . 8
β’ (π§ = π β ((((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))) β (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ Β¬ (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
92 | 91 | notbid 318 |
. . . . . . 7
β’ (π§ = π β (Β¬ (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (ππΌπ) β¨ π β (π§πΌπ) β¨ π β (ππΌπ§))) β Β¬ (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ Β¬ (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
93 | 66, 79, 92 | rspc3v 3592 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (βπ₯ β π βπ¦ β π βπ§ β π Β¬ (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β Β¬ (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ Β¬ (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
94 | 51, 52, 53, 93 | syl3anc 1372 |
. . . . 5
β’ (π β (βπ₯ β π βπ¦ β π βπ§ β π Β¬ (((π β π₯) = (π β π₯) β§ (π β π¦) = (π β π¦) β§ (π β π§) = (π β π§)) β§ Β¬ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))) β Β¬ (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ Β¬ (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))))) |
95 | 50, 94 | mpd 15 |
. . . 4
β’ (π β Β¬ (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ Β¬ (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
96 | | imnan 401 |
. . . 4
β’ ((((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β Β¬ Β¬ (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) β Β¬ (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β§ Β¬ (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
97 | 95, 96 | sylibr 233 |
. . 3
β’ (π β (((π β π) = (π β π) β§ (π β π) = (π β π) β§ (π β π) = (π β π)) β Β¬ Β¬ (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
98 | 1, 2, 3, 97 | mp3and 1465 |
. 2
β’ (π β Β¬ Β¬ (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) |
99 | 98 | notnotrd 133 |
1
β’ (π β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) |