Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . 4
β’ ((π β§ πΉ = β
) β πΉ = β
) |
2 | | mreexexlem2d.1 |
. . . . . . . . . 10
β’ (π β π΄ β (Mooreβπ)) |
3 | 2 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ πΊ = β
) β π΄ β (Mooreβπ)) |
4 | | mreexexlem2d.2 |
. . . . . . . . 9
β’ π = (mrClsβπ΄) |
5 | | mreexexlem2d.3 |
. . . . . . . . 9
β’ πΌ = (mrIndβπ΄) |
6 | | mreexexlem2d.7 |
. . . . . . . . . . . 12
β’ (π β πΉ β (πβ(πΊ βͺ π»))) |
7 | 6 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ πΊ = β
) β πΉ β (πβ(πΊ βͺ π»))) |
8 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ ((π β§ πΊ = β
) β πΊ = β
) |
9 | 8 | uneq1d 4162 |
. . . . . . . . . . . . 13
β’ ((π β§ πΊ = β
) β (πΊ βͺ π») = (β
βͺ π»)) |
10 | | uncom 4153 |
. . . . . . . . . . . . . 14
β’ (π» βͺ β
) = (β
βͺ
π») |
11 | | un0 4390 |
. . . . . . . . . . . . . 14
β’ (π» βͺ β
) = π» |
12 | 10, 11 | eqtr3i 2762 |
. . . . . . . . . . . . 13
β’ (β
βͺ π») = π» |
13 | 9, 12 | eqtrdi 2788 |
. . . . . . . . . . . 12
β’ ((π β§ πΊ = β
) β (πΊ βͺ π») = π») |
14 | 13 | fveq2d 6895 |
. . . . . . . . . . 11
β’ ((π β§ πΊ = β
) β (πβ(πΊ βͺ π»)) = (πβπ»)) |
15 | 7, 14 | sseqtrd 4022 |
. . . . . . . . . 10
β’ ((π β§ πΊ = β
) β πΉ β (πβπ»)) |
16 | | mreexexlem2d.8 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ βͺ π») β πΌ) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ πΊ = β
) β (πΉ βͺ π») β πΌ) |
18 | 5, 3, 17 | mrissd 17582 |
. . . . . . . . . . . 12
β’ ((π β§ πΊ = β
) β (πΉ βͺ π») β π) |
19 | 18 | unssbd 4188 |
. . . . . . . . . . 11
β’ ((π β§ πΊ = β
) β π» β π) |
20 | 3, 4, 19 | mrcssidd 17571 |
. . . . . . . . . 10
β’ ((π β§ πΊ = β
) β π» β (πβπ»)) |
21 | 15, 20 | unssd 4186 |
. . . . . . . . 9
β’ ((π β§ πΊ = β
) β (πΉ βͺ π») β (πβπ»)) |
22 | | ssun2 4173 |
. . . . . . . . . 10
β’ π» β (πΉ βͺ π») |
23 | 22 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ πΊ = β
) β π» β (πΉ βͺ π»)) |
24 | 3, 4, 5, 21, 23, 17 | mrissmrcd 17586 |
. . . . . . . 8
β’ ((π β§ πΊ = β
) β (πΉ βͺ π») = π») |
25 | | ssequn1 4180 |
. . . . . . . 8
β’ (πΉ β π» β (πΉ βͺ π») = π») |
26 | 24, 25 | sylibr 233 |
. . . . . . 7
β’ ((π β§ πΊ = β
) β πΉ β π») |
27 | | mreexexlem2d.5 |
. . . . . . . 8
β’ (π β πΉ β (π β π»)) |
28 | 27 | adantr 481 |
. . . . . . 7
β’ ((π β§ πΊ = β
) β πΉ β (π β π»)) |
29 | 26, 28 | ssind 4232 |
. . . . . 6
β’ ((π β§ πΊ = β
) β πΉ β (π» β© (π β π»))) |
30 | | disjdif 4471 |
. . . . . 6
β’ (π» β© (π β π»)) = β
|
31 | 29, 30 | sseqtrdi 4032 |
. . . . 5
β’ ((π β§ πΊ = β
) β πΉ β β
) |
32 | | ss0b 4397 |
. . . . 5
β’ (πΉ β β
β πΉ = β
) |
33 | 31, 32 | sylib 217 |
. . . 4
β’ ((π β§ πΊ = β
) β πΉ = β
) |
34 | | mreexexlem3d.9 |
. . . 4
β’ (π β (πΉ = β
β¨ πΊ = β
)) |
35 | 1, 33, 34 | mpjaodan 957 |
. . 3
β’ (π β πΉ = β
) |
36 | | 0elpw 5354 |
. . 3
β’ β
β π« πΊ |
37 | 35, 36 | eqeltrdi 2841 |
. 2
β’ (π β πΉ β π« πΊ) |
38 | 2 | elfvexd 6930 |
. . . 4
β’ (π β π β V) |
39 | 27 | difss2d 4134 |
. . . 4
β’ (π β πΉ β π) |
40 | 38, 39 | ssexd 5324 |
. . 3
β’ (π β πΉ β V) |
41 | | enrefg 8982 |
. . 3
β’ (πΉ β V β πΉ β πΉ) |
42 | 40, 41 | syl 17 |
. 2
β’ (π β πΉ β πΉ) |
43 | | breq2 5152 |
. . . 4
β’ (π = πΉ β (πΉ β π β πΉ β πΉ)) |
44 | | uneq1 4156 |
. . . . 5
β’ (π = πΉ β (π βͺ π») = (πΉ βͺ π»)) |
45 | 44 | eleq1d 2818 |
. . . 4
β’ (π = πΉ β ((π βͺ π») β πΌ β (πΉ βͺ π») β πΌ)) |
46 | 43, 45 | anbi12d 631 |
. . 3
β’ (π = πΉ β ((πΉ β π β§ (π βͺ π») β πΌ) β (πΉ β πΉ β§ (πΉ βͺ π») β πΌ))) |
47 | 46 | rspcev 3612 |
. 2
β’ ((πΉ β π« πΊ β§ (πΉ β πΉ β§ (πΉ βͺ π») β πΌ)) β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |
48 | 37, 42, 16, 47 | syl12anc 835 |
1
β’ (π β βπ β π« πΊ(πΉ β π β§ (π βͺ π») β πΌ)) |