Step | Hyp | Ref
| Expression |
1 | | segcon2 35015 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β βπ₯ β (πΌβπ)((π
Btwn β¨π΄, π₯β© β¨ π₯ Btwn β¨π΄, π
β©) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©)) |
2 | 1 | adantr 482 |
. . . 4
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π
β π΄ β§ π΅ β πΆ)) β βπ₯ β (πΌβπ)((π
Btwn β¨π΄, π₯β© β¨ π₯ Btwn β¨π΄, π
β©) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©)) |
3 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β π β β) |
4 | | simpl2l 1227 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β π΄ β (πΌβπ)) |
5 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β π₯ β (πΌβπ)) |
6 | | simpl2r 1228 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β π
β (πΌβπ)) |
7 | | broutsideof2 35032 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π₯ β (πΌβπ) β§ π
β (πΌβπ))) β (π΄OutsideOfβ¨π₯, π
β© β (π₯ β π΄ β§ π
β π΄ β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©)))) |
8 | 3, 4, 5, 6, 7 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β (π΄OutsideOfβ¨π₯, π
β© β (π₯ β π΄ β§ π
β π΄ β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©)))) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ ((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©)) β (π΄OutsideOfβ¨π₯, π
β© β (π₯ β π΄ β§ π
β π΄ β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©)))) |
10 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((π₯ β π΄ β§ π
β π΄ β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©)) β (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©)) |
11 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©)) β π΅ β πΆ) |
12 | 11 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) β π΅ β πΆ) |
13 | | simprlr 779 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) β β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) |
14 | | simp2l 1200 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β π΄ β (πΌβπ)) |
15 | 14 | anim1i 616 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β (π΄ β (πΌβπ) β§ π₯ β (πΌβπ))) |
16 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) |
17 | | cgrdegen 34914 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π₯ β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (β¨π΄, π₯β©Cgrβ¨π΅, πΆβ© β (π΄ = π₯ β π΅ = πΆ))) |
18 | 3, 15, 16, 17 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β (β¨π΄, π₯β©Cgrβ¨π΅, πΆβ© β (π΄ = π₯ β π΅ = πΆ))) |
19 | 18 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) β (β¨π΄, π₯β©Cgrβ¨π΅, πΆβ© β (π΄ = π₯ β π΅ = πΆ))) |
20 | 13, 19 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) β (π΄ = π₯ β π΅ = πΆ)) |
21 | 20 | necon3bid 2986 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) β (π΄ β π₯ β π΅ β πΆ)) |
22 | 12, 21 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) β π΄ β π₯) |
23 | 22 | necomd 2997 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) β π₯ β π΄) |
24 | | simplll 774 |
. . . . . . . . . . . . . 14
β’ ((((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©)) β π
β π΄) |
25 | 24 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) β π
β π΄) |
26 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) β (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©)) |
27 | 23, 25, 26 | 3jca 1129 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) β (π₯ β π΄ β§ π
β π΄ β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) |
28 | 27 | expr 458 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ ((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©)) β ((π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©) β (π₯ β π΄ β§ π
β π΄ β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©)))) |
29 | 10, 28 | impbid2 225 |
. . . . . . . . . 10
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ ((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©)) β ((π₯ β π΄ β§ π
β π΄ β§ (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©)) β (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) |
30 | 9, 29 | bitrd 279 |
. . . . . . . . 9
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ ((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©)) β (π΄OutsideOfβ¨π₯, π
β© β (π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©))) |
31 | | orcom 869 |
. . . . . . . . 9
β’ ((π₯ Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, π₯β©) β (π
Btwn β¨π΄, π₯β© β¨ π₯ Btwn β¨π΄, π
β©)) |
32 | 30, 31 | bitrdi 287 |
. . . . . . . 8
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ ((π
β π΄ β§ π΅ β πΆ) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©)) β (π΄OutsideOfβ¨π₯, π
β© β (π
Btwn β¨π΄, π₯β© β¨ π₯ Btwn β¨π΄, π
β©))) |
33 | 32 | expr 458 |
. . . . . . 7
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (π
β π΄ β§ π΅ β πΆ)) β (β¨π΄, π₯β©Cgrβ¨π΅, πΆβ© β (π΄OutsideOfβ¨π₯, π
β© β (π
Btwn β¨π΄, π₯β© β¨ π₯ Btwn β¨π΄, π
β©)))) |
34 | 33 | pm5.32rd 579 |
. . . . . 6
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ π₯ β (πΌβπ)) β§ (π
β π΄ β§ π΅ β πΆ)) β ((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β ((π
Btwn β¨π΄, π₯β© β¨ π₯ Btwn β¨π΄, π
β©) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©))) |
35 | 34 | an32s 651 |
. . . . 5
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π
β π΄ β§ π΅ β πΆ)) β§ π₯ β (πΌβπ)) β ((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β ((π
Btwn β¨π΄, π₯β© β¨ π₯ Btwn β¨π΄, π
β©) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©))) |
36 | 35 | rexbidva 3177 |
. . . 4
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π
β π΄ β§ π΅ β πΆ)) β (βπ₯ β (πΌβπ)(π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β βπ₯ β (πΌβπ)((π
Btwn β¨π΄, π₯β© β¨ π₯ Btwn β¨π΄, π
β©) β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©))) |
37 | 2, 36 | mpbird 257 |
. . 3
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π
β π΄ β§ π΅ β πΆ)) β βπ₯ β (πΌβπ)(π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©)) |
38 | | simpl1 1192 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β π β β) |
39 | | simpl2l 1227 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β π΄ β (πΌβπ)) |
40 | | simpl2r 1228 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β π
β (πΌβπ)) |
41 | | simpl3l 1229 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β π΅ β (πΌβπ)) |
42 | 39, 40, 41 | 3jca 1129 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ))) |
43 | | simpl3r 1230 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β πΆ β (πΌβπ)) |
44 | | simprl 770 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β π₯ β (πΌβπ)) |
45 | | simprr 772 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β π¦ β (πΌβπ)) |
46 | 43, 44, 45 | 3jca 1129 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β (πΆ β (πΌβπ) β§ π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) |
47 | 38, 42, 46 | 3jca 1129 |
. . . . . . 7
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β (π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π₯ β (πΌβπ) β§ π¦ β (πΌβπ)))) |
48 | | simpr 486 |
. . . . . . 7
β’ (((π
β π΄ β§ π΅ β πΆ) β§ ((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π¦, π
β© β§ β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©))) β ((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π¦, π
β© β§ β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©))) |
49 | | outsideofeq 35040 |
. . . . . . . 8
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β (((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π¦, π
β© β§ β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©)) β π₯ = π¦)) |
50 | 49 | imp 408 |
. . . . . . 7
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β§ ((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π¦, π
β© β§ β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©))) β π₯ = π¦) |
51 | 47, 48, 50 | syl2an 597 |
. . . . . 6
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β§ ((π
β π΄ β§ π΅ β πΆ) β§ ((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π¦, π
β© β§ β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©)))) β π₯ = π¦) |
52 | 51 | an4s 659 |
. . . . 5
β’ ((((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π
β π΄ β§ π΅ β πΆ)) β§ ((π₯ β (πΌβπ) β§ π¦ β (πΌβπ)) β§ ((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π¦, π
β© β§ β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©)))) β π₯ = π¦) |
53 | 52 | exp32 422 |
. . . 4
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π
β π΄ β§ π΅ β πΆ)) β ((π₯ β (πΌβπ) β§ π¦ β (πΌβπ)) β (((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π¦, π
β© β§ β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©)) β π₯ = π¦))) |
54 | 53 | ralrimivv 3199 |
. . 3
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π
β π΄ β§ π΅ β πΆ)) β βπ₯ β (πΌβπ)βπ¦ β (πΌβπ)(((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π¦, π
β© β§ β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©)) β π₯ = π¦)) |
55 | | opeq1 4872 |
. . . . . 6
β’ (π₯ = π¦ β β¨π₯, π
β© = β¨π¦, π
β©) |
56 | 55 | breq2d 5159 |
. . . . 5
β’ (π₯ = π¦ β (π΄OutsideOfβ¨π₯, π
β© β π΄OutsideOfβ¨π¦, π
β©)) |
57 | | opeq2 4873 |
. . . . . 6
β’ (π₯ = π¦ β β¨π΄, π₯β© = β¨π΄, π¦β©) |
58 | 57 | breq1d 5157 |
. . . . 5
β’ (π₯ = π¦ β (β¨π΄, π₯β©Cgrβ¨π΅, πΆβ© β β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©)) |
59 | 56, 58 | anbi12d 632 |
. . . 4
β’ (π₯ = π¦ β ((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β (π΄OutsideOfβ¨π¦, π
β© β§ β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©))) |
60 | 59 | reu4 3726 |
. . 3
β’
(β!π₯ β
(πΌβπ)(π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β (βπ₯ β (πΌβπ)(π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ βπ₯ β (πΌβπ)βπ¦ β (πΌβπ)(((π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π¦, π
β© β§ β¨π΄, π¦β©Cgrβ¨π΅, πΆβ©)) β π₯ = π¦))) |
61 | 37, 54, 60 | sylanbrc 584 |
. 2
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β§ (π
β π΄ β§ π΅ β πΆ)) β β!π₯ β (πΌβπ)(π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©)) |
62 | 61 | ex 414 |
1
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β ((π
β π΄ β§ π΅ β πΆ) β β!π₯ β (πΌβπ)(π΄OutsideOfβ¨π₯, π
β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©))) |