Step | Hyp | Ref
| Expression |
1 | | mreexexlem2d.1 |
. . . 4
β’ (π β π΄ β (Mooreβπ)) |
2 | 1 | adantr 482 |
. . 3
β’ ((π β§ πΉ = β
) β π΄ β (Mooreβπ)) |
3 | | mreexexlem2d.2 |
. . 3
β’ π = (mrClsβπ΄) |
4 | | mreexexlem2d.3 |
. . 3
β’ πΌ = (mrIndβπ΄) |
5 | | mreexexlem2d.4 |
. . . 4
β’ (π β βπ β π« πβπ¦ β π βπ§ β ((πβ(π βͺ {π¦})) β (πβπ ))π¦ β (πβ(π βͺ {π§}))) |
6 | 5 | adantr 482 |
. . 3
β’ ((π β§ πΉ = β
) β βπ β π« πβπ¦ β π βπ§ β ((πβ(π βͺ {π¦})) β (πβπ ))π¦ β (πβ(π βͺ {π§}))) |
7 | | mreexexlem2d.5 |
. . . 4
β’ (π β πΉ β (π β π»)) |
8 | 7 | adantr 482 |
. . 3
β’ ((π β§ πΉ = β
) β πΉ β (π β π»)) |
9 | | mreexexlem2d.6 |
. . . 4
β’ (π β πΊ β (π β π»)) |
10 | 9 | adantr 482 |
. . 3
β’ ((π β§ πΉ = β
) β πΊ β (π β π»)) |
11 | | mreexexlem2d.7 |
. . . 4
β’ (π β πΉ β (πβ(πΊ βͺ π»))) |
12 | 11 | adantr 482 |
. . 3
β’ ((π β§ πΉ = β
) β πΉ β (πβ(πΊ βͺ π»))) |
13 | | mreexexlem2d.8 |
. . . 4
β’ (π β (πΉ βͺ π») β πΌ) |
14 | 13 | adantr 482 |
. . 3
β’ ((π β§ πΉ = β
) β (πΉ βͺ π») β πΌ) |
15 | | animorrl 980 |
. . 3
β’ ((π β§ πΉ = β
) β (πΉ = β
β¨ πΊ = β
)) |
16 | 2, 3, 4, 6, 8, 10,
12, 14, 15 | mreexexlem3d 17531 |
. 2
β’ ((π β§ πΉ = β
) β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |
17 | | n0 4307 |
. . . . 5
β’ (πΉ β β
β
βπ π β πΉ) |
18 | 17 | biimpi 215 |
. . . 4
β’ (πΉ β β
β
βπ π β πΉ) |
19 | 18 | adantl 483 |
. . 3
β’ ((π β§ πΉ β β
) β βπ π β πΉ) |
20 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΉ) β π΄ β (Mooreβπ)) |
21 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΉ) β βπ β π« πβπ¦ β π βπ§ β ((πβ(π βͺ {π¦})) β (πβπ ))π¦ β (πβ(π βͺ {π§}))) |
22 | 7 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΉ) β πΉ β (π β π»)) |
23 | 9 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΉ) β πΊ β (π β π»)) |
24 | 11 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΉ) β πΉ β (πβ(πΊ βͺ π»))) |
25 | 13 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΉ) β (πΉ βͺ π») β πΌ) |
26 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β πΉ) β π β πΉ) |
27 | 20, 3, 4, 21, 22, 23, 24, 25, 26 | mreexexlem2d 17530 |
. . . . 5
β’ ((π β§ π β πΉ) β βπ β πΊ (Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) |
28 | | 3anass 1096 |
. . . . . 6
β’ ((π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ) β (π β πΊ β§ (Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ))) |
29 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β π΄ β (Mooreβπ)) |
30 | 29 | elfvexd 6882 |
. . . . . . . 8
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β π β V) |
31 | | simpr2 1196 |
. . . . . . . . . . 11
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β Β¬ π β (πΉ β {π})) |
32 | | difsnb 4767 |
. . . . . . . . . . 11
β’ (Β¬
π β (πΉ β {π}) β ((πΉ β {π}) β {π}) = (πΉ β {π})) |
33 | 31, 32 | sylib 217 |
. . . . . . . . . 10
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β ((πΉ β {π}) β {π}) = (πΉ β {π})) |
34 | 7 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β πΉ β (π β π»)) |
35 | 34 | ssdifssd 4103 |
. . . . . . . . . . 11
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β (πΉ β {π}) β (π β π»)) |
36 | 35 | ssdifd 4101 |
. . . . . . . . . 10
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β ((πΉ β {π}) β {π}) β ((π β π») β {π})) |
37 | 33, 36 | eqsstrrd 3984 |
. . . . . . . . 9
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β (πΉ β {π}) β ((π β π») β {π})) |
38 | | difun1 4250 |
. . . . . . . . 9
β’ (π β (π» βͺ {π})) = ((π β π») β {π}) |
39 | 37, 38 | sseqtrrdi 3996 |
. . . . . . . 8
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β (πΉ β {π}) β (π β (π» βͺ {π}))) |
40 | 9 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β πΊ β (π β π»)) |
41 | 40 | ssdifd 4101 |
. . . . . . . . 9
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β (πΊ β {π}) β ((π β π») β {π})) |
42 | 41, 38 | sseqtrrdi 3996 |
. . . . . . . 8
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β (πΊ β {π}) β (π β (π» βͺ {π}))) |
43 | 11 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β πΉ β (πβ(πΊ βͺ π»))) |
44 | | simpr1 1195 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β π β πΊ) |
45 | | uncom 4114 |
. . . . . . . . . . . . . 14
β’ (π» βͺ {π}) = ({π} βͺ π») |
46 | 45 | uneq2i 4121 |
. . . . . . . . . . . . 13
β’ ((πΊ β {π}) βͺ (π» βͺ {π})) = ((πΊ β {π}) βͺ ({π} βͺ π»)) |
47 | | unass 4127 |
. . . . . . . . . . . . . 14
β’ (((πΊ β {π}) βͺ {π}) βͺ π») = ((πΊ β {π}) βͺ ({π} βͺ π»)) |
48 | | difsnid 4771 |
. . . . . . . . . . . . . . 15
β’ (π β πΊ β ((πΊ β {π}) βͺ {π}) = πΊ) |
49 | 48 | uneq1d 4123 |
. . . . . . . . . . . . . 14
β’ (π β πΊ β (((πΊ β {π}) βͺ {π}) βͺ π») = (πΊ βͺ π»)) |
50 | 47, 49 | eqtr3id 2787 |
. . . . . . . . . . . . 13
β’ (π β πΊ β ((πΊ β {π}) βͺ ({π} βͺ π»)) = (πΊ βͺ π»)) |
51 | 46, 50 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ (π β πΊ β ((πΊ β {π}) βͺ (π» βͺ {π})) = (πΊ βͺ π»)) |
52 | 44, 51 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β ((πΊ β {π}) βͺ (π» βͺ {π})) = (πΊ βͺ π»)) |
53 | 52 | fveq2d 6847 |
. . . . . . . . . 10
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β (πβ((πΊ β {π}) βͺ (π» βͺ {π}))) = (πβ(πΊ βͺ π»))) |
54 | 43, 53 | sseqtrrd 3986 |
. . . . . . . . 9
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β πΉ β (πβ((πΊ β {π}) βͺ (π» βͺ {π})))) |
55 | 54 | ssdifssd 4103 |
. . . . . . . 8
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β (πΉ β {π}) β (πβ((πΊ β {π}) βͺ (π» βͺ {π})))) |
56 | | simpr3 1197 |
. . . . . . . 8
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ) |
57 | | mreexexlem4d.B |
. . . . . . . . . 10
β’ (π β (πΉ β suc πΏ β¨ πΊ β suc πΏ)) |
58 | 57 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β (πΉ β suc πΏ β¨ πΊ β suc πΏ)) |
59 | | mreexexlem4d.9 |
. . . . . . . . . . . 12
β’ (π β πΏ β Ο) |
60 | 59 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β πΏ β Ο) |
61 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β π β πΉ) |
62 | | 3anan12 1097 |
. . . . . . . . . . . . 13
β’ ((πΏ β Ο β§ πΉ β suc πΏ β§ π β πΉ) β (πΉ β suc πΏ β§ (πΏ β Ο β§ π β πΉ))) |
63 | | dif1ennn 9108 |
. . . . . . . . . . . . 13
β’ ((πΏ β Ο β§ πΉ β suc πΏ β§ π β πΉ) β (πΉ β {π}) β πΏ) |
64 | 62, 63 | sylbir 234 |
. . . . . . . . . . . 12
β’ ((πΉ β suc πΏ β§ (πΏ β Ο β§ π β πΉ)) β (πΉ β {π}) β πΏ) |
65 | 64 | expcom 415 |
. . . . . . . . . . 11
β’ ((πΏ β Ο β§ π β πΉ) β (πΉ β suc πΏ β (πΉ β {π}) β πΏ)) |
66 | 60, 61, 65 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β (πΉ β suc πΏ β (πΉ β {π}) β πΏ)) |
67 | | 3anan12 1097 |
. . . . . . . . . . . . 13
β’ ((πΏ β Ο β§ πΊ β suc πΏ β§ π β πΊ) β (πΊ β suc πΏ β§ (πΏ β Ο β§ π β πΊ))) |
68 | | dif1ennn 9108 |
. . . . . . . . . . . . 13
β’ ((πΏ β Ο β§ πΊ β suc πΏ β§ π β πΊ) β (πΊ β {π}) β πΏ) |
69 | 67, 68 | sylbir 234 |
. . . . . . . . . . . 12
β’ ((πΊ β suc πΏ β§ (πΏ β Ο β§ π β πΊ)) β (πΊ β {π}) β πΏ) |
70 | 69 | expcom 415 |
. . . . . . . . . . 11
β’ ((πΏ β Ο β§ π β πΊ) β (πΊ β suc πΏ β (πΊ β {π}) β πΏ)) |
71 | 60, 44, 70 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β (πΊ β suc πΏ β (πΊ β {π}) β πΏ)) |
72 | 66, 71 | orim12d 964 |
. . . . . . . . 9
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β ((πΉ β suc πΏ β¨ πΊ β suc πΏ) β ((πΉ β {π}) β πΏ β¨ (πΊ β {π}) β πΏ))) |
73 | 58, 72 | mpd 15 |
. . . . . . . 8
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β ((πΉ β {π}) β πΏ β¨ (πΊ β {π}) β πΏ)) |
74 | | mreexexlem4d.A |
. . . . . . . . 9
β’ (π β βββπ β π« (π β β)βπ β π« (π β β)(((π β πΏ β¨ π β πΏ) β§ π β (πβ(π βͺ β)) β§ (π βͺ β) β πΌ) β βπ β π« π(π β π β§ (π βͺ β) β πΌ))) |
75 | 74 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β βββπ β π« (π β β)βπ β π« (π β β)(((π β πΏ β¨ π β πΏ) β§ π β (πβ(π βͺ β)) β§ (π βͺ β) β πΌ) β βπ β π« π(π β π β§ (π βͺ β) β πΌ))) |
76 | 30, 39, 42, 55, 56, 73, 75 | mreexexlemd 17529 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β βπ β π« (πΊ β {π})((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ)) |
77 | 30 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β π β V) |
78 | 9 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β πΊ β (π β π»)) |
79 | 78 | difss2d 4095 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β πΊ β π) |
80 | 77, 79 | ssexd 5282 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β πΊ β V) |
81 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β π β π« (πΊ β {π})) |
82 | 81 | elpwid 4570 |
. . . . . . . . . . 11
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β π β (πΊ β {π})) |
83 | 82 | difss2d 4095 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β π β πΊ) |
84 | | simplr1 1216 |
. . . . . . . . . . 11
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β π β πΊ) |
85 | 84 | snssd 4770 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β {π} β πΊ) |
86 | 83, 85 | unssd 4147 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β (π βͺ {π}) β πΊ) |
87 | 80, 86 | sselpwd 5284 |
. . . . . . . 8
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β (π βͺ {π}) β π« πΊ) |
88 | | difsnid 4771 |
. . . . . . . . . 10
β’ (π β πΉ β ((πΉ β {π}) βͺ {π}) = πΉ) |
89 | 88 | ad3antlr 730 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β ((πΉ β {π}) βͺ {π}) = πΉ) |
90 | | simprrl 780 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β (πΉ β {π}) β π) |
91 | | en2sn 8988 |
. . . . . . . . . . . 12
β’ ((π β V β§ π β V) β {π} β {π}) |
92 | 91 | el2v 3452 |
. . . . . . . . . . 11
β’ {π} β {π} |
93 | 92 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β {π} β {π}) |
94 | | disjdifr 4433 |
. . . . . . . . . . 11
β’ ((πΉ β {π}) β© {π}) = β
|
95 | 94 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β ((πΉ β {π}) β© {π}) = β
) |
96 | | ssdifin0 4444 |
. . . . . . . . . . 11
β’ (π β (πΊ β {π}) β (π β© {π}) = β
) |
97 | 82, 96 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β (π β© {π}) = β
) |
98 | | unen 8993 |
. . . . . . . . . 10
β’ ((((πΉ β {π}) β π β§ {π} β {π}) β§ (((πΉ β {π}) β© {π}) = β
β§ (π β© {π}) = β
)) β ((πΉ β {π}) βͺ {π}) β (π βͺ {π})) |
99 | 90, 93, 95, 97, 98 | syl22anc 838 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β ((πΉ β {π}) βͺ {π}) β (π βͺ {π})) |
100 | 89, 99 | eqbrtrrd 5130 |
. . . . . . . 8
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β πΉ β (π βͺ {π})) |
101 | | unass 4127 |
. . . . . . . . . 10
β’ ((π βͺ {π}) βͺ π») = (π βͺ ({π} βͺ π»)) |
102 | | uncom 4114 |
. . . . . . . . . . 11
β’ ({π} βͺ π») = (π» βͺ {π}) |
103 | 102 | uneq2i 4121 |
. . . . . . . . . 10
β’ (π βͺ ({π} βͺ π»)) = (π βͺ (π» βͺ {π})) |
104 | 101, 103 | eqtr2i 2762 |
. . . . . . . . 9
β’ (π βͺ (π» βͺ {π})) = ((π βͺ {π}) βͺ π») |
105 | | simprrr 781 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β (π βͺ (π» βͺ {π})) β πΌ) |
106 | 104, 105 | eqeltrrid 2839 |
. . . . . . . 8
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β ((π βͺ {π}) βͺ π») β πΌ) |
107 | | breq2 5110 |
. . . . . . . . . 10
β’ (π = (π βͺ {π}) β (πΉ β π β πΉ β (π βͺ {π}))) |
108 | | uneq1 4117 |
. . . . . . . . . . 11
β’ (π = (π βͺ {π}) β (π βͺ π») = ((π βͺ {π}) βͺ π»)) |
109 | 108 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = (π βͺ {π}) β ((π βͺ π») β πΌ β ((π βͺ {π}) βͺ π») β πΌ)) |
110 | 107, 109 | anbi12d 632 |
. . . . . . . . 9
β’ (π = (π βͺ {π}) β ((πΉ β π β§ (π βͺ π») β πΌ) β (πΉ β (π βͺ {π}) β§ ((π βͺ {π}) βͺ π») β πΌ))) |
111 | 110 | rspcev 3580 |
. . . . . . . 8
β’ (((π βͺ {π}) β π« πΊ β§ (πΉ β (π βͺ {π}) β§ ((π βͺ {π}) βͺ π») β πΌ)) β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |
112 | 87, 100, 106, 111 | syl12anc 836 |
. . . . . . 7
β’ ((((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β§ (π β π« (πΊ β {π}) β§ ((πΉ β {π}) β π β§ (π βͺ (π» βͺ {π})) β πΌ))) β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |
113 | 76, 112 | rexlimddv 3155 |
. . . . . 6
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ)) β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |
114 | 28, 113 | sylan2br 596 |
. . . . 5
β’ (((π β§ π β πΉ) β§ (π β πΊ β§ (Β¬ π β (πΉ β {π}) β§ ((πΉ β {π}) βͺ (π» βͺ {π})) β πΌ))) β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |
115 | 27, 114 | rexlimddv 3155 |
. . . 4
β’ ((π β§ π β πΉ) β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |
116 | 115 | adantlr 714 |
. . 3
β’ (((π β§ πΉ β β
) β§ π β πΉ) β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |
117 | 19, 116 | exlimddv 1939 |
. 2
β’ ((π β§ πΉ β β
) β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |
118 | 16, 117 | pm2.61dane 3029 |
1
β’ (π β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |