Step | Hyp | Ref
| Expression |
1 | | satfv0fun 34362 |
. . . 4
β’ ((π β π β§ πΈ β π) β Fun ((π Sat πΈ)ββ
)) |
2 | | satfv0fv.s |
. . . . . 6
β’ π = (π Sat πΈ) |
3 | 2 | fveq1i 6893 |
. . . . 5
β’ (πββ
) = ((π Sat πΈ)ββ
) |
4 | 3 | funeqi 6570 |
. . . 4
β’ (Fun
(πββ
) β
Fun ((π Sat πΈ)ββ
)) |
5 | 1, 4 | sylibr 233 |
. . 3
β’ ((π β π β§ πΈ β π) β Fun (πββ
)) |
6 | 5 | 3adant3 1133 |
. 2
β’ ((π β π β§ πΈ β π β§ π β (Fmlaββ
)) β Fun
(πββ
)) |
7 | | fmla0 34373 |
. . . . . . . 8
β’
(Fmlaββ
) = {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} |
8 | 7 | eleq2i 2826 |
. . . . . . 7
β’ (π β (Fmlaββ
)
β π β {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)}) |
9 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ = (πβππ) β π = (πβππ))) |
10 | 9 | 2rexbidv 3220 |
. . . . . . . 8
β’ (π₯ = π β (βπ β Ο βπ β Ο π₯ = (πβππ) β βπ β Ο βπ β Ο π = (πβππ))) |
11 | 10 | elrab 3684 |
. . . . . . 7
β’ (π β {π₯ β V β£ βπ β Ο βπ β Ο π₯ = (πβππ)} β (π β V β§ βπ β Ο βπ β Ο π = (πβππ))) |
12 | 8, 11 | bitri 275 |
. . . . . 6
β’ (π β (Fmlaββ
)
β (π β V β§
βπ β Ο
βπ β Ο
π = (πβππ))) |
13 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β Ο β§ π β Ο) β§ π = (πβππ)) β π = (πβππ)) |
14 | | goel 34338 |
. . . . . . . . . . . . . 14
β’ ((π β Ο β§ π β Ο) β (πβππ) = β¨β
, β¨π, πβ©β©) |
15 | 14 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ ((π β Ο β§ π β Ο) β (π = (πβππ) β π = β¨β
, β¨π, πβ©β©)) |
16 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . 16
β’ (π = β¨β
, β¨π, πβ©β© β (1st
β(2nd βπ)) = (1st β(2nd
ββ¨β
, β¨π, πβ©β©))) |
17 | | 0ex 5308 |
. . . . . . . . . . . . . . . . . . 19
β’ β
β V |
18 | | opex 5465 |
. . . . . . . . . . . . . . . . . . 19
β’
β¨π, πβ© β V |
19 | 17, 18 | op2nd 7984 |
. . . . . . . . . . . . . . . . . 18
β’
(2nd ββ¨β
, β¨π, πβ©β©) = β¨π, πβ© |
20 | 19 | fveq2i 6895 |
. . . . . . . . . . . . . . . . 17
β’
(1st β(2nd ββ¨β
, β¨π, πβ©β©)) = (1st
ββ¨π, πβ©) |
21 | | vex 3479 |
. . . . . . . . . . . . . . . . . 18
β’ π β V |
22 | | vex 3479 |
. . . . . . . . . . . . . . . . . 18
β’ π β V |
23 | 21, 22 | op1st 7983 |
. . . . . . . . . . . . . . . . 17
β’
(1st ββ¨π, πβ©) = π |
24 | 20, 23 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
β’
(1st β(2nd ββ¨β
, β¨π, πβ©β©)) = π |
25 | 16, 24 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
β’ (π = β¨β
, β¨π, πβ©β© β (1st
β(2nd βπ)) = π) |
26 | 25 | fveq2d 6896 |
. . . . . . . . . . . . . 14
β’ (π = β¨β
, β¨π, πβ©β© β (πβ(1st β(2nd
βπ))) = (πβπ)) |
27 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . 16
β’ (π = β¨β
, β¨π, πβ©β© β (2nd
β(2nd βπ)) = (2nd β(2nd
ββ¨β
, β¨π, πβ©β©))) |
28 | 19 | fveq2i 6895 |
. . . . . . . . . . . . . . . . 17
β’
(2nd β(2nd ββ¨β
, β¨π, πβ©β©)) = (2nd
ββ¨π, πβ©) |
29 | 21, 22 | op2nd 7984 |
. . . . . . . . . . . . . . . . 17
β’
(2nd ββ¨π, πβ©) = π |
30 | 28, 29 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
β’
(2nd β(2nd ββ¨β
, β¨π, πβ©β©)) = π |
31 | 27, 30 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
β’ (π = β¨β
, β¨π, πβ©β© β (2nd
β(2nd βπ)) = π) |
32 | 31 | fveq2d 6896 |
. . . . . . . . . . . . . 14
β’ (π = β¨β
, β¨π, πβ©β© β (πβ(2nd β(2nd
βπ))) = (πβπ)) |
33 | 26, 32 | breq12d 5162 |
. . . . . . . . . . . . 13
β’ (π = β¨β
, β¨π, πβ©β© β ((πβ(1st β(2nd
βπ)))πΈ(πβ(2nd β(2nd
βπ))) β (πβπ)πΈ(πβπ))) |
34 | 15, 33 | syl6bi 253 |
. . . . . . . . . . . 12
β’ ((π β Ο β§ π β Ο) β (π = (πβππ) β ((πβ(1st β(2nd
βπ)))πΈ(πβ(2nd β(2nd
βπ))) β (πβπ)πΈ(πβπ)))) |
35 | 34 | imp 408 |
. . . . . . . . . . 11
β’ (((π β Ο β§ π β Ο) β§ π = (πβππ)) β ((πβ(1st β(2nd
βπ)))πΈ(πβ(2nd β(2nd
βπ))) β (πβπ)πΈ(πβπ))) |
36 | 35 | rabbidv 3441 |
. . . . . . . . . 10
β’ (((π β Ο β§ π β Ο) β§ π = (πβππ)) β {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)}) |
37 | 13, 36 | jca 513 |
. . . . . . . . 9
β’ (((π β Ο β§ π β Ο) β§ π = (πβππ)) β (π = (πβππ) β§ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})) |
38 | 37 | ex 414 |
. . . . . . . 8
β’ ((π β Ο β§ π β Ο) β (π = (πβππ) β (π = (πβππ) β§ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)}))) |
39 | 38 | reximdva 3169 |
. . . . . . 7
β’ (π β Ο β
(βπ β Ο
π = (πβππ) β βπ β Ο (π = (πβππ) β§ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)}))) |
40 | 39 | reximia 3082 |
. . . . . 6
β’
(βπ β
Ο βπ β
Ο π = (πβππ) β βπ β Ο βπ β Ο (π = (πβππ) β§ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})) |
41 | 12, 40 | simplbiim 506 |
. . . . 5
β’ (π β (Fmlaββ
)
β βπ β
Ο βπ β
Ο (π = (πβππ) β§ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})) |
42 | 41 | 3ad2ant3 1136 |
. . . 4
β’ ((π β π β§ πΈ β π β§ π β (Fmlaββ
)) β
βπ β Ο
βπ β Ο
(π = (πβππ) β§ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})) |
43 | | simp3 1139 |
. . . . 5
β’ ((π β π β§ πΈ β π β§ π β (Fmlaββ
)) β π β
(Fmlaββ
)) |
44 | | ovex 7442 |
. . . . . 6
β’ (π βm Ο)
β V |
45 | 44 | rabex 5333 |
. . . . 5
β’ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} β
V |
46 | | eqeq1 2737 |
. . . . . . . 8
β’ (π¦ = {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} β (π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)} β {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})) |
47 | 9, 46 | bi2anan9 638 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}) β
((π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)}) β (π = (πβππ) β§ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)}))) |
48 | 47 | 2rexbidv 3220 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}) β
(βπ β Ο
βπ β Ο
(π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)}) β βπ β Ο βπ β Ο (π = (πβππ) β§ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)}))) |
49 | 48 | opelopabga 5534 |
. . . . 5
β’ ((π β (Fmlaββ
)
β§ {π β (π βm Ο)
β£ (πβ(1st β(2nd
βπ)))πΈ(πβ(2nd β(2nd
βπ)))} β V)
β (β¨π, {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}β© β
{β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})} β βπ β Ο βπ β Ο (π = (πβππ) β§ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)}))) |
50 | 43, 45, 49 | sylancl 587 |
. . . 4
β’ ((π β π β§ πΈ β π β§ π β (Fmlaββ
)) β
(β¨π, {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}β© β
{β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})} β βπ β Ο βπ β Ο (π = (πβππ) β§ {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))} = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)}))) |
51 | 42, 50 | mpbird 257 |
. . 3
β’ ((π β π β§ πΈ β π β§ π β (Fmlaββ
)) β
β¨π, {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}β© β
{β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})}) |
52 | 2 | satfv0 34349 |
. . . . 5
β’ ((π β π β§ πΈ β π) β (πββ
) = {β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})}) |
53 | 52 | eleq2d 2820 |
. . . 4
β’ ((π β π β§ πΈ β π) β (β¨π, {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}β© β
(πββ
) β
β¨π, {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}β© β
{β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})})) |
54 | 53 | 3adant3 1133 |
. . 3
β’ ((π β π β§ πΈ β π β§ π β (Fmlaββ
)) β
(β¨π, {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}β© β
(πββ
) β
β¨π, {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}β© β
{β¨π₯, π¦β© β£ βπ β Ο βπ β Ο (π₯ = (πβππ) β§ π¦ = {π β (π βm Ο) β£ (πβπ)πΈ(πβπ)})})) |
55 | 51, 54 | mpbird 257 |
. 2
β’ ((π β π β§ πΈ β π β§ π β (Fmlaββ
)) β
β¨π, {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}β© β
(πββ
)) |
56 | | funopfv 6944 |
. 2
β’ (Fun
(πββ
) β
(β¨π, {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}β© β
(πββ
) β
((πββ
)βπ) = {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))})) |
57 | 6, 55, 56 | sylc 65 |
1
β’ ((π β π β§ πΈ β π β§ π β (Fmlaββ
)) β ((πββ
)βπ) = {π β (π βm Ο) β£ (πβ(1st
β(2nd βπ)))πΈ(πβ(2nd β(2nd
βπ)))}) |