Step | Hyp | Ref
| Expression |
1 | | satff 34699 |
. . . . . 6
β’ ((π β π β§ πΈ β π β§ π₯ β Ο) β ((π Sat πΈ)βπ₯):(Fmlaβπ₯)βΆπ« (π βm
Ο)) |
2 | 1 | 3expa 1116 |
. . . . 5
β’ (((π β π β§ πΈ β π) β§ π₯ β Ο) β ((π Sat πΈ)βπ₯):(Fmlaβπ₯)βΆπ« (π βm
Ο)) |
3 | | entric 10554 |
. . . . . . . . 9
β’ ((π₯ β Ο β§ π¦ β Ο) β (π₯ βΊ π¦ β¨ π₯ β π¦ β¨ π¦ βΊ π₯)) |
4 | 3 | adantl 480 |
. . . . . . . 8
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ βΊ π¦ β¨ π₯ β π¦ β¨ π¦ βΊ π₯)) |
5 | | nnsdomo 9236 |
. . . . . . . . . . 11
β’ ((π₯ β Ο β§ π¦ β Ο) β (π₯ βΊ π¦ β π₯ β π¦)) |
6 | 5 | adantl 480 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ βΊ π¦ β π₯ β π¦)) |
7 | | pm3.22 458 |
. . . . . . . . . . . . . 14
β’ ((π₯ β Ο β§ π¦ β Ο) β (π¦ β Ο β§ π₯ β
Ο)) |
8 | 7 | anim2i 615 |
. . . . . . . . . . . . 13
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β ((π β π β§ πΈ β π) β§ (π¦ β Ο β§ π₯ β Ο))) |
9 | | pssss 4094 |
. . . . . . . . . . . . 13
β’ (π₯ β π¦ β π₯ β π¦) |
10 | | eqid 2730 |
. . . . . . . . . . . . . . 15
β’ (π Sat πΈ) = (π Sat πΈ) |
11 | 10 | satfsschain 34653 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ πΈ β π) β§ (π¦ β Ο β§ π₯ β Ο)) β (π₯ β π¦ β ((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦))) |
12 | 11 | imp 405 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ πΈ β π) β§ (π¦ β Ο β§ π₯ β Ο)) β§ π₯ β π¦) β ((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦)) |
13 | 8, 9, 12 | syl2an 594 |
. . . . . . . . . . . 12
β’ ((((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β§ π₯ β π¦) β ((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦)) |
14 | 13 | orcd 869 |
. . . . . . . . . . 11
β’ ((((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β§ π₯ β π¦) β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
15 | 14 | ex 411 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ β π¦ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
16 | 6, 15 | sylbid 239 |
. . . . . . . . 9
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ βΊ π¦ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
17 | | nneneq 9211 |
. . . . . . . . . . 11
β’ ((π₯ β Ο β§ π¦ β Ο) β (π₯ β π¦ β π₯ = π¦)) |
18 | 17 | adantl 480 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ β π¦ β π₯ = π¦)) |
19 | | ssid 4003 |
. . . . . . . . . . . 12
β’ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ¦) |
20 | | fveq2 6890 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β ((π Sat πΈ)βπ₯) = ((π Sat πΈ)βπ¦)) |
21 | 19, 20 | sseqtrrid 4034 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)) |
22 | 21 | olcd 870 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
23 | 18, 22 | syl6bi 252 |
. . . . . . . . 9
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π₯ β π¦ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
24 | | nnsdomo 9236 |
. . . . . . . . . . . 12
β’ ((π¦ β Ο β§ π₯ β Ο) β (π¦ βΊ π₯ β π¦ β π₯)) |
25 | 24 | ancoms 457 |
. . . . . . . . . . 11
β’ ((π₯ β Ο β§ π¦ β Ο) β (π¦ βΊ π₯ β π¦ β π₯)) |
26 | 25 | adantl 480 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π¦ βΊ π₯ β π¦ β π₯)) |
27 | 10 | satfsschain 34653 |
. . . . . . . . . . . . 13
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π¦ β π₯ β ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
28 | | pssss 4094 |
. . . . . . . . . . . . 13
β’ (π¦ β π₯ β π¦ β π₯) |
29 | 27, 28 | impel 504 |
. . . . . . . . . . . 12
β’ ((((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β§ π¦ β π₯) β ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)) |
30 | 29 | olcd 870 |
. . . . . . . . . . 11
β’ ((((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β§ π¦ β π₯) β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
31 | 30 | ex 411 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π¦ β π₯ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
32 | 26, 31 | sylbid 239 |
. . . . . . . . 9
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (π¦ βΊ π₯ β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
33 | 16, 23, 32 | 3jaod 1426 |
. . . . . . . 8
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β ((π₯ βΊ π¦ β¨ π₯ β π¦ β¨ π¦ βΊ π₯) β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
34 | 4, 33 | mpd 15 |
. . . . . . 7
β’ (((π β π β§ πΈ β π) β§ (π₯ β Ο β§ π¦ β Ο)) β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
35 | 34 | expr 455 |
. . . . . 6
β’ (((π β π β§ πΈ β π) β§ π₯ β Ο) β (π¦ β Ο β (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
36 | 35 | ralrimiv 3143 |
. . . . 5
β’ (((π β π β§ πΈ β π) β§ π₯ β Ο) β βπ¦ β Ο (((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) |
37 | 2, 36 | jca 510 |
. . . 4
β’ (((π β π β§ πΈ β π) β§ π₯ β Ο) β (((π Sat πΈ)βπ₯):(Fmlaβπ₯)βΆπ« (π βm Ο) β§
βπ¦ β Ο
(((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
38 | 37 | ralrimiva 3144 |
. . 3
β’ ((π β π β§ πΈ β π) β βπ₯ β Ο (((π Sat πΈ)βπ₯):(Fmlaβπ₯)βΆπ« (π βm Ο) β§
βπ¦ β Ο
(((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯)))) |
39 | | fvex 6903 |
. . . 4
β’ ((π Sat πΈ)βπ₯) β V |
40 | 20, 39 | fiun 7931 |
. . 3
β’
(βπ₯ β
Ο (((π Sat πΈ)βπ₯):(Fmlaβπ₯)βΆπ« (π βm Ο) β§
βπ¦ β Ο
(((π Sat πΈ)βπ₯) β ((π Sat πΈ)βπ¦) β¨ ((π Sat πΈ)βπ¦) β ((π Sat πΈ)βπ₯))) β βͺ π₯ β Ο ((π Sat πΈ)βπ₯):βͺ π₯ β Ο
(Fmlaβπ₯)βΆπ« (π βm
Ο)) |
41 | 38, 40 | syl 17 |
. 2
β’ ((π β π β§ πΈ β π) β βͺ
π₯ β Ο ((π Sat πΈ)βπ₯):βͺ π₯ β Ο
(Fmlaβπ₯)βΆπ« (π βm
Ο)) |
42 | | satom 34645 |
. . 3
β’ ((π β π β§ πΈ β π) β ((π Sat πΈ)βΟ) = βͺ π₯ β Ο ((π Sat πΈ)βπ₯)) |
43 | | fmla 34670 |
. . . 4
β’
(FmlaβΟ) = βͺ π₯ β Ο
(Fmlaβπ₯) |
44 | 43 | a1i 11 |
. . 3
β’ ((π β π β§ πΈ β π) β (FmlaβΟ) = βͺ π₯ β Ο (Fmlaβπ₯)) |
45 | 42, 44 | feq12d 6704 |
. 2
β’ ((π β π β§ πΈ β π) β (((π Sat πΈ)βΟ):(FmlaβΟ)βΆπ«
(π βm Ο) β
βͺ π₯
β Ο ((π Sat πΈ)βπ₯):βͺ π₯ β Ο (Fmlaβπ₯)βΆπ« (π βm Ο))) |
46 | 41, 45 | mpbird 256 |
1
β’ ((π β π β§ πΈ β π) β ((π Sat πΈ)βΟ):(FmlaβΟ)βΆπ«
(π βm
Ο)) |