Step | Hyp | Ref
| Expression |
1 | | peano1 7829 |
. . . 4
β’ β
β Ο |
2 | | satfdmfmla 34058 |
. . . 4
β’ ((π β π β§ πΈ β π β§ β
β Ο) β dom
((π Sat πΈ)ββ
) =
(Fmlaββ
)) |
3 | 1, 2 | mp3an3 1451 |
. . 3
β’ ((π β π β§ πΈ β π) β dom ((π Sat πΈ)ββ
) =
(Fmlaββ
)) |
4 | | ovex 7394 |
. . . . . . . . . 10
β’ (π βm Ο)
β V |
5 | 4 | difexi 5289 |
. . . . . . . . 9
β’ ((π βm Ο)
β ((2nd βπ’) β© (2nd βπ£))) β V |
6 | 5 | a1i 11 |
. . . . . . . 8
β’ ((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ π£ β ((π Sat πΈ)ββ
)) β ((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£))) β V) |
7 | 6 | ralrimiva 3140 |
. . . . . . 7
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β βπ£ β ((π Sat πΈ)ββ
)((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£))) β V) |
8 | 4 | rabex 5293 |
. . . . . . . . 9
β’ {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)} β V |
9 | 8 | a1i 11 |
. . . . . . . 8
β’ ((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ π β Ο) β {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)} β V) |
10 | 9 | ralrimiva 3140 |
. . . . . . 7
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β βπ β Ο {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)} β V) |
11 | 7, 10 | jca 513 |
. . . . . 6
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β (βπ£ β ((π Sat πΈ)ββ
)((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£))) β V β§ βπ β Ο {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)} β V)) |
12 | 11 | ralrimiva 3140 |
. . . . 5
β’ ((π β π β§ πΈ β π) β βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£))) β V β§ βπ β Ο {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)} β V)) |
13 | | dmopab2rex 5877 |
. . . . 5
β’
(βπ’ β
((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£))) β V β§ βπ β Ο {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)} β V) β dom
{β¨π₯, π¦β© β£ βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = ((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))} = {π₯ β£ βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}) |
14 | 12, 13 | syl 17 |
. . . 4
β’ ((π β π β§ πΈ β π) β dom {β¨π₯, π¦β© β£ βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = ((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))} = {π₯ β£ βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))}) |
15 | | satfrel 34025 |
. . . . . . . . . . . . 13
β’ ((π β π β§ πΈ β π β§ β
β Ο) β Rel
((π Sat πΈ)ββ
)) |
16 | 1, 15 | mp3an3 1451 |
. . . . . . . . . . . 12
β’ ((π β π β§ πΈ β π) β Rel ((π Sat πΈ)ββ
)) |
17 | | 1stdm 7976 |
. . . . . . . . . . . 12
β’ ((Rel
((π Sat πΈ)ββ
) β§ π’ β ((π Sat πΈ)ββ
)) β (1st
βπ’) β dom
((π Sat πΈ)ββ
)) |
18 | 16, 17 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β (1st
βπ’) β dom
((π Sat πΈ)ββ
)) |
19 | 2 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ ((π β π β§ πΈ β π β§ β
β Ο) β
(Fmlaββ
) = dom ((π Sat πΈ)ββ
)) |
20 | 1, 19 | mp3an3 1451 |
. . . . . . . . . . . 12
β’ ((π β π β§ πΈ β π) β (Fmlaββ
) = dom ((π Sat πΈ)ββ
)) |
21 | 20 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β
(Fmlaββ
) = dom ((π Sat πΈ)ββ
)) |
22 | 18, 21 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β (1st
βπ’) β
(Fmlaββ
)) |
23 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ (βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))) β (1st βπ’) β
(Fmlaββ
)) |
24 | | oveq1 7368 |
. . . . . . . . . . . . 13
β’ (π = (1st βπ’) β (πβΌππ) = ((1st βπ’)βΌππ)) |
25 | 24 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π = (1st βπ’) β (π₯ = (πβΌππ) β π₯ = ((1st βπ’)βΌππ))) |
26 | 25 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π = (1st βπ’) β (βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β βπ β (Fmlaββ
)π₯ = ((1st βπ’)βΌππ))) |
27 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ (π = (1st βπ’) β π = π) |
28 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = (1st βπ’) β π = (1st βπ’)) |
29 | 27, 28 | goaleq12d 34009 |
. . . . . . . . . . . . 13
β’ (π = (1st βπ’) β
βπππ = βππ(1st βπ’)) |
30 | 29 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π = (1st βπ’) β (π₯ = βπππ β π₯ = βππ(1st βπ’))) |
31 | 30 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π = (1st βπ’) β (βπ β Ο π₯ =
βπππ β βπ β Ο π₯ = βππ(1st βπ’))) |
32 | 26, 31 | orbi12d 918 |
. . . . . . . . . 10
β’ (π = (1st βπ’) β ((βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ) β (βπ β (Fmlaββ
)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)))) |
33 | 32 | adantl 483 |
. . . . . . . . 9
β’
(((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ (βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))) β§ π = (1st βπ’)) β ((βπ β (Fmlaββ
)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β (βπ β (Fmlaββ
)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)))) |
34 | | 1stdm 7976 |
. . . . . . . . . . . . . . . . 17
β’ ((Rel
((π Sat πΈ)ββ
) β§ π£ β ((π Sat πΈ)ββ
)) β (1st
βπ£) β dom
((π Sat πΈ)ββ
)) |
35 | 16, 34 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ (((π β π β§ πΈ β π) β§ π£ β ((π Sat πΈ)ββ
)) β (1st
βπ£) β dom
((π Sat πΈ)ββ
)) |
36 | 20 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β π β§ πΈ β π) β§ π£ β ((π Sat πΈ)ββ
)) β
(Fmlaββ
) = dom ((π Sat πΈ)ββ
)) |
37 | 35, 36 | eleqtrrd 2837 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ πΈ β π) β§ π£ β ((π Sat πΈ)ββ
)) β (1st
βπ£) β
(Fmlaββ
)) |
38 | 37 | ad4ant13 750 |
. . . . . . . . . . . . . 14
β’
(((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ π£ β ((π Sat πΈ)ββ
)) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
(1st βπ£)
β (Fmlaββ
)) |
39 | | oveq2 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = (1st βπ£) β ((1st
βπ’)βΌππ) = ((1st
βπ’)βΌπ(1st
βπ£))) |
40 | 39 | eqeq2d 2744 |
. . . . . . . . . . . . . . 15
β’ (π = (1st βπ£) β (π₯ = ((1st βπ’)βΌππ) β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
41 | 40 | adantl 483 |
. . . . . . . . . . . . . 14
β’
((((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ π£ β ((π Sat πΈ)ββ
)) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β§ π = (1st βπ£)) β (π₯ = ((1st βπ’)βΌππ) β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
42 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ π£ β ((π Sat πΈ)ββ
)) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β π₯ = ((1st βπ’)βΌπ(1st
βπ£))) |
43 | 38, 41, 42 | rspcedvd 3585 |
. . . . . . . . . . . . 13
β’
(((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ π£ β ((π Sat πΈ)ββ
)) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
βπ β
(Fmlaββ
)π₯ =
((1st βπ’)βΌππ)) |
44 | 43 | ex 414 |
. . . . . . . . . . . 12
β’ ((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ π£ β ((π Sat πΈ)ββ
)) β (π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β
βπ β
(Fmlaββ
)π₯ =
((1st βπ’)βΌππ))) |
45 | 44 | rexlimdva 3149 |
. . . . . . . . . . 11
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β (βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β
βπ β
(Fmlaββ
)π₯ =
((1st βπ’)βΌππ))) |
46 | 45 | orim1d 965 |
. . . . . . . . . 10
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β ((βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β (βπ β (Fmlaββ
)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)))) |
47 | 46 | imp 408 |
. . . . . . . . 9
β’ ((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ (βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))) β (βπ β (Fmlaββ
)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’))) |
48 | 23, 33, 47 | rspcedvd 3585 |
. . . . . . . 8
β’ ((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ (βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))) β βπ β (Fmlaββ
)(βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ)) |
49 | 48 | ex 414 |
. . . . . . 7
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β ((βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β βπ β (Fmlaββ
)(βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ))) |
50 | 49 | rexlimdva 3149 |
. . . . . 6
β’ ((π β π β§ πΈ β π) β (βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β βπ β (Fmlaββ
)(βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ))) |
51 | | releldm2 7979 |
. . . . . . . . . 10
β’ (Rel
((π Sat πΈ)ββ
) β (π β dom ((π Sat πΈ)ββ
) β βπ’ β ((π Sat πΈ)ββ
)(1st βπ’) = π)) |
52 | 16, 51 | syl 17 |
. . . . . . . . 9
β’ ((π β π β§ πΈ β π) β (π β dom ((π Sat πΈ)ββ
) β βπ’ β ((π Sat πΈ)ββ
)(1st βπ’) = π)) |
53 | 3 | eleq2d 2820 |
. . . . . . . . 9
β’ ((π β π β§ πΈ β π) β (π β dom ((π Sat πΈ)ββ
) β π β
(Fmlaββ
))) |
54 | 52, 53 | bitr3d 281 |
. . . . . . . 8
β’ ((π β π β§ πΈ β π) β (βπ’ β ((π Sat πΈ)ββ
)(1st βπ’) = π β π β
(Fmlaββ
))) |
55 | | r19.41v 3182 |
. . . . . . . . . 10
β’
(βπ’ β
((π Sat πΈ)ββ
)((1st
βπ’) = π β§ (βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ)) β (βπ’ β ((π Sat πΈ)ββ
)(1st βπ’) = π β§ (βπ β (Fmlaββ
)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ))) |
56 | | oveq1 7368 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ’) = π β ((1st βπ’)βΌππ) = (πβΌππ)) |
57 | 56 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’
((1st βπ’) = π β (π₯ = ((1st βπ’)βΌππ) β π₯ = (πβΌππ))) |
58 | 57 | rexbidv 3172 |
. . . . . . . . . . . . . . 15
β’
((1st βπ’) = π β (βπ β (Fmlaββ
)π₯ = ((1st βπ’)βΌππ) β βπ β
(Fmlaββ
)π₯ =
(πβΌππ))) |
59 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ’) = π β π = π) |
60 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ’) = π β (1st βπ’) = π) |
61 | 59, 60 | goaleq12d 34009 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ’) = π β βππ(1st βπ’) =
βπππ) |
62 | 61 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’
((1st βπ’) = π β (π₯ = βππ(1st βπ’) β π₯ = βπππ)) |
63 | 62 | rexbidv 3172 |
. . . . . . . . . . . . . . 15
β’
((1st βπ’) = π β (βπ β Ο π₯ = βππ(1st βπ’) β βπ β Ο π₯ =
βπππ)) |
64 | 58, 63 | orbi12d 918 |
. . . . . . . . . . . . . 14
β’
((1st βπ’) = π β ((βπ β (Fmlaββ
)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)) β (βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ))) |
65 | 64 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ (1st
βπ’) = π) β ((βπ β
(Fmlaββ
)π₯ =
((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)) β (βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ))) |
66 | 3 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π β§ πΈ β π) β (Fmlaββ
) = dom ((π Sat πΈ)ββ
)) |
67 | 66 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π β§ πΈ β π) β (π β (Fmlaββ
) β π β dom ((π Sat πΈ)ββ
))) |
68 | | releldm2 7979 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Rel
((π Sat πΈ)ββ
) β (π β dom ((π Sat πΈ)ββ
) β βπ£ β ((π Sat πΈ)ββ
)(1st βπ£) = π)) |
69 | 16, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π β§ πΈ β π) β (π β dom ((π Sat πΈ)ββ
) β βπ£ β ((π Sat πΈ)ββ
)(1st βπ£) = π)) |
70 | 67, 69 | bitrd 279 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ πΈ β π) β (π β (Fmlaββ
) β
βπ£ β ((π Sat πΈ)ββ
)(1st βπ£) = π)) |
71 | | r19.41v 3182 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ£ β
((π Sat πΈ)ββ
)((1st
βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β (βπ£ β ((π Sat πΈ)ββ
)(1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ))) |
72 | 39 | eqcoms 2741 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((1st βπ£) = π β ((1st βπ’)βΌππ) = ((1st
βπ’)βΌπ(1st
βπ£))) |
73 | 72 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((1st βπ£) = π β (π₯ = ((1st βπ’)βΌππ) β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
74 | 73 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β π₯ = ((1st βπ’)βΌπ(1st
βπ£))) |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β π β§ πΈ β π) β (((1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
76 | 75 | reximdv 3164 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π β§ πΈ β π) β (βπ£ β ((π Sat πΈ)ββ
)((1st
βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
77 | 71, 76 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π β§ πΈ β π) β ((βπ£ β ((π Sat πΈ)ββ
)(1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
78 | 77 | expd 417 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ πΈ β π) β (βπ£ β ((π Sat πΈ)ββ
)(1st βπ£) = π β (π₯ = ((1st βπ’)βΌππ) β βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
79 | 70, 78 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ πΈ β π) β (π β (Fmlaββ
) β (π₯ = ((1st βπ’)βΌππ) β βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
80 | 79 | rexlimdv 3147 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ πΈ β π) β (βπ β (Fmlaββ
)π₯ = ((1st βπ’)βΌππ) β βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β (βπ β
(Fmlaββ
)π₯ =
((1st βπ’)βΌππ) β βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
82 | 81 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ (1st
βπ’) = π) β (βπ β
(Fmlaββ
)π₯ =
((1st βπ’)βΌππ) β βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
83 | 82 | orim1d 965 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ (1st
βπ’) = π) β ((βπ β
(Fmlaββ
)π₯ =
((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)) β (βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
84 | 65, 83 | sylbird 260 |
. . . . . . . . . . . 12
β’ ((((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β§ (1st
βπ’) = π) β ((βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ) β (βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
85 | 84 | expimpd 455 |
. . . . . . . . . . 11
β’ (((π β π β§ πΈ β π) β§ π’ β ((π Sat πΈ)ββ
)) β (((1st
βπ’) = π β§ (βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ)) β (βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
86 | 85 | reximdva 3162 |
. . . . . . . . . 10
β’ ((π β π β§ πΈ β π) β (βπ’ β ((π Sat πΈ)ββ
)((1st
βπ’) = π β§ (βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ)) β βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
87 | 55, 86 | biimtrrid 242 |
. . . . . . . . 9
β’ ((π β π β§ πΈ β π) β ((βπ’ β ((π Sat πΈ)ββ
)(1st βπ’) = π β§ (βπ β (Fmlaββ
)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ)) β βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
88 | 87 | expd 417 |
. . . . . . . 8
β’ ((π β π β§ πΈ β π) β (βπ’ β ((π Sat πΈ)ββ
)(1st βπ’) = π β ((βπ β (Fmlaββ
)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))))) |
89 | 54, 88 | sylbird 260 |
. . . . . . 7
β’ ((π β π β§ πΈ β π) β (π β (Fmlaββ
) β
((βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ) β βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))))) |
90 | 89 | rexlimdv 3147 |
. . . . . 6
β’ ((π β π β§ πΈ β π) β (βπ β (Fmlaββ
)(βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ) β βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
91 | 50, 90 | impbid 211 |
. . . . 5
β’ ((π β π β§ πΈ β π) β (βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β βπ β (Fmlaββ
)(βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ))) |
92 | 91 | abbidv 2802 |
. . . 4
β’ ((π β π β§ πΈ β π) β {π₯ β£ βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))} = {π₯ β£ βπ β (Fmlaββ
)(βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ)}) |
93 | 14, 92 | eqtrd 2773 |
. . 3
β’ ((π β π β§ πΈ β π) β dom {β¨π₯, π¦β© β£ βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = ((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))} = {π₯ β£ βπ β (Fmlaββ
)(βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ)}) |
94 | 3, 93 | ineq12d 4177 |
. 2
β’ ((π β π β§ πΈ β π) β (dom ((π Sat πΈ)ββ
) β© dom {β¨π₯, π¦β© β£ βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = ((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))}) = ((Fmlaββ
)
β© {π₯ β£
βπ β
(Fmlaββ
)(βπ β (Fmlaββ
)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ)})) |
95 | | fmla0disjsuc 34056 |
. 2
β’
((Fmlaββ
) β© {π₯ β£ βπ β (Fmlaββ
)(βπ β
(Fmlaββ
)π₯ =
(πβΌππ) β¨ βπ β Ο π₯ = βπππ)}) = β
|
96 | 94, 95 | eqtrdi 2789 |
1
β’ ((π β π β§ πΈ β π) β (dom ((π Sat πΈ)ββ
) β© dom {β¨π₯, π¦β© β£ βπ’ β ((π Sat πΈ)ββ
)(βπ£ β ((π Sat πΈ)ββ
)(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = ((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£)))) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = {π β (π βm Ο) β£
βπ β π ({β¨π, πβ©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)}))}) =
β
) |