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