Step | Hyp | Ref
| Expression |
1 | | sspr 4794 |
. . . . 5
β’ (π₯ β {β
, π΄} β ((π₯ = β
β¨ π₯ = {β
}) β¨ (π₯ = {π΄} β¨ π₯ = {β
, π΄}))) |
2 | | unieq 4877 |
. . . . . . . . 9
β’ (π₯ = β
β βͺ π₯ =
βͺ β
) |
3 | | uni0 4897 |
. . . . . . . . . 10
β’ βͺ β
= β
|
4 | | 0ex 5265 |
. . . . . . . . . . 11
β’ β
β V |
5 | 4 | prid1 4724 |
. . . . . . . . . 10
β’ β
β {β
, π΄} |
6 | 3, 5 | eqeltri 2830 |
. . . . . . . . 9
β’ βͺ β
β {β
, π΄} |
7 | 2, 6 | eqeltrdi 2842 |
. . . . . . . 8
β’ (π₯ = β
β βͺ π₯
β {β
, π΄}) |
8 | 7 | a1i 11 |
. . . . . . 7
β’ (π΄ β π β (π₯ = β
β βͺ π₯
β {β
, π΄})) |
9 | | unieq 4877 |
. . . . . . . . 9
β’ (π₯ = {β
} β βͺ π₯ =
βͺ {β
}) |
10 | 4 | unisn 4888 |
. . . . . . . . . 10
β’ βͺ {β
} = β
|
11 | 10, 5 | eqeltri 2830 |
. . . . . . . . 9
β’ βͺ {β
} β {β
, π΄} |
12 | 9, 11 | eqeltrdi 2842 |
. . . . . . . 8
β’ (π₯ = {β
} β βͺ π₯
β {β
, π΄}) |
13 | 12 | a1i 11 |
. . . . . . 7
β’ (π΄ β π β (π₯ = {β
} β βͺ π₯
β {β
, π΄})) |
14 | 8, 13 | jaod 858 |
. . . . . 6
β’ (π΄ β π β ((π₯ = β
β¨ π₯ = {β
}) β βͺ π₯
β {β
, π΄})) |
15 | | unieq 4877 |
. . . . . . . . . 10
β’ (π₯ = {π΄} β βͺ π₯ = βͺ
{π΄}) |
16 | | unisng 4887 |
. . . . . . . . . 10
β’ (π΄ β π β βͺ {π΄} = π΄) |
17 | 15, 16 | sylan9eqr 2795 |
. . . . . . . . 9
β’ ((π΄ β π β§ π₯ = {π΄}) β βͺ π₯ = π΄) |
18 | | prid2g 4723 |
. . . . . . . . . 10
β’ (π΄ β π β π΄ β {β
, π΄}) |
19 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β π β§ π₯ = {π΄}) β π΄ β {β
, π΄}) |
20 | 17, 19 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π΄ β π β§ π₯ = {π΄}) β βͺ π₯ β {β
, π΄}) |
21 | 20 | ex 414 |
. . . . . . 7
β’ (π΄ β π β (π₯ = {π΄} β βͺ π₯ β {β
, π΄})) |
22 | | unieq 4877 |
. . . . . . . . . 10
β’ (π₯ = {β
, π΄} β βͺ π₯ = βͺ
{β
, π΄}) |
23 | | uniprg 4883 |
. . . . . . . . . . . 12
β’ ((β
β V β§ π΄ β
π) β βͺ {β
, π΄} = (β
βͺ π΄)) |
24 | 4, 23 | mpan 689 |
. . . . . . . . . . 11
β’ (π΄ β π β βͺ
{β
, π΄} = (β
βͺ π΄)) |
25 | | uncom 4114 |
. . . . . . . . . . . 12
β’ (β
βͺ π΄) = (π΄ βͺ β
) |
26 | | un0 4351 |
. . . . . . . . . . . 12
β’ (π΄ βͺ β
) = π΄ |
27 | 25, 26 | eqtri 2761 |
. . . . . . . . . . 11
β’ (β
βͺ π΄) = π΄ |
28 | 24, 27 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π΄ β π β βͺ
{β
, π΄} = π΄) |
29 | 22, 28 | sylan9eqr 2795 |
. . . . . . . . 9
β’ ((π΄ β π β§ π₯ = {β
, π΄}) β βͺ π₯ = π΄) |
30 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β π β§ π₯ = {β
, π΄}) β π΄ β {β
, π΄}) |
31 | 29, 30 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π΄ β π β§ π₯ = {β
, π΄}) β βͺ π₯ β {β
, π΄}) |
32 | 31 | ex 414 |
. . . . . . 7
β’ (π΄ β π β (π₯ = {β
, π΄} β βͺ π₯ β {β
, π΄})) |
33 | 21, 32 | jaod 858 |
. . . . . 6
β’ (π΄ β π β ((π₯ = {π΄} β¨ π₯ = {β
, π΄}) β βͺ π₯ β {β
, π΄})) |
34 | 14, 33 | jaod 858 |
. . . . 5
β’ (π΄ β π β (((π₯ = β
β¨ π₯ = {β
}) β¨ (π₯ = {π΄} β¨ π₯ = {β
, π΄})) β βͺ
π₯ β {β
, π΄})) |
35 | 1, 34 | biimtrid 241 |
. . . 4
β’ (π΄ β π β (π₯ β {β
, π΄} β βͺ π₯ β {β
, π΄})) |
36 | 35 | alrimiv 1931 |
. . 3
β’ (π΄ β π β βπ₯(π₯ β {β
, π΄} β βͺ π₯ β {β
, π΄})) |
37 | | vex 3448 |
. . . . . 6
β’ π₯ β V |
38 | 37 | elpr 4610 |
. . . . 5
β’ (π₯ β {β
, π΄} β (π₯ = β
β¨ π₯ = π΄)) |
39 | | vex 3448 |
. . . . . . . . 9
β’ π¦ β V |
40 | 39 | elpr 4610 |
. . . . . . . 8
β’ (π¦ β {β
, π΄} β (π¦ = β
β¨ π¦ = π΄)) |
41 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π₯ = β
β§ π¦ = β
) β π¦ = β
) |
42 | 41 | ineq2d 4173 |
. . . . . . . . . . . . 13
β’ ((π₯ = β
β§ π¦ = β
) β (π₯ β© π¦) = (π₯ β© β
)) |
43 | | in0 4352 |
. . . . . . . . . . . . 13
β’ (π₯ β© β
) =
β
|
44 | 42, 43 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ ((π₯ = β
β§ π¦ = β
) β (π₯ β© π¦) = β
) |
45 | 44, 5 | eqeltrdi 2842 |
. . . . . . . . . . 11
β’ ((π₯ = β
β§ π¦ = β
) β (π₯ β© π¦) β {β
, π΄}) |
46 | 45 | a1i 11 |
. . . . . . . . . 10
β’ (π΄ β π β ((π₯ = β
β§ π¦ = β
) β (π₯ β© π¦) β {β
, π΄})) |
47 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π₯ = π΄ β§ π¦ = β
) β π¦ = β
) |
48 | 47 | ineq2d 4173 |
. . . . . . . . . . . . 13
β’ ((π₯ = π΄ β§ π¦ = β
) β (π₯ β© π¦) = (π₯ β© β
)) |
49 | 48, 43 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ ((π₯ = π΄ β§ π¦ = β
) β (π₯ β© π¦) = β
) |
50 | 49, 5 | eqeltrdi 2842 |
. . . . . . . . . . 11
β’ ((π₯ = π΄ β§ π¦ = β
) β (π₯ β© π¦) β {β
, π΄}) |
51 | 50 | a1i 11 |
. . . . . . . . . 10
β’ (π΄ β π β ((π₯ = π΄ β§ π¦ = β
) β (π₯ β© π¦) β {β
, π΄})) |
52 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π₯ = β
β§ π¦ = π΄) β π₯ = β
) |
53 | 52 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’ ((π₯ = β
β§ π¦ = π΄) β (π₯ β© π¦) = (β
β© π¦)) |
54 | | 0in 4354 |
. . . . . . . . . . . . 13
β’ (β
β© π¦) =
β
|
55 | 53, 54 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ ((π₯ = β
β§ π¦ = π΄) β (π₯ β© π¦) = β
) |
56 | 55, 5 | eqeltrdi 2842 |
. . . . . . . . . . 11
β’ ((π₯ = β
β§ π¦ = π΄) β (π₯ β© π¦) β {β
, π΄}) |
57 | 56 | a1i 11 |
. . . . . . . . . 10
β’ (π΄ β π β ((π₯ = β
β§ π¦ = π΄) β (π₯ β© π¦) β {β
, π΄})) |
58 | | ineq12 4168 |
. . . . . . . . . . . . . 14
β’ ((π₯ = π΄ β§ π¦ = π΄) β (π₯ β© π¦) = (π΄ β© π΄)) |
59 | 58 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ (π₯ = π΄ β§ π¦ = π΄)) β (π₯ β© π¦) = (π΄ β© π΄)) |
60 | | inidm 4179 |
. . . . . . . . . . . . 13
β’ (π΄ β© π΄) = π΄ |
61 | 59, 60 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π₯ = π΄ β§ π¦ = π΄)) β (π₯ β© π¦) = π΄) |
62 | 18 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π₯ = π΄ β§ π¦ = π΄)) β π΄ β {β
, π΄}) |
63 | 61, 62 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π₯ = π΄ β§ π¦ = π΄)) β (π₯ β© π¦) β {β
, π΄}) |
64 | 63 | ex 414 |
. . . . . . . . . 10
β’ (π΄ β π β ((π₯ = π΄ β§ π¦ = π΄) β (π₯ β© π¦) β {β
, π΄})) |
65 | 46, 51, 57, 64 | ccased 1038 |
. . . . . . . . 9
β’ (π΄ β π β (((π₯ = β
β¨ π₯ = π΄) β§ (π¦ = β
β¨ π¦ = π΄)) β (π₯ β© π¦) β {β
, π΄})) |
66 | 65 | expdimp 454 |
. . . . . . . 8
β’ ((π΄ β π β§ (π₯ = β
β¨ π₯ = π΄)) β ((π¦ = β
β¨ π¦ = π΄) β (π₯ β© π¦) β {β
, π΄})) |
67 | 40, 66 | biimtrid 241 |
. . . . . . 7
β’ ((π΄ β π β§ (π₯ = β
β¨ π₯ = π΄)) β (π¦ β {β
, π΄} β (π₯ β© π¦) β {β
, π΄})) |
68 | 67 | ralrimiv 3139 |
. . . . . 6
β’ ((π΄ β π β§ (π₯ = β
β¨ π₯ = π΄)) β βπ¦ β {β
, π΄} (π₯ β© π¦) β {β
, π΄}) |
69 | 68 | ex 414 |
. . . . 5
β’ (π΄ β π β ((π₯ = β
β¨ π₯ = π΄) β βπ¦ β {β
, π΄} (π₯ β© π¦) β {β
, π΄})) |
70 | 38, 69 | biimtrid 241 |
. . . 4
β’ (π΄ β π β (π₯ β {β
, π΄} β βπ¦ β {β
, π΄} (π₯ β© π¦) β {β
, π΄})) |
71 | 70 | ralrimiv 3139 |
. . 3
β’ (π΄ β π β βπ₯ β {β
, π΄}βπ¦ β {β
, π΄} (π₯ β© π¦) β {β
, π΄}) |
72 | | prex 5390 |
. . . 4
β’ {β
,
π΄} β
V |
73 | | istopg 22260 |
. . . 4
β’
({β
, π΄} β
V β ({β
, π΄}
β Top β (βπ₯(π₯ β {β
, π΄} β βͺ π₯ β {β
, π΄}) β§ βπ₯ β {β
, π΄}βπ¦ β {β
, π΄} (π₯ β© π¦) β {β
, π΄}))) |
74 | 72, 73 | mp1i 13 |
. . 3
β’ (π΄ β π β ({β
, π΄} β Top β (βπ₯(π₯ β {β
, π΄} β βͺ π₯ β {β
, π΄}) β§ βπ₯ β {β
, π΄}βπ¦ β {β
, π΄} (π₯ β© π¦) β {β
, π΄}))) |
75 | 36, 71, 74 | mpbir2and 712 |
. 2
β’ (π΄ β π β {β
, π΄} β Top) |
76 | 28 | eqcomd 2739 |
. 2
β’ (π΄ β π β π΄ = βͺ {β
,
π΄}) |
77 | | istopon 22277 |
. 2
β’
({β
, π΄} β
(TopOnβπ΄) β
({β
, π΄} β Top
β§ π΄ = βͺ {β
, π΄})) |
78 | 75, 76, 77 | sylanbrc 584 |
1
β’ (π΄ β π β {β
, π΄} β (TopOnβπ΄)) |