Step | Hyp | Ref
| Expression |
1 | | mbfresfi.1 |
. 2
β’ (π β πΉ:π΄βΆβ) |
2 | | mbfresfi.3 |
. 2
β’ (π β βπ β π (πΉ βΎ π ) β MblFn) |
3 | | mbfresfi.4 |
. . 3
β’ (π β βͺ π =
π΄) |
4 | | mbfresfi.2 |
. . . . . . 7
β’ (π β π β Fin) |
5 | 4 | uniexd 7679 |
. . . . . 6
β’ (π β βͺ π
β V) |
6 | 3, 5 | eqeltrrd 2838 |
. . . . 5
β’ (π β π΄ β V) |
7 | | fex 7176 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β V) β πΉ β V) |
8 | 7 | ex 413 |
. . . . . 6
β’ (πΉ:π΄βΆβ β (π΄ β V β πΉ β V)) |
9 | 1, 8 | syl 17 |
. . . . 5
β’ (π β (π΄ β V β πΉ β V)) |
10 | 6, 9 | jcai 517 |
. . . 4
β’ (π β (π΄ β V β§ πΉ β V)) |
11 | | feq2 6650 |
. . . . . . . . 9
β’ (π = π΄ β (π:πβΆβ β π:π΄βΆβ)) |
12 | 11 | anbi1d 630 |
. . . . . . . 8
β’ (π = π΄ β ((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β (π:π΄βΆβ β§ βπ β π (π βΎ π ) β MblFn))) |
13 | | eqeq2 2748 |
. . . . . . . 8
β’ (π = π΄ β (βͺ π = π β βͺ π = π΄)) |
14 | 12, 13 | anbi12d 631 |
. . . . . . 7
β’ (π = π΄ β (((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β ((π:π΄βΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π΄))) |
15 | 14 | imbi1d 341 |
. . . . . 6
β’ (π = π΄ β ((((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β (((π:π΄βΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π΄) β π β
MblFn))) |
16 | 15 | imbi2d 340 |
. . . . 5
β’ (π = π΄ β ((π β (((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn)) β (π β (((π:π΄βΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π΄) β π β
MblFn)))) |
17 | | feq1 6649 |
. . . . . . . . 9
β’ (π = πΉ β (π:π΄βΆβ β πΉ:π΄βΆβ)) |
18 | | reseq1 5931 |
. . . . . . . . . . 11
β’ (π = πΉ β (π βΎ π ) = (πΉ βΎ π )) |
19 | 18 | eleq1d 2822 |
. . . . . . . . . 10
β’ (π = πΉ β ((π βΎ π ) β MblFn β (πΉ βΎ π ) β MblFn)) |
20 | 19 | ralbidv 3174 |
. . . . . . . . 9
β’ (π = πΉ β (βπ β π (π βΎ π ) β MblFn β βπ β π (πΉ βΎ π ) β MblFn)) |
21 | 17, 20 | anbi12d 631 |
. . . . . . . 8
β’ (π = πΉ β ((π:π΄βΆβ β§ βπ β π (π βΎ π ) β MblFn) β (πΉ:π΄βΆβ β§ βπ β π (πΉ βΎ π ) β MblFn))) |
22 | 21 | anbi1d 630 |
. . . . . . 7
β’ (π = πΉ β (((π:π΄βΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π΄) β ((πΉ:π΄βΆβ β§ βπ β π (πΉ βΎ π ) β MblFn) β§ βͺ π =
π΄))) |
23 | | eleq1 2825 |
. . . . . . 7
β’ (π = πΉ β (π β MblFn β πΉ β MblFn)) |
24 | 22, 23 | imbi12d 344 |
. . . . . 6
β’ (π = πΉ β ((((π:π΄βΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π΄) β π β MblFn) β (((πΉ:π΄βΆβ β§ βπ β π (πΉ βΎ π ) β MblFn) β§ βͺ π =
π΄) β πΉ β MblFn))) |
25 | 24 | imbi2d 340 |
. . . . 5
β’ (π = πΉ β ((π β (((π:π΄βΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π΄) β π β MblFn)) β (π β (((πΉ:π΄βΆβ β§ βπ β π (πΉ βΎ π ) β MblFn) β§ βͺ π =
π΄) β πΉ β MblFn)))) |
26 | | rzal 4466 |
. . . . . . . . . . . 12
β’ (π = β
β βπ β π (π βΎ π ) β MblFn) |
27 | 26 | biantrud 532 |
. . . . . . . . . . 11
β’ (π = β
β (π:πβΆβ β (π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn))) |
28 | 27 | bicomd 222 |
. . . . . . . . . 10
β’ (π = β
β ((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β π:πβΆβ)) |
29 | | unieq 4876 |
. . . . . . . . . . . 12
β’ (π = β
β βͺ π =
βͺ β
) |
30 | | uni0 4896 |
. . . . . . . . . . . 12
β’ βͺ β
= β
|
31 | 29, 30 | eqtrdi 2792 |
. . . . . . . . . . 11
β’ (π = β
β βͺ π =
β
) |
32 | 31 | eqeq1d 2738 |
. . . . . . . . . 10
β’ (π = β
β (βͺ π =
π β β
= π)) |
33 | 28, 32 | anbi12d 631 |
. . . . . . . . 9
β’ (π = β
β (((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β (π:πβΆβ β§ β
= π))) |
34 | 33 | imbi1d 341 |
. . . . . . . 8
β’ (π = β
β ((((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β ((π:πβΆβ β§ β
= π) β π β MblFn))) |
35 | 34 | 2albidv 1926 |
. . . . . . 7
β’ (π = β
β (βπβπ(((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β
βπβπ((π:πβΆβ β§ β
= π) β π β MblFn))) |
36 | | raleq 3309 |
. . . . . . . . . . . 12
β’ (π = π‘ β (βπ β π (π βΎ π ) β MblFn β βπ β π‘ (π βΎ π ) β MblFn)) |
37 | 36 | anbi2d 629 |
. . . . . . . . . . 11
β’ (π = π‘ β ((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β (π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn))) |
38 | | unieq 4876 |
. . . . . . . . . . . 12
β’ (π = π‘ β βͺ π = βͺ
π‘) |
39 | 38 | eqeq1d 2738 |
. . . . . . . . . . 11
β’ (π = π‘ β (βͺ π = π β βͺ π‘ = π)) |
40 | 37, 39 | anbi12d 631 |
. . . . . . . . . 10
β’ (π = π‘ β (((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β ((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π))) |
41 | 40 | imbi1d 341 |
. . . . . . . . 9
β’ (π = π‘ β ((((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β (((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β
MblFn))) |
42 | 41 | 2albidv 1926 |
. . . . . . . 8
β’ (π = π‘ β (βπβπ(((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β
βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β
MblFn))) |
43 | | simpl 483 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β π = π) |
44 | | simpr 485 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β π = π) |
45 | 43, 44 | feq12d 6656 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π) β (π:πβΆβ β π:πβΆβ)) |
46 | | reseq1 5931 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π βΎ π ) = (π βΎ π )) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π = π) β (π βΎ π ) = (π βΎ π )) |
48 | 47 | eleq1d 2822 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = π) β ((π βΎ π ) β MblFn β (π βΎ π ) β MblFn)) |
49 | 48 | ralbidv 3174 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π) β (βπ β π‘ (π βΎ π ) β MblFn β βπ β π‘ (π βΎ π ) β MblFn)) |
50 | 45, 49 | anbi12d 631 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π) β ((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β (π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn))) |
51 | | eqeq2 2748 |
. . . . . . . . . . . 12
β’ (π = π β (βͺ π‘ = π β βͺ π‘ = π)) |
52 | 51 | adantl 482 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π) β (βͺ π‘ = π β βͺ π‘ = π)) |
53 | 50, 52 | anbi12d 631 |
. . . . . . . . . 10
β’ ((π = π β§ π = π) β (((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β ((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π))) |
54 | | eleq1 2825 |
. . . . . . . . . . 11
β’ (π = π β (π β MblFn β π β MblFn)) |
55 | 54 | adantr 481 |
. . . . . . . . . 10
β’ ((π = π β§ π = π) β (π β MblFn β π β MblFn)) |
56 | 53, 55 | imbi12d 344 |
. . . . . . . . 9
β’ ((π = π β§ π = π) β ((((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β (((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β
MblFn))) |
57 | 56 | cbval2vw 2043 |
. . . . . . . 8
β’
(βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β
βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn)) |
58 | 42, 57 | bitrdi 286 |
. . . . . . 7
β’ (π = π‘ β (βπβπ(((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β
βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β
MblFn))) |
59 | | raleq 3309 |
. . . . . . . . . . 11
β’ (π = (π‘ βͺ {β}) β (βπ β π (π βΎ π ) β MblFn β βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn)) |
60 | 59 | anbi2d 629 |
. . . . . . . . . 10
β’ (π = (π‘ βͺ {β}) β ((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β (π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn))) |
61 | | unieq 4876 |
. . . . . . . . . . 11
β’ (π = (π‘ βͺ {β}) β βͺ π = βͺ
(π‘ βͺ {β})) |
62 | 61 | eqeq1d 2738 |
. . . . . . . . . 10
β’ (π = (π‘ βͺ {β}) β (βͺ π = π β βͺ (π‘ βͺ {β}) = π)) |
63 | 60, 62 | anbi12d 631 |
. . . . . . . . 9
β’ (π = (π‘ βͺ {β}) β (((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π))) |
64 | 63 | imbi1d 341 |
. . . . . . . 8
β’ (π = (π‘ βͺ {β}) β ((((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β π β MblFn))) |
65 | 64 | 2albidv 1926 |
. . . . . . 7
β’ (π = (π‘ βͺ {β}) β (βπβπ(((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β
βπβπ(((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β π β MblFn))) |
66 | | raleq 3309 |
. . . . . . . . . . 11
β’ (π = π β (βπ β π (π βΎ π ) β MblFn β βπ β π (π βΎ π ) β MblFn)) |
67 | 66 | anbi2d 629 |
. . . . . . . . . 10
β’ (π = π β ((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β (π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn))) |
68 | | unieq 4876 |
. . . . . . . . . . 11
β’ (π = π β βͺ π = βͺ
π) |
69 | 68 | eqeq1d 2738 |
. . . . . . . . . 10
β’ (π = π β (βͺ π = π β βͺ π = π)) |
70 | 67, 69 | anbi12d 631 |
. . . . . . . . 9
β’ (π = π β (((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β ((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π))) |
71 | 70 | imbi1d 341 |
. . . . . . . 8
β’ (π = π β ((((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β (((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β
MblFn))) |
72 | 71 | 2albidv 1926 |
. . . . . . 7
β’ (π = π β (βπβπ(((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β
βπβπ(((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β
MblFn))) |
73 | | frel 6673 |
. . . . . . . . . 10
β’ (π:πβΆβ β Rel π) |
74 | 73 | adantr 481 |
. . . . . . . . 9
β’ ((π:πβΆβ β§ β
= π) β Rel π) |
75 | | fdm 6677 |
. . . . . . . . . 10
β’ (π:πβΆβ β dom π = π) |
76 | | eqcom 2743 |
. . . . . . . . . . 11
β’ (β
= π β π = β
) |
77 | 76 | biimpi 215 |
. . . . . . . . . 10
β’ (β
= π β π = β
) |
78 | 75, 77 | sylan9eq 2796 |
. . . . . . . . 9
β’ ((π:πβΆβ β§ β
= π) β dom π = β
) |
79 | | reldm0 5883 |
. . . . . . . . . . 11
β’ (Rel
π β (π = β
β dom π = β
)) |
80 | 79 | biimpar 478 |
. . . . . . . . . 10
β’ ((Rel
π β§ dom π = β
) β π = β
) |
81 | | mbf0 24998 |
. . . . . . . . . 10
β’ β
β MblFn |
82 | 80, 81 | eqeltrdi 2845 |
. . . . . . . . 9
β’ ((Rel
π β§ dom π = β
) β π β MblFn) |
83 | 74, 78, 82 | syl2anc 584 |
. . . . . . . 8
β’ ((π:πβΆβ β§ β
= π) β π β MblFn) |
84 | 83 | gen2 1798 |
. . . . . . 7
β’
βπβπ((π:πβΆβ β§ β
= π) β π β MblFn) |
85 | | ref 14997 |
. . . . . . . . . . . . . . 15
β’
β:ββΆβ |
86 | | fco 6692 |
. . . . . . . . . . . . . . 15
β’
((β:ββΆβ β§ π:πβΆβ) β (β β π):πβΆβ) |
87 | 85, 86 | mpan 688 |
. . . . . . . . . . . . . 14
β’ (π:πβΆβ β (β β π):πβΆβ) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β (β β π):πβΆβ) |
89 | 88 | ad2antrl 726 |
. . . . . . . . . . . 12
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β (β β π):πβΆβ) |
90 | | recncf 24265 |
. . . . . . . . . . . . . . . . 17
β’ β
β (ββcnββ) |
91 | 90 | elexi 3464 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
92 | | vex 3449 |
. . . . . . . . . . . . . . . 16
β’ π β V |
93 | 91, 92 | coex 7867 |
. . . . . . . . . . . . . . 15
β’ (β
β π) β
V |
94 | 93 | resex 5985 |
. . . . . . . . . . . . . 14
β’ ((β
β π) βΎ βͺ π‘)
β V |
95 | | vuniex 7676 |
. . . . . . . . . . . . . 14
β’ βͺ π‘
β V |
96 | | eqcom 2743 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = βͺ
π‘ β βͺ π‘ =
π) |
97 | 96 | biimpi 215 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = βͺ
π‘ β βͺ π‘ =
π) |
98 | 97 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β βͺ π‘ = π) |
99 | 98 | biantrud 532 |
. . . . . . . . . . . . . . . . 17
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β ((π:πβΆβ β§
βπ β π‘ (π βΎ π ) β MblFn) β ((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π))) |
100 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . 19
β’ β =
β |
101 | | feq123 6658 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘
β§ β = β) β (π:πβΆβ β ((β β π) βΎ βͺ π‘):βͺ π‘βΆβ)) |
102 | 100, 101 | mp3an3 1450 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β (π:πβΆβ β ((β
β π) βΎ βͺ π‘):βͺ π‘βΆβ)) |
103 | | reseq1 5931 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = ((β β π) βΎ βͺ π‘)
β (π βΎ π ) = (((β β π) βΎ βͺ π‘)
βΎ π )) |
104 | 103 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = ((β β π) βΎ βͺ π‘)
β ((π βΎ π ) β MblFn β (((β
β π) βΎ βͺ π‘)
βΎ π ) β
MblFn)) |
105 | 104 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β ((π βΎ π ) β MblFn β (((β
β π) βΎ βͺ π‘)
βΎ π ) β
MblFn)) |
106 | 105 | ralbidv 3174 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β (βπ β
π‘ (π βΎ π ) β MblFn β βπ β π‘ (((β β π) βΎ βͺ π‘) βΎ π ) β MblFn)) |
107 | 102, 106 | anbi12d 631 |
. . . . . . . . . . . . . . . . 17
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β ((π:πβΆβ β§
βπ β π‘ (π βΎ π ) β MblFn) β (((β β
π) βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β
MblFn))) |
108 | 99, 107 | bitr3d 280 |
. . . . . . . . . . . . . . . 16
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β (((π:πβΆβ β§
βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β (((β β
π) βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β
MblFn))) |
109 | | eleq1 2825 |
. . . . . . . . . . . . . . . . 17
β’ (π = ((β β π) βΎ βͺ π‘)
β (π β MblFn
β ((β β π)
βΎ βͺ π‘) β MblFn)) |
110 | 109 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β (π β MblFn
β ((β β π)
βΎ βͺ π‘) β MblFn)) |
111 | 108, 110 | imbi12d 344 |
. . . . . . . . . . . . . . 15
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β ((((π:πβΆβ β§
βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β ((((β
β π) βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β ((β β π)
βΎ βͺ π‘) β MblFn))) |
112 | 111 | spc2gv 3559 |
. . . . . . . . . . . . . 14
β’
((((β β π) βΎ βͺ π‘) β V β§ βͺ π‘
β V) β (βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β ((((β
β π) βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β ((β β π)
βΎ βͺ π‘) β MblFn))) |
113 | 94, 95, 112 | mp2an 690 |
. . . . . . . . . . . . 13
β’
(βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β ((((β
β π) βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β ((β β π)
βΎ βͺ π‘) β MblFn)) |
114 | | ax-resscn 11108 |
. . . . . . . . . . . . . . . . . 18
β’ β
β β |
115 | | fss 6685 |
. . . . . . . . . . . . . . . . . 18
β’
((β:ββΆβ β§ β β β) β
β:ββΆβ) |
116 | 85, 114, 115 | mp2an 690 |
. . . . . . . . . . . . . . . . 17
β’
β:ββΆβ |
117 | | fco 6692 |
. . . . . . . . . . . . . . . . 17
β’
((β:ββΆβ β§ π:πβΆβ) β (β β π):πβΆβ) |
118 | 116, 117 | mpan 688 |
. . . . . . . . . . . . . . . 16
β’ (π:πβΆβ β (β β π):πβΆβ) |
119 | | ssun1 4132 |
. . . . . . . . . . . . . . . . . 18
β’ π‘ β (π‘ βͺ {β}) |
120 | 119 | unissi 4874 |
. . . . . . . . . . . . . . . . 17
β’ βͺ π‘
β βͺ (π‘ βͺ {β}) |
121 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (βͺ (π‘
βͺ {β}) = π β βͺ (π‘
βͺ {β}) = π) |
122 | 120, 121 | sseqtrid 3996 |
. . . . . . . . . . . . . . . 16
β’ (βͺ (π‘
βͺ {β}) = π β βͺ π‘
β π) |
123 | | fssres 6708 |
. . . . . . . . . . . . . . . 16
β’ (((β
β π):πβΆβ β§ βͺ π‘
β π) β ((β
β π) βΎ βͺ π‘):βͺ π‘βΆβ) |
124 | 118, 122,
123 | syl2an 596 |
. . . . . . . . . . . . . . 15
β’ ((π:πβΆβ β§ βͺ (π‘
βͺ {β}) = π) β ((β β π) βΎ βͺ π‘):βͺ π‘βΆβ) |
125 | 124 | adantlr 713 |
. . . . . . . . . . . . . 14
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β ((β β π) βΎ βͺ π‘):βͺ π‘βΆβ) |
126 | | elssuni 4898 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π‘ β π β βͺ π‘) |
127 | 126 | resabs1d 5968 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π‘ β (((β β π) βΎ βͺ π‘) βΎ π) = ((β β π) βΎ π)) |
128 | | resco 6202 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β
β π) βΎ π) = (β β (π βΎ π)) |
129 | 127, 128 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π‘ β (((β β π) βΎ βͺ π‘) βΎ π) = (β β (π βΎ π))) |
130 | 129 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ π β π‘) β (((β β π) βΎ βͺ π‘) βΎ π) = (β β (π βΎ π))) |
131 | | elun1 4136 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π‘ β π β (π‘ βͺ {β})) |
132 | | reseq2 5932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (π βΎ π ) = (π βΎ π)) |
133 | 132 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β ((π βΎ π ) β MblFn β (π βΎ π) β MblFn)) |
134 | 133 | rspccva 3580 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((βπ β
(π‘ βͺ {β})(π βΎ π ) β MblFn β§ π β (π‘ βͺ {β})) β (π βΎ π) β MblFn) |
135 | 131, 134 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((βπ β
(π‘ βͺ {β})(π βΎ π ) β MblFn β§ π β π‘) β (π βΎ π) β MblFn) |
136 | 135 | adantll 712 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ π β π‘) β (π βΎ π) β MblFn) |
137 | | fresin 6711 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:πβΆβ β (π βΎ π):(π β© π)βΆβ) |
138 | | ismbfcn 24993 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π βΎ π):(π β© π)βΆβ β ((π βΎ π) β MblFn β ((β β (π βΎ π)) β MblFn β§ (β β (π βΎ π)) β MblFn))) |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:πβΆβ β ((π βΎ π) β MblFn β ((β β (π βΎ π)) β MblFn β§ (β β (π βΎ π)) β MblFn))) |
140 | 139 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π:πβΆβ β ((π βΎ π) β MblFn β ((β β (π βΎ π)) β MblFn β§ (β β (π βΎ π)) β MblFn))) |
141 | 140 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ π β π‘) β ((π βΎ π) β MblFn β ((β β (π βΎ π)) β MblFn β§ (β β (π βΎ π)) β MblFn))) |
142 | 136, 141 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ π β π‘) β ((β β (π βΎ π)) β MblFn β§ (β β (π βΎ π)) β MblFn)) |
143 | 142 | simpld 495 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ π β π‘) β (β β (π βΎ π)) β MblFn) |
144 | 130, 143 | eqeltrd 2837 |
. . . . . . . . . . . . . . . . 17
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ π β π‘) β (((β β π) βΎ βͺ π‘) βΎ π) β MblFn) |
145 | 144 | ralrimiva 3143 |
. . . . . . . . . . . . . . . 16
β’ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β βπ β π‘ (((β β π) βΎ βͺ π‘) βΎ π) β MblFn) |
146 | | reseq2 5932 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((β β π) βΎ βͺ π‘) βΎ π) = (((β β π) βΎ βͺ π‘) βΎ π )) |
147 | 146 | eleq1d 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((((β β π) βΎ βͺ π‘) βΎ π) β MblFn β (((β β π) βΎ βͺ π‘)
βΎ π ) β
MblFn)) |
148 | 147 | cbvralvw 3225 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
π‘ (((β β π) βΎ βͺ π‘)
βΎ π) β MblFn
β βπ β
π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β
MblFn) |
149 | 145, 148 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β βπ β π‘ (((β β π) βΎ βͺ π‘) βΎ π ) β MblFn) |
150 | 149 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β βπ β π‘ (((β β π) βΎ βͺ π‘) βΎ π ) β MblFn) |
151 | | pm2.27 42 |
. . . . . . . . . . . . . 14
β’
((((β β π) βΎ βͺ π‘):βͺ
π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β (((((β β π) βΎ βͺ π‘):βͺ
π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β ((β β π)
βΎ βͺ π‘) β MblFn) β ((β β π) βΎ βͺ π‘)
β MblFn)) |
152 | 125, 150,
151 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β (((((β β
π) βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β ((β β π)
βΎ βͺ π‘) β MblFn) β ((β β π) βΎ βͺ π‘)
β MblFn)) |
153 | 113, 152 | mpan9 507 |
. . . . . . . . . . . 12
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β ((β β π) βΎ βͺ π‘)
β MblFn) |
154 | | vsnid 4623 |
. . . . . . . . . . . . . . 15
β’ β β {β} |
155 | | elun2 4137 |
. . . . . . . . . . . . . . 15
β’ (β β {β} β β β (π‘ βͺ {β})) |
156 | | reseq2 5932 |
. . . . . . . . . . . . . . . . 17
β’ (π = β β (π βΎ π ) = (π βΎ β)) |
157 | 156 | eleq1d 2822 |
. . . . . . . . . . . . . . . 16
β’ (π = β β ((π βΎ π ) β MblFn β (π βΎ β) β MblFn)) |
158 | 157 | rspcv 3577 |
. . . . . . . . . . . . . . 15
β’ (β β (π‘ βͺ {β}) β (βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn β (π βΎ β) β MblFn)) |
159 | 154, 155,
158 | mp2b 10 |
. . . . . . . . . . . . . 14
β’
(βπ β
(π‘ βͺ {β})(π βΎ π ) β MblFn β (π βΎ β) β MblFn) |
160 | | resco 6202 |
. . . . . . . . . . . . . . 15
β’ ((β
β π) βΎ β) = (β β (π βΎ β)) |
161 | | fresin 6711 |
. . . . . . . . . . . . . . . . 17
β’ (π:πβΆβ β (π βΎ β):(π β© β)βΆβ) |
162 | | ismbfcn 24993 |
. . . . . . . . . . . . . . . . 17
β’ ((π βΎ β):(π β© β)βΆβ β ((π βΎ β) β MblFn β ((β β (π βΎ β)) β MblFn β§ (β β (π βΎ β)) β MblFn))) |
163 | 161, 162 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π:πβΆβ β ((π βΎ β) β MblFn β ((β β (π βΎ β)) β MblFn β§ (β β (π βΎ β)) β MblFn))) |
164 | 163 | simprbda 499 |
. . . . . . . . . . . . . . 15
β’ ((π:πβΆβ β§ (π βΎ β) β MblFn) β (β β (π βΎ β)) β MblFn) |
165 | 160, 164 | eqeltrid 2841 |
. . . . . . . . . . . . . 14
β’ ((π:πβΆβ β§ (π βΎ β) β MblFn) β ((β β π) βΎ β) β MblFn) |
166 | 159, 165 | sylan2 593 |
. . . . . . . . . . . . 13
β’ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β ((β β π) βΎ β) β MblFn) |
167 | 166 | ad2antrl 726 |
. . . . . . . . . . . 12
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β ((β β π) βΎ β) β MblFn) |
168 | | uniun 4891 |
. . . . . . . . . . . . . . 15
β’ βͺ (π‘
βͺ {β}) = (βͺ π‘
βͺ βͺ {β}) |
169 | | unisnv 4888 |
. . . . . . . . . . . . . . . 16
β’ βͺ {β} =
β |
170 | 169 | uneq2i 4120 |
. . . . . . . . . . . . . . 15
β’ (βͺ π‘
βͺ βͺ {β}) = (βͺ π‘ βͺ β) |
171 | 168, 170 | eqtri 2764 |
. . . . . . . . . . . . . 14
β’ βͺ (π‘
βͺ {β}) = (βͺ π‘
βͺ β) |
172 | 171, 121 | eqtr3id 2790 |
. . . . . . . . . . . . 13
β’ (βͺ (π‘
βͺ {β}) = π β (βͺ π‘
βͺ β) = π) |
173 | 172 | ad2antll 727 |
. . . . . . . . . . . 12
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β (βͺ π‘
βͺ β) = π) |
174 | 89, 153, 167, 173 | mbfres2 25009 |
. . . . . . . . . . 11
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β (β β π) β MblFn) |
175 | | imf 14998 |
. . . . . . . . . . . . . . 15
β’
β:ββΆβ |
176 | | fco 6692 |
. . . . . . . . . . . . . . 15
β’
((β:ββΆβ β§ π:πβΆβ) β (β β
π):πβΆβ) |
177 | 175, 176 | mpan 688 |
. . . . . . . . . . . . . 14
β’ (π:πβΆβ β (β β π):πβΆβ) |
178 | 177 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β (β β π):πβΆβ) |
179 | 178 | ad2antrl 726 |
. . . . . . . . . . . 12
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β (β β π):πβΆβ) |
180 | | imcncf 24266 |
. . . . . . . . . . . . . . . . 17
β’ β
β (ββcnββ) |
181 | 180 | elexi 3464 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
182 | 181, 92 | coex 7867 |
. . . . . . . . . . . . . . 15
β’ (β
β π) β
V |
183 | 182 | resex 5985 |
. . . . . . . . . . . . . 14
β’ ((β
β π) βΎ βͺ π‘)
β V |
184 | 97 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β βͺ π‘ = π) |
185 | 184 | biantrud 532 |
. . . . . . . . . . . . . . . . 17
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β ((π:πβΆβ β§
βπ β π‘ (π βΎ π ) β MblFn) β ((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π))) |
186 | | feq123 6658 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘
β§ β = β) β (π:πβΆβ β ((β β
π) βΎ βͺ π‘):βͺ π‘βΆβ)) |
187 | 100, 186 | mp3an3 1450 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β (π:πβΆβ β ((β
β π) βΎ βͺ π‘):βͺ π‘βΆβ)) |
188 | | reseq1 5931 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = ((β β π) βΎ βͺ π‘)
β (π βΎ π ) = (((β β π) βΎ βͺ π‘)
βΎ π )) |
189 | 188 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = ((β β π) βΎ βͺ π‘)
β ((π βΎ π ) β MblFn β (((β
β π) βΎ βͺ π‘)
βΎ π ) β
MblFn)) |
190 | 189 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β ((π βΎ π ) β MblFn β (((β
β π) βΎ βͺ π‘)
βΎ π ) β
MblFn)) |
191 | 190 | ralbidv 3174 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β (βπ β
π‘ (π βΎ π ) β MblFn β βπ β π‘ (((β β π) βΎ βͺ π‘) βΎ π ) β MblFn)) |
192 | 187, 191 | anbi12d 631 |
. . . . . . . . . . . . . . . . 17
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β ((π:πβΆβ β§
βπ β π‘ (π βΎ π ) β MblFn) β (((β β
π) βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β
MblFn))) |
193 | 185, 192 | bitr3d 280 |
. . . . . . . . . . . . . . . 16
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β (((π:πβΆβ β§
βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β (((β
β π) βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β
MblFn))) |
194 | | eleq1 2825 |
. . . . . . . . . . . . . . . . 17
β’ (π = ((β β π) βΎ βͺ π‘)
β (π β MblFn
β ((β β π)
βΎ βͺ π‘) β MblFn)) |
195 | 194 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β (π β MblFn
β ((β β π)
βΎ βͺ π‘) β MblFn)) |
196 | 193, 195 | imbi12d 344 |
. . . . . . . . . . . . . . 15
β’ ((π = ((β β π) βΎ βͺ π‘)
β§ π = βͺ π‘)
β ((((π:πβΆβ β§
βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β
((((β β π)
βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β ((β β π)
βΎ βͺ π‘) β MblFn))) |
197 | 196 | spc2gv 3559 |
. . . . . . . . . . . . . 14
β’
((((β β π) βΎ βͺ π‘) β V β§ βͺ π‘
β V) β (βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β
((((β β π)
βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β ((β β π)
βΎ βͺ π‘) β MblFn))) |
198 | 183, 95, 197 | mp2an 690 |
. . . . . . . . . . . . 13
β’
(βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β
((((β β π)
βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β ((β β π)
βΎ βͺ π‘) β MblFn)) |
199 | | fss 6685 |
. . . . . . . . . . . . . . . . . 18
β’
((β:ββΆβ β§ β β β) β
β:ββΆβ) |
200 | 175, 114,
199 | mp2an 690 |
. . . . . . . . . . . . . . . . 17
β’
β:ββΆβ |
201 | | fco 6692 |
. . . . . . . . . . . . . . . . 17
β’
((β:ββΆβ β§ π:πβΆβ) β (β β
π):πβΆβ) |
202 | 200, 201 | mpan 688 |
. . . . . . . . . . . . . . . 16
β’ (π:πβΆβ β (β β π):πβΆβ) |
203 | | fssres 6708 |
. . . . . . . . . . . . . . . 16
β’
(((β β π):πβΆβ β§ βͺ π‘
β π) β ((β
β π) βΎ βͺ π‘):βͺ π‘βΆβ) |
204 | 202, 122,
203 | syl2an 596 |
. . . . . . . . . . . . . . 15
β’ ((π:πβΆβ β§ βͺ (π‘
βͺ {β}) = π) β ((β β π) βΎ βͺ π‘):βͺ π‘βΆβ) |
205 | 204 | adantlr 713 |
. . . . . . . . . . . . . 14
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β ((β β π) βΎ βͺ π‘):βͺ π‘βΆβ) |
206 | 126 | resabs1d 5968 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π‘ β (((β β π) βΎ βͺ π‘) βΎ π) = ((β β π) βΎ π)) |
207 | | resco 6202 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β
β π) βΎ π) = (β β (π βΎ π)) |
208 | 206, 207 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π‘ β (((β β π) βΎ βͺ π‘) βΎ π) = (β β (π βΎ π))) |
209 | 208 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ π β π‘) β (((β β π) βΎ βͺ π‘)
βΎ π) = (β
β (π βΎ π))) |
210 | 142 | simprd 496 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ π β π‘) β (β β (π βΎ π)) β MblFn) |
211 | 209, 210 | eqeltrd 2837 |
. . . . . . . . . . . . . . . . 17
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ π β π‘) β (((β β π) βΎ βͺ π‘)
βΎ π) β
MblFn) |
212 | 211 | ralrimiva 3143 |
. . . . . . . . . . . . . . . 16
β’ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β βπ β π‘ (((β β π) βΎ βͺ π‘) βΎ π) β MblFn) |
213 | | reseq2 5932 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((β β π) βΎ βͺ π‘) βΎ π) = (((β β π) βΎ βͺ π‘) βΎ π )) |
214 | 213 | eleq1d 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((((β β π) βΎ βͺ π‘)
βΎ π) β MblFn
β (((β β π) βΎ βͺ π‘) βΎ π ) β MblFn)) |
215 | 214 | cbvralvw 3225 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
π‘ (((β β π) βΎ βͺ π‘)
βΎ π) β MblFn
β βπ β
π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β
MblFn) |
216 | 212, 215 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β βπ β π‘ (((β β π) βΎ βͺ π‘) βΎ π ) β MblFn) |
217 | 216 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β βπ β π‘ (((β β π) βΎ βͺ π‘) βΎ π ) β MblFn) |
218 | | pm2.27 42 |
. . . . . . . . . . . . . 14
β’
((((β β π) βΎ βͺ π‘):βͺ
π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β (((((β β π) βΎ βͺ π‘):βͺ
π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β ((β β π)
βΎ βͺ π‘) β MblFn) β ((β β
π) βΎ βͺ π‘)
β MblFn)) |
219 | 205, 217,
218 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β (((((β β
π) βΎ βͺ π‘):βͺ π‘βΆβ β§
βπ β π‘ (((β β π) βΎ βͺ π‘)
βΎ π ) β MblFn)
β ((β β π)
βΎ βͺ π‘) β MblFn) β ((β β
π) βΎ βͺ π‘)
β MblFn)) |
220 | 198, 219 | mpan9 507 |
. . . . . . . . . . . 12
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β ((β β
π) βΎ βͺ π‘)
β MblFn) |
221 | | resco 6202 |
. . . . . . . . . . . . . . 15
β’ ((β
β π) βΎ β) = (β β (π βΎ β)) |
222 | 163 | simplbda 500 |
. . . . . . . . . . . . . . 15
β’ ((π:πβΆβ β§ (π βΎ β) β MblFn) β (β β (π βΎ β)) β MblFn) |
223 | 221, 222 | eqeltrid 2841 |
. . . . . . . . . . . . . 14
β’ ((π:πβΆβ β§ (π βΎ β) β MblFn) β ((β β π) βΎ β) β MblFn) |
224 | 159, 223 | sylan2 593 |
. . . . . . . . . . . . 13
β’ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β ((β β
π) βΎ β) β MblFn) |
225 | 224 | ad2antrl 726 |
. . . . . . . . . . . 12
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β ((β β
π) βΎ β) β MblFn) |
226 | 179, 220,
225, 173 | mbfres2 25009 |
. . . . . . . . . . 11
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β (β β π) β MblFn) |
227 | | ismbfcn 24993 |
. . . . . . . . . . . . 13
β’ (π:πβΆβ β (π β MblFn β ((β β π) β MblFn β§ (β
β π) β
MblFn))) |
228 | 227 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β (π β MblFn β ((β β π) β MblFn β§ (β
β π) β
MblFn))) |
229 | 228 | ad2antrl 726 |
. . . . . . . . . . 11
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β (π β MblFn β ((β β π) β MblFn β§ (β
β π) β
MblFn))) |
230 | 174, 226,
229 | mpbir2and 711 |
. . . . . . . . . 10
β’
((βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β§ ((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π)) β π β MblFn) |
231 | 230 | ex 413 |
. . . . . . . . 9
β’
(βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β (((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β π β MblFn)) |
232 | 231 | alrimivv 1931 |
. . . . . . . 8
β’
(βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β
βπβπ(((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β π β MblFn)) |
233 | 232 | a1i 11 |
. . . . . . 7
β’ (π‘ β Fin β
(βπβπ(((π:πβΆβ β§ βπ β π‘ (π βΎ π ) β MblFn) β§ βͺ π‘ =
π) β π β MblFn) β
βπβπ(((π:πβΆβ β§ βπ β (π‘ βͺ {β})(π βΎ π ) β MblFn) β§ βͺ (π‘
βͺ {β}) = π) β π β MblFn))) |
234 | 35, 58, 65, 72, 84, 233 | findcard2 9108 |
. . . . . 6
β’ (π β Fin β βπβπ(((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn)) |
235 | | 2sp 2179 |
. . . . . 6
β’
(βπβπ(((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn) β (((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn)) |
236 | 4, 234, 235 | 3syl 18 |
. . . . 5
β’ (π β (((π:πβΆβ β§ βπ β π (π βΎ π ) β MblFn) β§ βͺ π =
π) β π β MblFn)) |
237 | 16, 25, 236 | vtocl2g 3531 |
. . . 4
β’ ((π΄ β V β§ πΉ β V) β (π β (((πΉ:π΄βΆβ β§ βπ β π (πΉ βΎ π ) β MblFn) β§ βͺ π =
π΄) β πΉ β MblFn))) |
238 | 10, 237 | mpcom 38 |
. . 3
β’ (π β (((πΉ:π΄βΆβ β§ βπ β π (πΉ βΎ π ) β MblFn) β§ βͺ π =
π΄) β πΉ β MblFn)) |
239 | 3, 238 | mpan2d 692 |
. 2
β’ (π β ((πΉ:π΄βΆβ β§ βπ β π (πΉ βΎ π ) β MblFn) β πΉ β MblFn)) |
240 | 1, 2, 239 | mp2and 697 |
1
β’ (π β πΉ β MblFn) |