Step | Hyp | Ref
| Expression |
1 | | satff 34401 |
. . . . . 6
β’ ((π β π β§ πΈ β π β§ π₯ β Ο) β ((π Sat πΈ)βπ₯):(Fmlaβπ₯)βΆπ« (π βm
Ο)) |
2 | 1 | 3expa 1119 |
. . . . 5
β’ (((π β π β§ πΈ β π) β§ π₯ β Ο) β ((π Sat πΈ)βπ₯):(Fmlaβπ₯)βΆπ« (π βm
Ο)) |
3 | | entric 10552 |
. . . . . . . . 9
β’ ((π₯ β Ο β§ π¦ β Ο) β (π₯ βΊ π¦ β¨ π₯ β π¦ β¨ π¦ βΊ π₯)) |
4 | 3 | adantl 483 |
. . . . . . . 8
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ βΊ π¦ β¨ π₯ β π¦ β¨ π¦ βΊ π₯)) |
5 | | nnsdomo 9234 |
. . . . . . . . . . 11
β’ ((π₯ β Ο β§ π¦ β Ο) β (π₯ βΊ π¦ β π₯ β π¦)) |
6 | 5 | adantl 483 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ βΊ π¦ β π₯ β π¦)) |
7 | | pm3.22 461 |
. . . . . . . . . . . . . 14
β’ ((π₯ β Ο β§ π¦ β Ο) β (π¦ β Ο β§ π₯ β
Ο)) |
8 | 7 | anim2i 618 |
. . . . . . . . . . . . 13
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β ((π β π β§ πΈ β π) β§ (π¦ β Ο β§ π₯ β Ο))) |
9 | | pssss 4096 |
. . . . . . . . . . . . 13
β’ (π₯ β π¦ β π₯ β π¦) |
10 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π Sat πΈ) = (π Sat πΈ) |
11 | 10 | satfsschain 34355 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ πΈ β π) β§ (π¦ β Ο β§ π₯ β Ο)) β (π₯ β π¦ β ((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦))) |
12 | 11 | imp 408 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ πΈ β π) β§ (π¦ β Ο β§ π₯ β Ο)) β§ π₯ β π¦) β ((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦)) |
13 | 8, 9, 12 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β§ π₯ β π¦) β ((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦)) |
14 | 13 | orcd 872 |
. . . . . . . . . . 11
β’ ((((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β§ π₯ β π¦) β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
15 | 14 | ex 414 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ β π¦ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
16 | 6, 15 | sylbid 239 |
. . . . . . . . 9
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ βΊ π¦ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
17 | | nneneq 9209 |
. . . . . . . . . . 11
β’ ((π₯ β Ο β§ π¦ β Ο) β (π₯ β π¦ β π₯ = π¦)) |
18 | 17 | adantl 483 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ β π¦ β π₯ = π¦)) |
19 | | ssid 4005 |
. . . . . . . . . . . 12
β’ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ¦) |
20 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β ((π Sat πΈ)βπ₯) = ((π Sat πΈ)βπ¦)) |
21 | 19, 20 | sseqtrrid 4036 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)) |
22 | 21 | olcd 873 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
23 | 18, 22 | syl6bi 253 |
. . . . . . . . 9
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ β π¦ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
24 | | nnsdomo 9234 |
. . . . . . . . . . . 12
β’ ((π¦ β Ο β§ π₯ β Ο) β (π¦ βΊ π₯ β π¦ β π₯)) |
25 | 24 | ancoms 460 |
. . . . . . . . . . 11
β’ ((π₯ β Ο β§ π¦ β Ο) β (π¦ βΊ π₯ β π¦ β π₯)) |
26 | 25 | adantl 483 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π¦ βΊ π₯ β π¦ β π₯)) |
27 | 10 | satfsschain 34355 |
. . . . . . . . . . . . 13
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π¦ β π₯ β ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
28 | | pssss 4096 |
. . . . . . . . . . . . 13
β’ (π¦ β π₯ β π¦ β π₯) |
29 | 27, 28 | impel 507 |
. . . . . . . . . . . 12
β’ ((((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β§ π¦ β π₯) β ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)) |
30 | 29 | olcd 873 |
. . . . . . . . . . 11
β’ ((((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β§ π¦ β π₯) β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
31 | 30 | ex 414 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π¦ β π₯ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
32 | 26, 31 | sylbid 239 |
. . . . . . . . 9
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π¦ βΊ π₯ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
33 | 16, 23, 32 | 3jaod 1429 |
. . . . . . . 8
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β ((π₯ βΊ π¦ β¨ π₯ β π¦ β¨ π¦ βΊ π₯) β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
34 | 4, 33 | mpd 15 |
. . . . . . 7
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
35 | 34 | expr 458 |
. . . . . 6
β’ (((π β π β§ πΈ β π) β§ π₯ β Ο) β (π¦ β Ο β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
36 | 35 | ralrimiv 3146 |
. . . . 5
β’ (((π β π β§ πΈ β π) β§ π₯ β Ο) β βπ¦ β Ο (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
37 | 2, 36 | jca 513 |
. . . 4
β’ (((π β π β§ πΈ β π) β§ π₯ β Ο) β (((π Sat πΈ)βπ₯):(Fmlaβπ₯)βΆπ« (π βm Ο) β§
βπ¦ β Ο
(((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
38 | 37 | ralrimiva 3147 |
. . 3
β’ ((π β π β§ πΈ β π) β βπ₯ β Ο (((π Sat πΈ)βπ₯):(Fmlaβπ₯)βΆπ« (π βm Ο) β§
βπ¦ β Ο
(((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
39 | | fvex 6905 |
. . . 4
β’ ((π Sat πΈ)βπ₯) β V |
40 | 20, 39 | fiun 7929 |
. . 3
β’
(βπ₯ β
Ο (((π Sat πΈ)βπ₯):(Fmlaβπ₯)βΆπ« (π βm Ο) β§
βπ¦ β Ο
(((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) β βͺ π₯ β Ο ((π Sat πΈ)βπ₯):βͺ π₯ β Ο
(Fmlaβπ₯)βΆπ« (π βm
Ο)) |
41 | 38, 40 | syl 17 |
. 2
β’ ((π β π β§ πΈ β π) β βͺ
π₯ β Ο ((π Sat πΈ)βπ₯):βͺ π₯ β Ο
(Fmlaβπ₯)βΆπ« (π βm
Ο)) |
42 | | satom 34347 |
. . 3
β’ ((π β π β§ πΈ β π) β ((π Sat πΈ)βΟ) = βͺ π₯ β Ο ((π Sat πΈ)βπ₯)) |
43 | | fmla 34372 |
. . . 4
β’
(FmlaβΟ) = βͺ π₯ β Ο
(Fmlaβπ₯) |
44 | 43 | a1i 11 |
. . 3
β’ ((π β π β§ πΈ β π) β (FmlaβΟ) = βͺ π₯ β Ο (Fmlaβπ₯)) |
45 | 42, 44 | feq12d 6706 |
. 2
β’ ((π β π β§ πΈ β π) β (((π Sat πΈ)βΟ):(FmlaβΟ)βΆπ«
(π βm Ο) β
βͺ π₯
β Ο ((π Sat πΈ)βπ₯):βͺ π₯ β Ο (Fmlaβπ₯)βΆπ« (π βm Ο))) |
46 | 41, 45 | mpbird 257 |
1
β’ ((π β π β§ πΈ β π) β ((π Sat πΈ)βΟ):(FmlaβΟ)βΆπ«
(π βm
Ο)) |