Step | Hyp | Ref
| Expression |
1 | | unieq 4881 |
. . . . 5
β’ (π = β
β βͺ π =
βͺ β
) |
2 | | uni0 4901 |
. . . . 5
β’ βͺ β
= β
|
3 | 1, 2 | eqtrdi 2793 |
. . . 4
β’ (π = β
β βͺ π =
β
) |
4 | 3 | adantl 483 |
. . 3
β’ ((π β§ π = β
) β βͺ π =
β
) |
5 | | caragenunicl.o |
. . . . 5
β’ (π β π β OutMeas) |
6 | | caragenunicl.s |
. . . . 5
β’ π = (CaraGenβπ) |
7 | 5, 6 | caragen0 44821 |
. . . 4
β’ (π β β
β π) |
8 | 7 | adantr 482 |
. . 3
β’ ((π β§ π = β
) β β
β π) |
9 | 4, 8 | eqeltrd 2838 |
. 2
β’ ((π β§ π = β
) β βͺ π
β π) |
10 | | simpl 484 |
. . 3
β’ ((π β§ Β¬ π = β
) β π) |
11 | | neqne 2952 |
. . . 4
β’ (Β¬
π = β
β π β β
) |
12 | 11 | adantl 483 |
. . 3
β’ ((π β§ Β¬ π = β
) β π β β
) |
13 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β β
) β π β β
) |
14 | | caragenunicl.ctb |
. . . . . . . . 9
β’ (π β π βΌ Ο) |
15 | | reldom 8896 |
. . . . . . . . . 10
β’ Rel
βΌ |
16 | | brrelex1 5690 |
. . . . . . . . . 10
β’ ((Rel
βΌ β§ π βΌ
Ο) β π β
V) |
17 | 15, 16 | mpan 689 |
. . . . . . . . 9
β’ (π βΌ Ο β π β V) |
18 | 14, 17 | syl 17 |
. . . . . . . 8
β’ (π β π β V) |
19 | 18 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β
) β π β V) |
20 | | 0sdomg 9055 |
. . . . . . 7
β’ (π β V β (β
βΊ π β π β β
)) |
21 | 19, 20 | syl 17 |
. . . . . 6
β’ ((π β§ π β β
) β (β
βΊ π β π β β
)) |
22 | 13, 21 | mpbird 257 |
. . . . 5
β’ ((π β§ π β β
) β β
βΊ π) |
23 | | nnenom 13892 |
. . . . . . . . 9
β’ β
β Ο |
24 | 23 | ensymi 8951 |
. . . . . . . 8
β’ Ο
β β |
25 | 24 | a1i 11 |
. . . . . . 7
β’ (π β Ο β
β) |
26 | | domentr 8960 |
. . . . . . 7
β’ ((π βΌ Ο β§ Ο
β β) β π
βΌ β) |
27 | 14, 25, 26 | syl2anc 585 |
. . . . . 6
β’ (π β π βΌ β) |
28 | 27 | adantr 482 |
. . . . 5
β’ ((π β§ π β β
) β π βΌ β) |
29 | | fodomr 9079 |
. . . . 5
β’ ((β
βΊ π β§ π βΌ β) β
βπ π:ββontoβπ) |
30 | 22, 28, 29 | syl2anc 585 |
. . . 4
β’ ((π β§ π β β
) β βπ π:ββontoβπ) |
31 | | founiiun 43470 |
. . . . . . . . 9
β’ (π:ββontoβπ β βͺ π = βͺ π β β (πβπ)) |
32 | 31 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π:ββontoβπ) β βͺ π = βͺ π β β (πβπ)) |
33 | 5 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π:ββontoβπ) β π β OutMeas) |
34 | | 1zzd 12541 |
. . . . . . . . 9
β’ ((π β§ π:ββontoβπ) β 1 β β€) |
35 | | nnuz 12813 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
36 | | fof 6761 |
. . . . . . . . . . 11
β’ (π:ββontoβπ β π:ββΆπ) |
37 | 36 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π:ββontoβπ) β π:ββΆπ) |
38 | | caragenunicl.y |
. . . . . . . . . . 11
β’ (π β π β π) |
39 | 38 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π:ββontoβπ) β π β π) |
40 | 37, 39 | fssd 6691 |
. . . . . . . . 9
β’ ((π β§ π:ββontoβπ) β π:ββΆπ) |
41 | 33, 6, 34, 35, 40 | carageniuncl 44838 |
. . . . . . . 8
β’ ((π β§ π:ββontoβπ) β βͺ
π β β (πβπ) β π) |
42 | 32, 41 | eqeltrd 2838 |
. . . . . . 7
β’ ((π β§ π:ββontoβπ) β βͺ π β π) |
43 | 42 | ex 414 |
. . . . . 6
β’ (π β (π:ββontoβπ β βͺ π β π)) |
44 | 43 | adantr 482 |
. . . . 5
β’ ((π β§ π β β
) β (π:ββontoβπ β βͺ π β π)) |
45 | 44 | exlimdv 1937 |
. . . 4
β’ ((π β§ π β β
) β (βπ π:ββontoβπ β βͺ π β π)) |
46 | 30, 45 | mpd 15 |
. . 3
β’ ((π β§ π β β
) β βͺ π
β π) |
47 | 10, 12, 46 | syl2anc 585 |
. 2
β’ ((π β§ Β¬ π = β
) β βͺ π
β π) |
48 | 9, 47 | pm2.61dan 812 |
1
β’ (π β βͺ π
β π) |