Step | Hyp | Ref
| Expression |
1 | | difeq2 4081 |
. . . . . . . 8
β’ (π₯ = βͺ
π¦ β (π΄ β π₯) = (π΄ β βͺ π¦)) |
2 | 1 | breq1d 5120 |
. . . . . . 7
β’ (π₯ = βͺ
π¦ β ((π΄ β π₯) βΌ Ο β (π΄ β βͺ π¦) βΌ
Ο)) |
3 | | eqeq1 2741 |
. . . . . . 7
β’ (π₯ = βͺ
π¦ β (π₯ = β
β βͺ π¦ =
β
)) |
4 | 2, 3 | orbi12d 918 |
. . . . . 6
β’ (π₯ = βͺ
π¦ β (((π΄ β π₯) βΌ Ο β¨ π₯ = β
) β ((π΄ β βͺ π¦) βΌ Ο β¨ βͺ π¦ =
β
))) |
5 | | uniss 4878 |
. . . . . . . 8
β’ (π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β βͺ π¦
β βͺ {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) |
6 | | ssrab2 4042 |
. . . . . . . . 9
β’ {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β π« π΄ |
7 | | sspwuni 5065 |
. . . . . . . . 9
β’ ({π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β π« π΄ β βͺ {π₯
β π« π΄ β£
((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β π΄) |
8 | 6, 7 | mpbi 229 |
. . . . . . . 8
β’ βͺ {π₯
β π« π΄ β£
((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β π΄ |
9 | 5, 8 | sstrdi 3961 |
. . . . . . 7
β’ (π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β βͺ π¦
β π΄) |
10 | | vuniex 7681 |
. . . . . . . 8
β’ βͺ π¦
β V |
11 | 10 | elpw 4569 |
. . . . . . 7
β’ (βͺ π¦
β π« π΄ β
βͺ π¦ β π΄) |
12 | 9, 11 | sylibr 233 |
. . . . . 6
β’ (π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β βͺ π¦
β π« π΄) |
13 | | uni0c 4900 |
. . . . . . . . . . 11
β’ (βͺ π¦ =
β
β βπ§
β π¦ π§ = β
) |
14 | 13 | notbii 320 |
. . . . . . . . . 10
β’ (Β¬
βͺ π¦ = β
β Β¬ βπ§ β π¦ π§ = β
) |
15 | | rexnal 3104 |
. . . . . . . . . 10
β’
(βπ§ β
π¦ Β¬ π§ = β
β Β¬ βπ§ β π¦ π§ = β
) |
16 | 14, 15 | bitr4i 278 |
. . . . . . . . 9
β’ (Β¬
βͺ π¦ = β
β βπ§ β π¦ Β¬ π§ = β
) |
17 | | ssel2 3944 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β π§ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) |
18 | | difeq2 4081 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π§ β (π΄ β π₯) = (π΄ β π§)) |
19 | 18 | breq1d 5120 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π§ β ((π΄ β π₯) βΌ Ο β (π΄ β π§) βΌ Ο)) |
20 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π§ β (π₯ = β
β π§ = β
)) |
21 | 19, 20 | orbi12d 918 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β (((π΄ β π₯) βΌ Ο β¨ π₯ = β
) β ((π΄ β π§) βΌ Ο β¨ π§ = β
))) |
22 | 21 | elrab 3650 |
. . . . . . . . . . . . . . . 16
β’ (π§ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β (π§ β π« π΄ β§ ((π΄ β π§) βΌ Ο β¨ π§ = β
))) |
23 | 17, 22 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β (π§ β π« π΄ β§ ((π΄ β π§) βΌ Ο β¨ π§ = β
))) |
24 | 23 | simprd 497 |
. . . . . . . . . . . . . 14
β’ ((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β ((π΄ β π§) βΌ Ο β¨ π§ = β
)) |
25 | 24 | ord 863 |
. . . . . . . . . . . . 13
β’ ((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β (Β¬ (π΄ β π§) βΌ Ο β π§ = β
)) |
26 | 25 | con1d 145 |
. . . . . . . . . . . 12
β’ ((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β (Β¬ π§ = β
β (π΄ β π§) βΌ Ο)) |
27 | 26 | imp 408 |
. . . . . . . . . . 11
β’ (((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β§ Β¬ π§ = β
) β (π΄ β π§) βΌ Ο) |
28 | | ctex 8910 |
. . . . . . . . . . . . . 14
β’ ((π΄ β π§) βΌ Ο β (π΄ β π§) β V) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β§ Β¬ π§ = β
) β§ (π΄ β π§) βΌ Ο) β (π΄ β π§) β V) |
30 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β§ Β¬ π§ = β
) β§ (π΄ β π§) βΌ Ο) β π§ β π¦) |
31 | | elssuni 4903 |
. . . . . . . . . . . . . 14
β’ (π§ β π¦ β π§ β βͺ π¦) |
32 | | sscon 4103 |
. . . . . . . . . . . . . 14
β’ (π§ β βͺ π¦
β (π΄ β βͺ π¦)
β (π΄ β π§)) |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . . . . . . . 13
β’ ((((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β§ Β¬ π§ = β
) β§ (π΄ β π§) βΌ Ο) β (π΄ β βͺ π¦) β (π΄ β π§)) |
34 | | ssdomg 8947 |
. . . . . . . . . . . . 13
β’ ((π΄ β π§) β V β ((π΄ β βͺ π¦) β (π΄ β π§) β (π΄ β βͺ π¦) βΌ (π΄ β π§))) |
35 | 29, 33, 34 | sylc 65 |
. . . . . . . . . . . 12
β’ ((((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β§ Β¬ π§ = β
) β§ (π΄ β π§) βΌ Ο) β (π΄ β βͺ π¦) βΌ (π΄ β π§)) |
36 | | domtr 8954 |
. . . . . . . . . . . 12
β’ (((π΄ β βͺ π¦)
βΌ (π΄ β π§) β§ (π΄ β π§) βΌ Ο) β (π΄ β βͺ π¦) βΌ
Ο) |
37 | 35, 36 | sylancom 589 |
. . . . . . . . . . 11
β’ ((((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β§ Β¬ π§ = β
) β§ (π΄ β π§) βΌ Ο) β (π΄ β βͺ π¦) βΌ
Ο) |
38 | 27, 37 | mpdan 686 |
. . . . . . . . . 10
β’ (((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β π¦) β§ Β¬ π§ = β
) β (π΄ β βͺ π¦) βΌ
Ο) |
39 | 38 | rexlimdva2 3155 |
. . . . . . . . 9
β’ (π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β (βπ§ β π¦ Β¬ π§ = β
β (π΄ β βͺ π¦) βΌ
Ο)) |
40 | 16, 39 | biimtrid 241 |
. . . . . . . 8
β’ (π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β (Β¬ βͺ π¦ =
β
β (π΄ β
βͺ π¦) βΌ Ο)) |
41 | 40 | con1d 145 |
. . . . . . 7
β’ (π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β (Β¬ (π΄ β βͺ π¦) βΌ Ο β βͺ π¦ =
β
)) |
42 | 41 | orrd 862 |
. . . . . 6
β’ (π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β ((π΄ β βͺ π¦) βΌ Ο β¨ βͺ π¦ =
β
)) |
43 | 4, 12, 42 | elrabd 3652 |
. . . . 5
β’ (π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β βͺ π¦
β {π₯ β π«
π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) |
44 | 43 | ax-gen 1798 |
. . . 4
β’
βπ¦(π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β βͺ π¦
β {π₯ β π«
π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) |
45 | | difeq2 4081 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (π΄ β π₯) = (π΄ β π¦)) |
46 | 45 | breq1d 5120 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((π΄ β π₯) βΌ Ο β (π΄ β π¦) βΌ Ο)) |
47 | | eqeq1 2741 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯ = β
β π¦ = β
)) |
48 | 46, 47 | orbi12d 918 |
. . . . . . . 8
β’ (π₯ = π¦ β (((π΄ β π₯) βΌ Ο β¨ π₯ = β
) β ((π΄ β π¦) βΌ Ο β¨ π¦ = β
))) |
49 | 48 | elrab 3650 |
. . . . . . 7
β’ (π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β (π¦ β π« π΄ β§ ((π΄ β π¦) βΌ Ο β¨ π¦ = β
))) |
50 | | ssinss1 4202 |
. . . . . . . . . 10
β’ (π¦ β π΄ β (π¦ β© π§) β π΄) |
51 | | vex 3452 |
. . . . . . . . . . 11
β’ π¦ β V |
52 | 51 | elpw 4569 |
. . . . . . . . . 10
β’ (π¦ β π« π΄ β π¦ β π΄) |
53 | 51 | inex1 5279 |
. . . . . . . . . . 11
β’ (π¦ β© π§) β V |
54 | 53 | elpw 4569 |
. . . . . . . . . 10
β’ ((π¦ β© π§) β π« π΄ β (π¦ β© π§) β π΄) |
55 | 50, 52, 54 | 3imtr4i 292 |
. . . . . . . . 9
β’ (π¦ β π« π΄ β (π¦ β© π§) β π« π΄) |
56 | 55 | ad2antrr 725 |
. . . . . . . 8
β’ (((π¦ β π« π΄ β§ ((π΄ β π¦) βΌ Ο β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ ((π΄ β π§) βΌ Ο β¨ π§ = β
))) β (π¦ β© π§) β π« π΄) |
57 | | difindi 4246 |
. . . . . . . . . . . 12
β’ (π΄ β (π¦ β© π§)) = ((π΄ β π¦) βͺ (π΄ β π§)) |
58 | | unctb 10148 |
. . . . . . . . . . . 12
β’ (((π΄ β π¦) βΌ Ο β§ (π΄ β π§) βΌ Ο) β ((π΄ β π¦) βͺ (π΄ β π§)) βΌ Ο) |
59 | 57, 58 | eqbrtrid 5145 |
. . . . . . . . . . 11
β’ (((π΄ β π¦) βΌ Ο β§ (π΄ β π§) βΌ Ο) β (π΄ β (π¦ β© π§)) βΌ Ο) |
60 | 59 | orcd 872 |
. . . . . . . . . 10
β’ (((π΄ β π¦) βΌ Ο β§ (π΄ β π§) βΌ Ο) β ((π΄ β (π¦ β© π§)) βΌ Ο β¨ (π¦ β© π§) = β
)) |
61 | | ineq1 4170 |
. . . . . . . . . . . 12
β’ (π¦ = β
β (π¦ β© π§) = (β
β© π§)) |
62 | | 0in 4358 |
. . . . . . . . . . . 12
β’ (β
β© π§) =
β
|
63 | 61, 62 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (π¦ = β
β (π¦ β© π§) = β
) |
64 | 63 | olcd 873 |
. . . . . . . . . 10
β’ (π¦ = β
β ((π΄ β (π¦ β© π§)) βΌ Ο β¨ (π¦ β© π§) = β
)) |
65 | | ineq2 4171 |
. . . . . . . . . . . 12
β’ (π§ = β
β (π¦ β© π§) = (π¦ β© β
)) |
66 | | in0 4356 |
. . . . . . . . . . . 12
β’ (π¦ β© β
) =
β
|
67 | 65, 66 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (π§ = β
β (π¦ β© π§) = β
) |
68 | 67 | olcd 873 |
. . . . . . . . . 10
β’ (π§ = β
β ((π΄ β (π¦ β© π§)) βΌ Ο β¨ (π¦ β© π§) = β
)) |
69 | 60, 64, 68 | ccase2 1039 |
. . . . . . . . 9
β’ ((((π΄ β π¦) βΌ Ο β¨ π¦ = β
) β§ ((π΄ β π§) βΌ Ο β¨ π§ = β
)) β ((π΄ β (π¦ β© π§)) βΌ Ο β¨ (π¦ β© π§) = β
)) |
70 | 69 | ad2ant2l 745 |
. . . . . . . 8
β’ (((π¦ β π« π΄ β§ ((π΄ β π¦) βΌ Ο β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ ((π΄ β π§) βΌ Ο β¨ π§ = β
))) β ((π΄ β (π¦ β© π§)) βΌ Ο β¨ (π¦ β© π§) = β
)) |
71 | 56, 70 | jca 513 |
. . . . . . 7
β’ (((π¦ β π« π΄ β§ ((π΄ β π¦) βΌ Ο β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ ((π΄ β π§) βΌ Ο β¨ π§ = β
))) β ((π¦ β© π§) β π« π΄ β§ ((π΄ β (π¦ β© π§)) βΌ Ο β¨ (π¦ β© π§) = β
))) |
72 | 49, 22, 71 | syl2anb 599 |
. . . . . 6
β’ ((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) β ((π¦ β© π§) β π« π΄ β§ ((π΄ β (π¦ β© π§)) βΌ Ο β¨ (π¦ β© π§) = β
))) |
73 | | difeq2 4081 |
. . . . . . . . 9
β’ (π₯ = (π¦ β© π§) β (π΄ β π₯) = (π΄ β (π¦ β© π§))) |
74 | 73 | breq1d 5120 |
. . . . . . . 8
β’ (π₯ = (π¦ β© π§) β ((π΄ β π₯) βΌ Ο β (π΄ β (π¦ β© π§)) βΌ Ο)) |
75 | | eqeq1 2741 |
. . . . . . . 8
β’ (π₯ = (π¦ β© π§) β (π₯ = β
β (π¦ β© π§) = β
)) |
76 | 74, 75 | orbi12d 918 |
. . . . . . 7
β’ (π₯ = (π¦ β© π§) β (((π΄ β π₯) βΌ Ο β¨ π₯ = β
) β ((π΄ β (π¦ β© π§)) βΌ Ο β¨ (π¦ β© π§) = β
))) |
77 | 76 | elrab 3650 |
. . . . . 6
β’ ((π¦ β© π§) β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β ((π¦ β© π§) β π« π΄ β§ ((π΄ β (π¦ β© π§)) βΌ Ο β¨ (π¦ β© π§) = β
))) |
78 | 72, 77 | sylibr 233 |
. . . . 5
β’ ((π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β§ π§ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) β (π¦ β© π§) β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) |
79 | 78 | rgen2 3195 |
. . . 4
β’
βπ¦ β
{π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}βπ§ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} (π¦ β© π§) β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} |
80 | 44, 79 | pm3.2i 472 |
. . 3
β’
(βπ¦(π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β βͺ π¦
β {π₯ β π«
π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) β§ βπ¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}βπ§ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} (π¦ β© π§) β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) |
81 | | pwexg 5338 |
. . . 4
β’ (π΄ β π β π« π΄ β V) |
82 | | rabexg 5293 |
. . . 4
β’
(π« π΄ β
V β {π₯ β
π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β V) |
83 | | istopg 22260 |
. . . 4
β’ ({π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β V β ({π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β Top β (βπ¦(π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β βͺ π¦
β {π₯ β π«
π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) β§ βπ¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}βπ§ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} (π¦ β© π§) β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}))) |
84 | 81, 82, 83 | 3syl 18 |
. . 3
β’ (π΄ β π β ({π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β Top β (βπ¦(π¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β βͺ π¦
β {π₯ β π«
π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) β§ βπ¦ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}βπ§ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} (π¦ β© π§) β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}))) |
85 | 80, 84 | mpbiri 258 |
. 2
β’ (π΄ β π β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β Top) |
86 | | difeq2 4081 |
. . . . . . . 8
β’ (π₯ = π΄ β (π΄ β π₯) = (π΄ β π΄)) |
87 | | difid 4335 |
. . . . . . . 8
β’ (π΄ β π΄) = β
|
88 | 86, 87 | eqtrdi 2793 |
. . . . . . 7
β’ (π₯ = π΄ β (π΄ β π₯) = β
) |
89 | 88 | breq1d 5120 |
. . . . . 6
β’ (π₯ = π΄ β ((π΄ β π₯) βΌ Ο β β
βΌ
Ο)) |
90 | | eqeq1 2741 |
. . . . . 6
β’ (π₯ = π΄ β (π₯ = β
β π΄ = β
)) |
91 | 89, 90 | orbi12d 918 |
. . . . 5
β’ (π₯ = π΄ β (((π΄ β π₯) βΌ Ο β¨ π₯ = β
) β (β
βΌ Ο
β¨ π΄ =
β
))) |
92 | | pwidg 4585 |
. . . . 5
β’ (π΄ β π β π΄ β π« π΄) |
93 | | omex 9586 |
. . . . . . . 8
β’ Ο
β V |
94 | 93 | 0dom 9057 |
. . . . . . 7
β’ β
βΌ Ο |
95 | 94 | orci 864 |
. . . . . 6
β’ (β
βΌ Ο β¨ π΄ =
β
) |
96 | 95 | a1i 11 |
. . . . 5
β’ (π΄ β π β (β
βΌ Ο β¨ π΄ = β
)) |
97 | 91, 92, 96 | elrabd 3652 |
. . . 4
β’ (π΄ β π β π΄ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) |
98 | | elssuni 4903 |
. . . 4
β’ (π΄ β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β π΄ β βͺ {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) |
99 | 97, 98 | syl 17 |
. . 3
β’ (π΄ β π β π΄ β βͺ {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) |
100 | 8 | a1i 11 |
. . 3
β’ (π΄ β π β βͺ {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β π΄) |
101 | 99, 100 | eqssd 3966 |
. 2
β’ (π΄ β π β π΄ = βͺ {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)}) |
102 | | istopon 22277 |
. 2
β’ ({π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β (TopOnβπ΄) β ({π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β Top β§ π΄ = βͺ
{π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)})) |
103 | 85, 101, 102 | sylanbrc 584 |
1
β’ (π΄ β π β {π₯ β π« π΄ β£ ((π΄ β π₯) βΌ Ο β¨ π₯ = β
)} β (TopOnβπ΄)) |