Step | Hyp | Ref
| Expression |
1 | | unieq 4918 |
. . . . 5
β’ (π = β
β βͺ π =
βͺ β
) |
2 | | uni0 4938 |
. . . . 5
β’ βͺ β
= β
|
3 | 1, 2 | eqtrdi 2788 |
. . . 4
β’ (π = β
β βͺ π =
β
) |
4 | 3 | adantl 482 |
. . 3
β’ ((π β§ π = β
) β βͺ π =
β
) |
5 | | caragenunicl.o |
. . . . 5
β’ (π β π β OutMeas) |
6 | | caragenunicl.s |
. . . . 5
β’ π = (CaraGenβπ) |
7 | 5, 6 | caragen0 45208 |
. . . 4
β’ (π β β
β π) |
8 | 7 | adantr 481 |
. . 3
β’ ((π β§ π = β
) β β
β π) |
9 | 4, 8 | eqeltrd 2833 |
. 2
β’ ((π β§ π = β
) β βͺ π
β π) |
10 | | simpl 483 |
. . 3
β’ ((π β§ Β¬ π = β
) β π) |
11 | | neqne 2948 |
. . . 4
β’ (Β¬
π = β
β π β β
) |
12 | 11 | adantl 482 |
. . 3
β’ ((π β§ Β¬ π = β
) β π β β
) |
13 | | simpr 485 |
. . . . . 6
β’ ((π β§ π β β
) β π β β
) |
14 | | caragenunicl.ctb |
. . . . . . . . 9
β’ (π β π βΌ Ο) |
15 | | reldom 8941 |
. . . . . . . . . 10
β’ Rel
βΌ |
16 | | brrelex1 5727 |
. . . . . . . . . 10
β’ ((Rel
βΌ β§ π βΌ
Ο) β π β
V) |
17 | 15, 16 | mpan 688 |
. . . . . . . . 9
β’ (π βΌ Ο β π β V) |
18 | 14, 17 | syl 17 |
. . . . . . . 8
β’ (π β π β V) |
19 | 18 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β
) β π β V) |
20 | | 0sdomg 9100 |
. . . . . . 7
β’ (π β V β (β
βΊ π β π β β
)) |
21 | 19, 20 | syl 17 |
. . . . . 6
β’ ((π β§ π β β
) β (β
βΊ π β π β β
)) |
22 | 13, 21 | mpbird 256 |
. . . . 5
β’ ((π β§ π β β
) β β
βΊ π) |
23 | | nnenom 13941 |
. . . . . . . . 9
β’ β
β Ο |
24 | 23 | ensymi 8996 |
. . . . . . . 8
β’ Ο
β β |
25 | 24 | a1i 11 |
. . . . . . 7
β’ (π β Ο β
β) |
26 | | domentr 9005 |
. . . . . . 7
β’ ((π βΌ Ο β§ Ο
β β) β π
βΌ β) |
27 | 14, 25, 26 | syl2anc 584 |
. . . . . 6
β’ (π β π βΌ β) |
28 | 27 | adantr 481 |
. . . . 5
β’ ((π β§ π β β
) β π βΌ β) |
29 | | fodomr 9124 |
. . . . 5
β’ ((β
βΊ π β§ π βΌ β) β
βπ π:ββontoβπ) |
30 | 22, 28, 29 | syl2anc 584 |
. . . 4
β’ ((π β§ π β β
) β βπ π:ββontoβπ) |
31 | | founiiun 43860 |
. . . . . . . . 9
β’ (π:ββontoβπ β βͺ π = βͺ π β β (πβπ)) |
32 | 31 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π:ββontoβπ) β βͺ π = βͺ π β β (πβπ)) |
33 | 5 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π:ββontoβπ) β π β OutMeas) |
34 | | 1zzd 12589 |
. . . . . . . . 9
β’ ((π β§ π:ββontoβπ) β 1 β β€) |
35 | | nnuz 12861 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
36 | | fof 6802 |
. . . . . . . . . . 11
β’ (π:ββontoβπ β π:ββΆπ) |
37 | 36 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π:ββontoβπ) β π:ββΆπ) |
38 | | caragenunicl.y |
. . . . . . . . . . 11
β’ (π β π β π) |
39 | 38 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π:ββontoβπ) β π β π) |
40 | 37, 39 | fssd 6732 |
. . . . . . . . 9
β’ ((π β§ π:ββontoβπ) β π:ββΆπ) |
41 | 33, 6, 34, 35, 40 | carageniuncl 45225 |
. . . . . . . 8
β’ ((π β§ π:ββontoβπ) β βͺ
π β β (πβπ) β π) |
42 | 32, 41 | eqeltrd 2833 |
. . . . . . 7
β’ ((π β§ π:ββontoβπ) β βͺ π β π) |
43 | 42 | ex 413 |
. . . . . 6
β’ (π β (π:ββontoβπ β βͺ π β π)) |
44 | 43 | adantr 481 |
. . . . 5
β’ ((π β§ π β β
) β (π:ββontoβπ β βͺ π β π)) |
45 | 44 | exlimdv 1936 |
. . . 4
β’ ((π β§ π β β
) β (βπ π:ββontoβπ β βͺ π β π)) |
46 | 30, 45 | mpd 15 |
. . 3
β’ ((π β§ π β β
) β βͺ π
β π) |
47 | 10, 12, 46 | syl2anc 584 |
. 2
β’ ((π β§ Β¬ π = β
) β βͺ π
β π) |
48 | 9, 47 | pm2.61dan 811 |
1
β’ (π β βͺ π
β π) |