Step | Hyp | Ref
| Expression |
1 | | satffunlem2lem2.s |
. . . . . 6
β’ π = (π Sat πΈ) |
2 | 1 | fveq1i 6847 |
. . . . 5
β’ (πβsuc π) = ((π Sat πΈ)βsuc π) |
3 | 2 | dmeqi 5864 |
. . . 4
β’ dom
(πβsuc π) = dom ((π Sat πΈ)βsuc π) |
4 | | simprl 770 |
. . . . . . 7
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β π β π) |
5 | | simprr 772 |
. . . . . . 7
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β πΈ β π) |
6 | | peano2 7831 |
. . . . . . . 8
β’ (π β Ο β suc π β
Ο) |
7 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β suc π β Ο) |
8 | 4, 5, 7 | 3jca 1129 |
. . . . . 6
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β (π β π β§ πΈ β π β§ suc π β Ο)) |
9 | | satfdmfmla 34058 |
. . . . . 6
β’ ((π β π β§ πΈ β π β§ suc π β Ο) β dom ((π Sat πΈ)βsuc π) = (Fmlaβsuc π)) |
10 | 8, 9 | syl 17 |
. . . . 5
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β dom ((π Sat πΈ)βsuc π) = (Fmlaβsuc π)) |
11 | 10 | adantr 482 |
. . . 4
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β dom ((π Sat πΈ)βsuc π) = (Fmlaβsuc π)) |
12 | 3, 11 | eqtrid 2785 |
. . 3
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β dom (πβsuc π) = (Fmlaβsuc π)) |
13 | | satffunlem2lem2.a |
. . . . . . . . . 10
β’ π΄ = ((π βm Ο) β
((2nd βπ’)
β© (2nd βπ£))) |
14 | | ovex 7394 |
. . . . . . . . . . 11
β’ (π βm Ο)
β V |
15 | 14 | difexi 5289 |
. . . . . . . . . 10
β’ ((π βm Ο)
β ((2nd βπ’) β© (2nd βπ£))) β V |
16 | 13, 15 | eqeltri 2830 |
. . . . . . . . 9
β’ π΄ β V |
17 | 16 | a1i 11 |
. . . . . . . 8
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβsuc π)) β§ π£ β (πβsuc π)) β π΄ β V) |
18 | 17 | ralrimiva 3140 |
. . . . . . 7
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβsuc π)) β βπ£ β (πβsuc π)π΄ β V) |
19 | | satffunlem2lem2.b |
. . . . . . . . . 10
β’ π΅ = {π β (π βm Ο) β£
βπ§ β π ({β¨π, π§β©} βͺ (π βΎ (Ο β {π}))) β (2nd βπ’)} |
20 | 19, 14 | rabex2 5295 |
. . . . . . . . 9
β’ π΅ β V |
21 | 20 | a1i 11 |
. . . . . . . 8
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβsuc π)) β§ π β Ο) β π΅ β V) |
22 | 21 | ralrimiva 3140 |
. . . . . . 7
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβsuc π)) β βπ β Ο π΅ β V) |
23 | 18, 22 | jca 513 |
. . . . . 6
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβsuc π)) β (βπ£ β (πβsuc π)π΄ β V β§ βπ β Ο π΅ β V)) |
24 | 23 | ralrimiva 3140 |
. . . . 5
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β βπ’ β (πβsuc π)(βπ£ β (πβsuc π)π΄ β V β§ βπ β Ο π΅ β V)) |
25 | | simplr 768 |
. . . . . . 7
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β π β§ πΈ β π)) |
26 | 6 | ancri 551 |
. . . . . . . 8
β’ (π β Ο β (suc
π β Ο β§
π β
Ο)) |
27 | 26 | ad2antrr 725 |
. . . . . . 7
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (suc π β Ο β§ π β Ο)) |
28 | 25, 27 | jca 513 |
. . . . . 6
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((π β π β§ πΈ β π) β§ (suc π β Ο β§ π β Ο))) |
29 | | sssucid 6401 |
. . . . . 6
β’ π β suc π |
30 | 1 | satfsschain 34022 |
. . . . . 6
β’ (((π β π β§ πΈ β π) β§ (suc π β Ο β§ π β Ο)) β (π β suc π β (πβπ) β (πβsuc π))) |
31 | 28, 29, 30 | mpisyl 21 |
. . . . 5
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (πβπ) β (πβsuc π)) |
32 | | dmopab3rexdif 34063 |
. . . . 5
β’
((βπ’ β
(πβsuc π)(βπ£ β (πβsuc π)π΄ β V β§ βπ β Ο π΅ β V) β§ (πβπ) β (πβsuc π)) β dom {β¨π₯, π¦β© β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = π΄) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = π΅)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = π΄))} = {π₯ β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))}) |
33 | 24, 31, 32 | syl2anc 585 |
. . . 4
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β dom {β¨π₯, π¦β© β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = π΄) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = π΅)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = π΄))} = {π₯ β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))}) |
34 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) |
35 | | fveqeq2 6855 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π’ β ((1st βπ€) = (1st βπ’) β (1st
βπ’) = (1st
βπ’))) |
36 | 35 | adantl 483 |
. . . . . . . . . . . . . . 15
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β§ π€ = π’) β ((1st βπ€) = (1st βπ’) β (1st
βπ’) = (1st
βπ’))) |
37 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β (1st βπ’) = (1st βπ’)) |
38 | 34, 36, 37 | rspcedvd 3585 |
. . . . . . . . . . . . . 14
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β βπ€ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ€) = (1st βπ’)) |
39 | 2 | funeqi 6526 |
. . . . . . . . . . . . . . . . . . 19
β’ (Fun
(πβsuc π) β Fun ((π Sat πΈ)βsuc π)) |
40 | 39 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ (Fun
(πβsuc π) β Fun ((π Sat πΈ)βsuc π)) |
41 | 40 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β Fun ((π Sat πΈ)βsuc π)) |
42 | 1 | fveq1i 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (πβπ) = ((π Sat πΈ)βπ) |
43 | 31, 42, 2 | 3sstr3g 3992 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((π Sat πΈ)βπ) β ((π Sat πΈ)βsuc π)) |
44 | 41, 43 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (Fun ((π Sat πΈ)βsuc π) β§ ((π Sat πΈ)βπ) β ((π Sat πΈ)βsuc π))) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β (Fun ((π Sat πΈ)βsuc π) β§ ((π Sat πΈ)βπ) β ((π Sat πΈ)βsuc π))) |
46 | | funeldmdif 7984 |
. . . . . . . . . . . . . . 15
β’ ((Fun
((π Sat πΈ)βsuc π) β§ ((π Sat πΈ)βπ) β ((π Sat πΈ)βsuc π)) β ((1st βπ’) β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)) β βπ€ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ€) = (1st βπ’))) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β ((1st βπ’) β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)) β βπ€ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ€) = (1st βπ’))) |
48 | 38, 47 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β (1st βπ’) β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ))) |
49 | 48 | ex 414 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ)) β (1st βπ’) β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)))) |
50 | 2, 42 | difeq12i 4084 |
. . . . . . . . . . . . . 14
β’ ((πβsuc π) β (πβπ)) = (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ)) |
51 | 50 | eleq2i 2826 |
. . . . . . . . . . . . 13
β’ (π’ β ((πβsuc π) β (πβπ)) β π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) |
52 | 51 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π’ β ((πβsuc π) β (πβπ)) β π’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ)))) |
53 | 11 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (Fmlaβsuc π) = dom ((π Sat πΈ)βsuc π)) |
54 | | simpl 484 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β π β Ο) |
55 | 4, 5, 54 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β (π β π β§ πΈ β π β§ π β Ο)) |
56 | | satfdmfmla 34058 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ πΈ β π β§ π β Ο) β dom ((π Sat πΈ)βπ) = (Fmlaβπ)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β dom ((π Sat πΈ)βπ) = (Fmlaβπ)) |
58 | 57 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β (Fmlaβπ) = dom ((π Sat πΈ)βπ)) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (Fmlaβπ) = dom ((π Sat πΈ)βπ)) |
60 | 53, 59 | difeq12d 4087 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((Fmlaβsuc π) β (Fmlaβπ)) = (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ))) |
61 | 60 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((1st βπ’) β ((Fmlaβsuc π) β (Fmlaβπ)) β (1st
βπ’) β (dom
((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)))) |
62 | 49, 52, 61 | 3imtr4d 294 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π’ β ((πβsuc π) β (πβπ)) β (1st βπ’) β ((Fmlaβsuc π) β (Fmlaβπ)))) |
63 | 62 | imp 408 |
. . . . . . . . . 10
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β (1st βπ’) β ((Fmlaβsuc π) β (Fmlaβπ))) |
64 | 63 | adantr 482 |
. . . . . . . . 9
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ (βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))) β (1st βπ’) β ((Fmlaβsuc π) β (Fmlaβπ))) |
65 | | oveq1 7368 |
. . . . . . . . . . . . 13
β’ (π = (1st βπ’) β (πβΌππ) = ((1st βπ’)βΌππ)) |
66 | 65 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π = (1st βπ’) β (π₯ = (πβΌππ) β π₯ = ((1st βπ’)βΌππ))) |
67 | 66 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π = (1st βπ’) β (βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ))) |
68 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ (π = (1st βπ’) β π = π) |
69 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = (1st βπ’) β π = (1st βπ’)) |
70 | 68, 69 | goaleq12d 34009 |
. . . . . . . . . . . . 13
β’ (π = (1st βπ’) β
βπππ = βππ(1st βπ’)) |
71 | 70 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π = (1st βπ’) β (π₯ = βπππ β π₯ = βππ(1st βπ’))) |
72 | 71 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π = (1st βπ’) β (βπ β Ο π₯ =
βπππ β βπ β Ο π₯ = βππ(1st βπ’))) |
73 | 67, 72 | orbi12d 918 |
. . . . . . . . . 10
β’ (π = (1st βπ’) β ((βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β (βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)))) |
74 | 73 | adantl 483 |
. . . . . . . . 9
β’
((((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ (βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))) β§ π = (1st βπ’)) β ((βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β (βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)))) |
75 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β π β π) |
76 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β πΈ β π) |
77 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β suc π β Ο) |
78 | 75, 76, 77 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β π β§ πΈ β π β§ suc π β Ο)) |
79 | | satfrel 34025 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ πΈ β π β§ suc π β Ο) β Rel ((π Sat πΈ)βsuc π)) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β Rel ((π Sat πΈ)βsuc π)) |
81 | 2 | releqi 5737 |
. . . . . . . . . . . . . . . . 17
β’ (Rel
(πβsuc π) β Rel ((π Sat πΈ)βsuc π)) |
82 | 80, 81 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β Rel (πβsuc π)) |
83 | | 1stdm 7976 |
. . . . . . . . . . . . . . . 16
β’ ((Rel
(πβsuc π) β§ π£ β (πβsuc π)) β (1st βπ£) β dom (πβsuc π)) |
84 | 82, 83 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π£ β (πβsuc π)) β (1st βπ£) β dom (πβsuc π)) |
85 | 12 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (Fmlaβsuc π) = dom (πβsuc π)) |
86 | 85 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π£ β (πβsuc π)) β (Fmlaβsuc π) = dom (πβsuc π)) |
87 | 84, 86 | eleqtrrd 2837 |
. . . . . . . . . . . . . 14
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π£ β (πβsuc π)) β (1st βπ£) β (Fmlaβsuc π)) |
88 | 87 | ad4ant13 750 |
. . . . . . . . . . . . 13
β’
((((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ π£ β (πβsuc π)) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
(1st βπ£)
β (Fmlaβsuc π)) |
89 | | oveq2 7369 |
. . . . . . . . . . . . . . 15
β’ (π = (1st βπ£) β ((1st
βπ’)βΌππ) = ((1st
βπ’)βΌπ(1st
βπ£))) |
90 | 89 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
β’ (π = (1st βπ£) β (π₯ = ((1st βπ’)βΌππ) β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
91 | 90 | adantl 483 |
. . . . . . . . . . . . 13
β’
(((((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ π£ β (πβsuc π)) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β§ π = (1st βπ£)) β (π₯ = ((1st βπ’)βΌππ) β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
92 | | simpr 486 |
. . . . . . . . . . . . 13
β’
((((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ π£ β (πβsuc π)) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β π₯ = ((1st βπ’)βΌπ(1st
βπ£))) |
93 | 88, 91, 92 | rspcedvd 3585 |
. . . . . . . . . . . 12
β’
((((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ π£ β (πβsuc π)) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
βπ β
(Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ)) |
94 | 93 | rexlimdva2 3151 |
. . . . . . . . . . 11
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β (βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β
βπ β
(Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ))) |
95 | 94 | orim1d 965 |
. . . . . . . . . 10
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β ((βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β (βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)))) |
96 | 95 | imp 408 |
. . . . . . . . 9
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ (βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))) β (βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’))) |
97 | 64, 74, 96 | rspcedvd 3585 |
. . . . . . . 8
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ (βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))) β βπ β ((Fmlaβsuc π) β (Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ)) |
98 | 97 | rexlimdva2 3151 |
. . . . . . 7
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β βπ β ((Fmlaβsuc π) β (Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ))) |
99 | 55 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β π β§ πΈ β π β§ π β Ο)) |
100 | | satfrel 34025 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ πΈ β π β§ π β Ο) β Rel ((π Sat πΈ)βπ)) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β Rel ((π Sat πΈ)βπ)) |
102 | 42 | releqi 5737 |
. . . . . . . . . . . . 13
β’ (Rel
(πβπ) β Rel ((π Sat πΈ)βπ)) |
103 | 101, 102 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β Rel (πβπ)) |
104 | | 1stdm 7976 |
. . . . . . . . . . . 12
β’ ((Rel
(πβπ) β§ π’ β (πβπ)) β (1st βπ’) β dom (πβπ)) |
105 | 103, 104 | sylan 581 |
. . . . . . . . . . 11
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β (1st βπ’) β dom (πβπ)) |
106 | 42 | dmeqi 5864 |
. . . . . . . . . . . . . 14
β’ dom
(πβπ) = dom ((π Sat πΈ)βπ) |
107 | 99, 56 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β dom ((π Sat πΈ)βπ) = (Fmlaβπ)) |
108 | 106, 107 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β dom (πβπ) = (Fmlaβπ)) |
109 | 108 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (Fmlaβπ) = dom (πβπ)) |
110 | 109 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β (Fmlaβπ) = dom (πβπ)) |
111 | 105, 110 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β (1st βπ’) β (Fmlaβπ)) |
112 | 111 | adantr 482 |
. . . . . . . . 9
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β§ βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
(1st βπ’)
β (Fmlaβπ)) |
113 | 66 | rexbidv 3172 |
. . . . . . . . . 10
β’ (π = (1st βπ’) β (βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ) β βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = ((1st βπ’)βΌππ))) |
114 | 113 | adantl 483 |
. . . . . . . . 9
β’
((((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β§ βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β§ π = (1st βπ’)) β (βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ) β βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = ((1st βπ’)βΌππ))) |
115 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) |
116 | | fveqeq2 6855 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = π£ β ((1st βπ‘) = (1st βπ£) β (1st
βπ£) = (1st
βπ£))) |
117 | 116 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β§ π‘ = π£) β ((1st βπ‘) = (1st βπ£) β (1st
βπ£) = (1st
βπ£))) |
118 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β (1st βπ£) = (1st βπ£)) |
119 | 115, 117,
118 | rspcedvd 3585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β βπ‘ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ‘) = (1st βπ£)) |
120 | 44 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β (Fun ((π Sat πΈ)βsuc π) β§ ((π Sat πΈ)βπ) β ((π Sat πΈ)βsuc π))) |
121 | | funeldmdif 7984 |
. . . . . . . . . . . . . . . . . 18
β’ ((Fun
((π Sat πΈ)βsuc π) β§ ((π Sat πΈ)βπ) β ((π Sat πΈ)βsuc π)) β ((1st βπ£) β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)) β βπ‘ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ‘) = (1st βπ£))) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β ((1st βπ£) β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)) β βπ‘ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ‘) = (1st βπ£))) |
123 | 119, 122 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) β (1st βπ£) β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ))) |
124 | 123 | ex 414 |
. . . . . . . . . . . . . . 15
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ)) β (1st βπ£) β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)))) |
125 | 50 | eleq2i 2826 |
. . . . . . . . . . . . . . . 16
β’ (π£ β ((πβsuc π) β (πβπ)) β π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))) |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π£ β ((πβsuc π) β (πβπ)) β π£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ)))) |
127 | 10 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β (Fmlaβsuc π) = dom ((π Sat πΈ)βsuc π)) |
128 | 127, 58 | difeq12d 4087 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β ((Fmlaβsuc π) β (Fmlaβπ)) = (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ))) |
129 | 128 | eleq2d 2820 |
. . . . . . . . . . . . . . . 16
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β ((1st βπ£) β ((Fmlaβsuc π) β (Fmlaβπ)) β (1st
βπ£) β (dom
((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)))) |
130 | 129 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((1st βπ£) β ((Fmlaβsuc π) β (Fmlaβπ)) β (1st
βπ£) β (dom
((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)))) |
131 | 124, 126,
130 | 3imtr4d 294 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π£ β ((πβsuc π) β (πβπ)) β (1st βπ£) β ((Fmlaβsuc π) β (Fmlaβπ)))) |
132 | 131 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β (π£ β ((πβsuc π) β (πβπ)) β (1st βπ£) β ((Fmlaβsuc π) β (Fmlaβπ)))) |
133 | 132 | imp 408 |
. . . . . . . . . . . 12
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β§ π£ β ((πβsuc π) β (πβπ))) β (1st βπ£) β ((Fmlaβsuc π) β (Fmlaβπ))) |
134 | 133 | adantr 482 |
. . . . . . . . . . 11
β’
((((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β§ π£ β ((πβsuc π) β (πβπ))) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
(1st βπ£)
β ((Fmlaβsuc π)
β (Fmlaβπ))) |
135 | 90 | adantl 483 |
. . . . . . . . . . 11
β’
(((((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β§ π£ β ((πβsuc π) β (πβπ))) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β§ π = (1st βπ£)) β (π₯ = ((1st βπ’)βΌππ) β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
136 | | simpr 486 |
. . . . . . . . . . 11
β’
((((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β§ π£ β ((πβsuc π) β (πβπ))) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β π₯ = ((1st βπ’)βΌπ(1st
βπ£))) |
137 | 134, 135,
136 | rspcedvd 3585 |
. . . . . . . . . 10
β’
((((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β§ π£ β ((πβsuc π) β (πβπ))) β§ π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
βπ β
((Fmlaβsuc π) β
(Fmlaβπ))π₯ = ((1st βπ’)βΌππ)) |
138 | 137 | r19.29an 3152 |
. . . . . . . . 9
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β§ βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
βπ β
((Fmlaβsuc π) β
(Fmlaβπ))π₯ = ((1st βπ’)βΌππ)) |
139 | 112, 114,
138 | rspcedvd 3585 |
. . . . . . . 8
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β (πβπ)) β§ βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
βπ β
(Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ)) |
140 | 139 | rexlimdva2 3151 |
. . . . . . 7
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β
βπ β
(Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ))) |
141 | 98, 140 | orim12d 964 |
. . . . . 6
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
(βπ β
((Fmlaβsuc π) β
(Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β¨ βπ β (Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ)))) |
142 | 8 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β π β§ πΈ β π β§ suc π β Ο)) |
143 | 9 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ ((π β π β§ πΈ β π β§ suc π β Ο) β (Fmlaβsuc
π) = dom ((π Sat πΈ)βsuc π)) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (Fmlaβsuc π) = dom ((π Sat πΈ)βsuc π)) |
145 | 107 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (Fmlaβπ) = dom ((π Sat πΈ)βπ)) |
146 | 144, 145 | difeq12d 4087 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((Fmlaβsuc π) β (Fmlaβπ)) = (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ))) |
147 | 146 | eleq2d 2820 |
. . . . . . . . . 10
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β ((Fmlaβsuc π) β (Fmlaβπ)) β π β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)))) |
148 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π Sat πΈ) = (π Sat πΈ) |
149 | 148 | satfsschain 34022 |
. . . . . . . . . . . 12
β’ (((π β π β§ πΈ β π) β§ (suc π β Ο β§ π β Ο)) β (π β suc π β ((π Sat πΈ)βπ) β ((π Sat πΈ)βsuc π))) |
150 | 28, 29, 149 | mpisyl 21 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((π Sat πΈ)βπ) β ((π Sat πΈ)βsuc π)) |
151 | | releldmdifi 7981 |
. . . . . . . . . . 11
β’ ((Rel
((π Sat πΈ)βsuc π) β§ ((π Sat πΈ)βπ) β ((π Sat πΈ)βsuc π)) β (π β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)) β βπ’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ’) = π)) |
152 | 80, 150, 151 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)) β βπ’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ’) = π)) |
153 | 147, 152 | sylbid 239 |
. . . . . . . . 9
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β ((Fmlaβsuc π) β (Fmlaβπ)) β βπ’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ’) = π)) |
154 | 50 | eqcomi 2742 |
. . . . . . . . . . 11
β’ (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ)) = ((πβsuc π) β (πβπ)) |
155 | 154 | rexeqi 3311 |
. . . . . . . . . 10
β’
(βπ’ β
(((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ’) = π β βπ’ β ((πβsuc π) β (πβπ))(1st βπ’) = π) |
156 | | r19.41v 3182 |
. . . . . . . . . . . 12
β’
(βπ’ β
((πβsuc π) β (πβπ))((1st βπ’) = π β§ (βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ)) β (βπ’ β ((πβsuc π) β (πβπ))(1st βπ’) = π β§ (βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ))) |
157 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . 19
β’
((1st βπ’) = π β ((1st βπ’)βΌππ) = (πβΌππ)) |
158 | 157 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ’) = π β (π₯ = ((1st βπ’)βΌππ) β π₯ = (πβΌππ))) |
159 | 158 | rexbidv 3172 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ’) = π β (βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ) β βπ β (Fmlaβsuc π)π₯ = (πβΌππ))) |
160 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1st βπ’) = π β π = π) |
161 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1st βπ’) = π β (1st βπ’) = π) |
162 | 160, 161 | goaleq12d 34009 |
. . . . . . . . . . . . . . . . . . 19
β’
((1st βπ’) = π β βππ(1st βπ’) =
βπππ) |
163 | 162 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ’) = π β (π₯ = βππ(1st βπ’) β π₯ = βπππ)) |
164 | 163 | rexbidv 3172 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ’) = π β (βπ β Ο π₯ = βππ(1st βπ’) β βπ β Ο π₯ =
βπππ)) |
165 | 159, 164 | orbi12d 918 |
. . . . . . . . . . . . . . . 16
β’
((1st βπ’) = π β ((βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)) β (βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ))) |
166 | 165 | adantl 483 |
. . . . . . . . . . . . . . 15
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ (1st βπ’) = π) β ((βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)) β (βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ))) |
167 | 142, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β dom ((π Sat πΈ)βsuc π) = (Fmlaβsuc π)) |
168 | 167 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (Fmlaβsuc π) = dom ((π Sat πΈ)βsuc π)) |
169 | 168 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β (Fmlaβsuc π) β π β dom ((π Sat πΈ)βsuc π))) |
170 | | releldm2 7979 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Rel
((π Sat πΈ)βsuc π) β (π β dom ((π Sat πΈ)βsuc π) β βπ£ β ((π Sat πΈ)βsuc π)(1st βπ£) = π)) |
171 | 80, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β dom ((π Sat πΈ)βsuc π) β βπ£ β ((π Sat πΈ)βsuc π)(1st βπ£) = π)) |
172 | 169, 171 | bitrd 279 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β (Fmlaβsuc π) β βπ£ β ((π Sat πΈ)βsuc π)(1st βπ£) = π)) |
173 | | r19.41v 3182 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ£ β
((π Sat πΈ)βsuc π)((1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β (βπ£ β ((π Sat πΈ)βsuc π)(1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ))) |
174 | 1 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π Sat πΈ) = π |
175 | 174 | fveq1i 6847 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π Sat πΈ)βsuc π) = (πβsuc π) |
176 | 175 | rexeqi 3311 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ£ β
((π Sat πΈ)βsuc π)((1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β βπ£ β (πβsuc π)((1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ))) |
177 | 89 | eqcoms 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((1st βπ£) = π β ((1st βπ’)βΌππ) = ((1st
βπ’)βΌπ(1st
βπ£))) |
178 | 177 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((1st βπ£) = π β (π₯ = ((1st βπ’)βΌππ) β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
179 | 178 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β π₯ = ((1st βπ’)βΌπ(1st
βπ£))) |
180 | 179 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (((1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
181 | 180 | reximdv 3164 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ£ β (πβsuc π)((1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
182 | 176, 181 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ£ β ((π Sat πΈ)βsuc π)((1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
183 | 173, 182 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((βπ£ β ((π Sat πΈ)βsuc π)(1st βπ£) = π β§ π₯ = ((1st βπ’)βΌππ)) β βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
184 | 183 | expd 417 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ£ β ((π Sat πΈ)βsuc π)(1st βπ£) = π β (π₯ = ((1st βπ’)βΌππ) β βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
185 | 172, 184 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β (Fmlaβsuc π) β (π₯ = ((1st βπ’)βΌππ) β βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
186 | 185 | rexlimdv 3147 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ) β βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
187 | 186 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ (1st βπ’) = π) β (βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ) β βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
188 | 187 | orim1d 965 |
. . . . . . . . . . . . . . 15
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ (1st βπ’) = π) β ((βπ β (Fmlaβsuc π)π₯ = ((1st βπ’)βΌππ) β¨ βπ β Ο π₯ = βππ(1st βπ’)) β (βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
189 | 166, 188 | sylbird 260 |
. . . . . . . . . . . . . 14
β’
(((((π β
Ο β§ (π β
π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β§ (1st βπ’) = π) β ((βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β (βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
190 | 189 | expimpd 455 |
. . . . . . . . . . . . 13
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π’ β ((πβsuc π) β (πβπ))) β (((1st βπ’) = π β§ (βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ)) β (βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
191 | 190 | reximdva 3162 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ’ β ((πβsuc π) β (πβπ))((1st βπ’) = π β§ (βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ)) β βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
192 | 156, 191 | biimtrrid 242 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((βπ’ β ((πβsuc π) β (πβπ))(1st βπ’) = π β§ (βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ)) β βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
193 | 192 | expd 417 |
. . . . . . . . . 10
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ’ β ((πβsuc π) β (πβπ))(1st βπ’) = π β ((βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))))) |
194 | 155, 193 | biimtrid 241 |
. . . . . . . . 9
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ’ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ’) = π β ((βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))))) |
195 | 153, 194 | syld 47 |
. . . . . . . 8
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β ((Fmlaβsuc π) β (Fmlaβπ)) β ((βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’))))) |
196 | 195 | rexlimdv 3147 |
. . . . . . 7
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ β ((Fmlaβsuc π) β (Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)))) |
197 | 145 | eleq2d 2820 |
. . . . . . . . . 10
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β (Fmlaβπ) β π β dom ((π Sat πΈ)βπ))) |
198 | 55, 100 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β Ο β§ (π β π β§ πΈ β π)) β Rel ((π Sat πΈ)βπ)) |
199 | 198 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β Rel ((π Sat πΈ)βπ)) |
200 | | releldm2 7979 |
. . . . . . . . . . 11
β’ (Rel
((π Sat πΈ)βπ) β (π β dom ((π Sat πΈ)βπ) β βπ’ β ((π Sat πΈ)βπ)(1st βπ’) = π)) |
201 | 199, 200 | syl 17 |
. . . . . . . . . 10
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β dom ((π Sat πΈ)βπ) β βπ’ β ((π Sat πΈ)βπ)(1st βπ’) = π)) |
202 | 197, 201 | bitrd 279 |
. . . . . . . . 9
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β (Fmlaβπ) β βπ’ β ((π Sat πΈ)βπ)(1st βπ’) = π)) |
203 | | r19.41v 3182 |
. . . . . . . . . . 11
β’
(βπ’ β
((π Sat πΈ)βπ)((1st βπ’) = π β§ βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ)) β (βπ’ β ((π Sat πΈ)βπ)(1st βπ’) = π β§ βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ))) |
204 | 42 | eqcomi 2742 |
. . . . . . . . . . . . 13
β’ ((π Sat πΈ)βπ) = (πβπ) |
205 | 204 | rexeqi 3311 |
. . . . . . . . . . . 12
β’
(βπ’ β
((π Sat πΈ)βπ)((1st βπ’) = π β§ βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ)) β βπ’ β (πβπ)((1st βπ’) = π β§ βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ))) |
206 | 158 | rexbidv 3172 |
. . . . . . . . . . . . . . . 16
β’
((1st βπ’) = π β (βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = ((1st βπ’)βΌππ) β βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ))) |
207 | 206 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ (1st βπ’) = π) β (βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = ((1st βπ’)βΌππ) β βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ))) |
208 | 146 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β ((Fmlaβsuc π) β (Fmlaβπ)) β π β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)))) |
209 | | releldmdifi 7981 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((Rel
((π Sat πΈ)βsuc π) β§ ((π Sat πΈ)βπ) β ((π Sat πΈ)βsuc π)) β (π β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)) β βπ£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ£) = π)) |
210 | 80, 150, 209 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β (dom ((π Sat πΈ)βsuc π) β dom ((π Sat πΈ)βπ)) β βπ£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ£) = π)) |
211 | 208, 210 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β ((Fmlaβsuc π) β (Fmlaβπ)) β βπ£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ£) = π)) |
212 | 154 | rexeqi 3311 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ£ β
(((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ£) = π β βπ£ β ((πβsuc π) β (πβπ))(1st βπ£) = π) |
213 | 178 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = ((1st βπ’)βΌππ) β ((1st
βπ£) = π β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
214 | 213 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π₯ = ((1st βπ’)βΌππ)) β ((1st
βπ£) = π β π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
215 | 214 | reximdv 3164 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ π₯ = ((1st βπ’)βΌππ)) β (βπ£ β ((πβsuc π) β (πβπ))(1st βπ£) = π β βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
216 | 215 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π₯ = ((1st βπ’)βΌππ) β (βπ£ β ((πβsuc π) β (πβπ))(1st βπ£) = π β βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
217 | 216 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ£ β ((πβsuc π) β (πβπ))(1st βπ£) = π β (π₯ = ((1st βπ’)βΌππ) β βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
218 | 212, 217 | biimtrid 241 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ£ β (((π Sat πΈ)βsuc π) β ((π Sat πΈ)βπ))(1st βπ£) = π β (π₯ = ((1st βπ’)βΌππ) β βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
219 | 211, 218 | syld 47 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β ((Fmlaβsuc π) β (Fmlaβπ)) β (π₯ = ((1st βπ’)βΌππ) β βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
220 | 219 | rexlimdv 3147 |
. . . . . . . . . . . . . . . 16
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = ((1st βπ’)βΌππ) β βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
221 | 220 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ (1st βπ’) = π) β (βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = ((1st βπ’)βΌππ) β βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
222 | 207, 221 | sylbird 260 |
. . . . . . . . . . . . . 14
β’ ((((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β§ (1st βπ’) = π) β (βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ) β βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
223 | 222 | expimpd 455 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (((1st βπ’) = π β§ βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ)) β βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
224 | 223 | reximdv 3164 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ’ β (πβπ)((1st βπ’) = π β§ βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ)) β βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
225 | 205, 224 | biimtrid 241 |
. . . . . . . . . . 11
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ’ β ((π Sat πΈ)βπ)((1st βπ’) = π β§ βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ)) β βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
226 | 203, 225 | biimtrrid 242 |
. . . . . . . . . 10
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((βπ’ β ((π Sat πΈ)βπ)(1st βπ’) = π β§ βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ)) β βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
227 | 226 | expd 417 |
. . . . . . . . 9
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ’ β ((π Sat πΈ)βπ)(1st βπ’) = π β (βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ) β βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
228 | 202, 227 | sylbid 239 |
. . . . . . . 8
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (π β (Fmlaβπ) β (βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ) β βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
229 | 228 | rexlimdv 3147 |
. . . . . . 7
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (βπ β (Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ) β βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))) |
230 | 196, 229 | orim12d 964 |
. . . . . 6
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((βπ β ((Fmlaβsuc π) β (Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β¨ βπ β (Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ)) β (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))))) |
231 | 141, 230 | impbid 211 |
. . . . 5
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£))) β
(βπ β
((Fmlaβsuc π) β
(Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β¨ βπ β (Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ)))) |
232 | 231 | abbidv 2802 |
. . . 4
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β {π₯ β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β¨
βπ β Ο
π₯ =
βππ(1st βπ’)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))π₯ = ((1st βπ’)βΌπ(1st
βπ£)))} = {π₯ β£ (βπ β ((Fmlaβsuc π) β (Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β¨ βπ β (Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ))}) |
233 | 33, 232 | eqtrd 2773 |
. . 3
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β dom {β¨π₯, π¦β© β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = π΄) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = π΅)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = π΄))} = {π₯ β£ (βπ β ((Fmlaβsuc π) β (Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β¨ βπ β (Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ))}) |
234 | 12, 233 | ineq12d 4177 |
. 2
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (dom (πβsuc π) β© dom {β¨π₯, π¦β© β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = π΄) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = π΅)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = π΄))}) = ((Fmlaβsuc π) β© {π₯ β£ (βπ β ((Fmlaβsuc π) β (Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β¨ βπ β (Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ))})) |
235 | | fmlasucdisj 34057 |
. . 3
β’ (π β Ο β
((Fmlaβsuc π) β©
{π₯ β£ (βπ β ((Fmlaβsuc π) β (Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β¨ βπ β (Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ))}) = β
) |
236 | 235 | ad2antrr 725 |
. 2
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β ((Fmlaβsuc π) β© {π₯ β£ (βπ β ((Fmlaβsuc π) β (Fmlaβπ))(βπ β (Fmlaβsuc π)π₯ = (πβΌππ) β¨ βπ β Ο π₯ = βπππ) β¨ βπ β (Fmlaβπ)βπ β ((Fmlaβsuc π) β (Fmlaβπ))π₯ = (πβΌππ))}) = β
) |
237 | 234, 236 | eqtrd 2773 |
1
β’ (((π β Ο β§ (π β π β§ πΈ β π)) β§ Fun (πβsuc π)) β (dom (πβsuc π) β© dom {β¨π₯, π¦β© β£ (βπ’ β ((πβsuc π) β (πβπ))(βπ£ β (πβsuc π)(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = π΄) β¨ βπ β Ο (π₯ = βππ(1st βπ’) β§ π¦ = π΅)) β¨ βπ’ β (πβπ)βπ£ β ((πβsuc π) β (πβπ))(π₯ = ((1st βπ’)βΌπ(1st
βπ£)) β§ π¦ = π΄))}) = β
) |