Step | Hyp | Ref
| Expression |
1 | | ssrab 4035 |
. . . . 5
β’ (π¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) |
2 | | eleq2 2827 |
. . . . . . . 8
β’ (π₯ = βͺ
π¦ β (π β π₯ β π β βͺ π¦)) |
3 | | eqeq1 2741 |
. . . . . . . 8
β’ (π₯ = βͺ
π¦ β (π₯ = β
β βͺ π¦ =
β
)) |
4 | 2, 3 | orbi12d 918 |
. . . . . . 7
β’ (π₯ = βͺ
π¦ β ((π β π₯ β¨ π₯ = β
) β (π β βͺ π¦ β¨ βͺ π¦ =
β
))) |
5 | | simprl 770 |
. . . . . . . . 9
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) β π¦ β π« π΄) |
6 | | sspwuni 5065 |
. . . . . . . . 9
β’ (π¦ β π« π΄ β βͺ π¦
β π΄) |
7 | 5, 6 | sylib 217 |
. . . . . . . 8
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) β βͺ π¦
β π΄) |
8 | | vuniex 7681 |
. . . . . . . . 9
β’ βͺ π¦
β V |
9 | 8 | elpw 4569 |
. . . . . . . 8
β’ (βͺ π¦
β π« π΄ β
βͺ π¦ β π΄) |
10 | 7, 9 | sylibr 233 |
. . . . . . 7
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) β βͺ π¦
β π« π΄) |
11 | | neq0 4310 |
. . . . . . . . . 10
β’ (Β¬
βͺ π¦ = β
β βπ§ π§ β βͺ π¦) |
12 | | eluni2 4874 |
. . . . . . . . . . . 12
β’ (π§ β βͺ π¦
β βπ₯ β
π¦ π§ β π₯) |
13 | | r19.29 3118 |
. . . . . . . . . . . . . . 15
β’
((βπ₯ β
π¦ (π β π₯ β¨ π₯ = β
) β§ βπ₯ β π¦ π§ β π₯) β βπ₯ β π¦ ((π β π₯ β¨ π₯ = β
) β§ π§ β π₯)) |
14 | | n0i 4298 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β π₯ β Β¬ π₯ = β
) |
15 | 14 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β π₯ β¨ π₯ = β
) β§ π§ β π₯) β Β¬ π₯ = β
) |
16 | | simpl 484 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β π₯ β¨ π₯ = β
) β§ π§ β π₯) β (π β π₯ β¨ π₯ = β
)) |
17 | 16 | ord 863 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β π₯ β¨ π₯ = β
) β§ π§ β π₯) β (Β¬ π β π₯ β π₯ = β
)) |
18 | 15, 17 | mt3d 148 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π₯ β¨ π₯ = β
) β§ π§ β π₯) β π β π₯) |
19 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π¦ β§ ((π β π₯ β¨ π₯ = β
) β§ π§ β π₯)) β π₯ β π¦) |
20 | | elunii 4875 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π₯ β§ π₯ β π¦) β π β βͺ π¦) |
21 | 18, 19, 20 | syl2an2 685 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π¦ β§ ((π β π₯ β¨ π₯ = β
) β§ π§ β π₯)) β π β βͺ π¦) |
22 | 21 | rexlimiva 3145 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
π¦ ((π β π₯ β¨ π₯ = β
) β§ π§ β π₯) β π β βͺ π¦) |
23 | 13, 22 | syl 17 |
. . . . . . . . . . . . . 14
β’
((βπ₯ β
π¦ (π β π₯ β¨ π₯ = β
) β§ βπ₯ β π¦ π§ β π₯) β π β βͺ π¦) |
24 | 23 | ex 414 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
π¦ (π β π₯ β¨ π₯ = β
) β (βπ₯ β π¦ π§ β π₯ β π β βͺ π¦)) |
25 | 24 | ad2antll 728 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) β (βπ₯ β π¦ π§ β π₯ β π β βͺ π¦)) |
26 | 12, 25 | biimtrid 241 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) β (π§ β βͺ π¦ β π β βͺ π¦)) |
27 | 26 | exlimdv 1937 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) β (βπ§ π§ β βͺ π¦ β π β βͺ π¦)) |
28 | 11, 27 | biimtrid 241 |
. . . . . . . . 9
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) β (Β¬ βͺ π¦ =
β
β π β
βͺ π¦)) |
29 | 28 | con1d 145 |
. . . . . . . 8
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) β (Β¬ π β βͺ π¦ β βͺ π¦ =
β
)) |
30 | 29 | orrd 862 |
. . . . . . 7
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) β (π β βͺ π¦ β¨ βͺ π¦ =
β
)) |
31 | 4, 10, 30 | elrabd 3652 |
. . . . . 6
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
))) β βͺ π¦
β {π₯ β π«
π΄ β£ (π β π₯ β¨ π₯ = β
)}) |
32 | 31 | ex 414 |
. . . . 5
β’ ((π΄ β π β§ π β π΄) β ((π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β¨ π₯ = β
)) β βͺ π¦
β {π₯ β π«
π΄ β£ (π β π₯ β¨ π₯ = β
)})) |
33 | 1, 32 | biimtrid 241 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β (π¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β βͺ π¦
β {π₯ β π«
π΄ β£ (π β π₯ β¨ π₯ = β
)})) |
34 | 33 | alrimiv 1931 |
. . 3
β’ ((π΄ β π β§ π β π΄) β βπ¦(π¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β βͺ π¦
β {π₯ β π«
π΄ β£ (π β π₯ β¨ π₯ = β
)})) |
35 | | eleq2 2827 |
. . . . . . . 8
β’ (π₯ = π¦ β (π β π₯ β π β π¦)) |
36 | | eqeq1 2741 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯ = β
β π¦ = β
)) |
37 | 35, 36 | orbi12d 918 |
. . . . . . 7
β’ (π₯ = π¦ β ((π β π₯ β¨ π₯ = β
) β (π β π¦ β¨ π¦ = β
))) |
38 | 37 | elrab 3650 |
. . . . . 6
β’ (π¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β (π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
))) |
39 | | eleq2 2827 |
. . . . . . . 8
β’ (π₯ = π§ β (π β π₯ β π β π§)) |
40 | | eqeq1 2741 |
. . . . . . . 8
β’ (π₯ = π§ β (π₯ = β
β π§ = β
)) |
41 | 39, 40 | orbi12d 918 |
. . . . . . 7
β’ (π₯ = π§ β ((π β π₯ β¨ π₯ = β
) β (π β π§ β¨ π§ = β
))) |
42 | 41 | elrab 3650 |
. . . . . 6
β’ (π§ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) |
43 | 38, 42 | anbi12i 628 |
. . . . 5
β’ ((π¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β§ π§ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}) β ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) |
44 | | eleq2 2827 |
. . . . . . . 8
β’ (π₯ = (π¦ β© π§) β (π β π₯ β π β (π¦ β© π§))) |
45 | | eqeq1 2741 |
. . . . . . . 8
β’ (π₯ = (π¦ β© π§) β (π₯ = β
β (π¦ β© π§) = β
)) |
46 | 44, 45 | orbi12d 918 |
. . . . . . 7
β’ (π₯ = (π¦ β© π§) β ((π β π₯ β¨ π₯ = β
) β (π β (π¦ β© π§) β¨ (π¦ β© π§) = β
))) |
47 | | inss1 4193 |
. . . . . . . . 9
β’ (π¦ β© π§) β π¦ |
48 | | simprll 778 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β π¦ β π« π΄) |
49 | 48 | elpwid 4574 |
. . . . . . . . 9
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β π¦ β π΄) |
50 | 47, 49 | sstrid 3960 |
. . . . . . . 8
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β (π¦ β© π§) β π΄) |
51 | | vex 3452 |
. . . . . . . . . 10
β’ π¦ β V |
52 | 51 | inex1 5279 |
. . . . . . . . 9
β’ (π¦ β© π§) β V |
53 | 52 | elpw 4569 |
. . . . . . . 8
β’ ((π¦ β© π§) β π« π΄ β (π¦ β© π§) β π΄) |
54 | 50, 53 | sylibr 233 |
. . . . . . 7
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β (π¦ β© π§) β π« π΄) |
55 | | ianor 981 |
. . . . . . . . . . 11
β’ (Β¬
(π β π¦ β§ π β π§) β (Β¬ π β π¦ β¨ Β¬ π β π§)) |
56 | | elin 3931 |
. . . . . . . . . . 11
β’ (π β (π¦ β© π§) β (π β π¦ β§ π β π§)) |
57 | 55, 56 | xchnxbir 333 |
. . . . . . . . . 10
β’ (Β¬
π β (π¦ β© π§) β (Β¬ π β π¦ β¨ Β¬ π β π§)) |
58 | | simprlr 779 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β (π β π¦ β¨ π¦ = β
)) |
59 | 58 | ord 863 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β (Β¬ π β π¦ β π¦ = β
)) |
60 | | simprrr 781 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β (π β π§ β¨ π§ = β
)) |
61 | 60 | ord 863 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β (Β¬ π β π§ β π§ = β
)) |
62 | 59, 61 | orim12d 964 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β ((Β¬ π β π¦ β¨ Β¬ π β π§) β (π¦ = β
β¨ π§ = β
))) |
63 | 57, 62 | biimtrid 241 |
. . . . . . . . 9
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β (Β¬ π β (π¦ β© π§) β (π¦ = β
β¨ π§ = β
))) |
64 | | inss 4203 |
. . . . . . . . . 10
β’ ((π¦ β β
β¨ π§ β β
) β (π¦ β© π§) β β
) |
65 | | ss0b 4362 |
. . . . . . . . . . 11
β’ (π¦ β β
β π¦ = β
) |
66 | | ss0b 4362 |
. . . . . . . . . . 11
β’ (π§ β β
β π§ = β
) |
67 | 65, 66 | orbi12i 914 |
. . . . . . . . . 10
β’ ((π¦ β β
β¨ π§ β β
) β (π¦ = β
β¨ π§ = β
)) |
68 | | ss0b 4362 |
. . . . . . . . . 10
β’ ((π¦ β© π§) β β
β (π¦ β© π§) = β
) |
69 | 64, 67, 68 | 3imtr3i 291 |
. . . . . . . . 9
β’ ((π¦ = β
β¨ π§ = β
) β (π¦ β© π§) = β
) |
70 | 63, 69 | syl6 35 |
. . . . . . . 8
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β (Β¬ π β (π¦ β© π§) β (π¦ β© π§) = β
)) |
71 | 70 | orrd 862 |
. . . . . . 7
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β (π β (π¦ β© π§) β¨ (π¦ β© π§) = β
)) |
72 | 46, 54, 71 | elrabd 3652 |
. . . . . 6
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)))) β (π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}) |
73 | 72 | ex 414 |
. . . . 5
β’ ((π΄ β π β§ π β π΄) β (((π¦ β π« π΄ β§ (π β π¦ β¨ π¦ = β
)) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β (π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)})) |
74 | 43, 73 | biimtrid 241 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β ((π¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β§ π§ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}) β (π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)})) |
75 | 74 | ralrimivv 3196 |
. . 3
β’ ((π΄ β π β§ π β π΄) β βπ¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}βπ§ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} (π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}) |
76 | | pwexg 5338 |
. . . . 5
β’ (π΄ β π β π« π΄ β V) |
77 | 76 | adantr 482 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β π« π΄ β V) |
78 | | rabexg 5293 |
. . . 4
β’
(π« π΄ β
V β {π₯ β
π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β V) |
79 | | istopg 22260 |
. . . 4
β’ ({π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β V β ({π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β Top β (βπ¦(π¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β βͺ π¦
β {π₯ β π«
π΄ β£ (π β π₯ β¨ π₯ = β
)}) β§ βπ¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}βπ§ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} (π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}))) |
80 | 77, 78, 79 | 3syl 18 |
. . 3
β’ ((π΄ β π β§ π β π΄) β ({π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β Top β (βπ¦(π¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β βͺ π¦
β {π₯ β π«
π΄ β£ (π β π₯ β¨ π₯ = β
)}) β§ βπ¦ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}βπ§ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} (π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}))) |
81 | 34, 75, 80 | mpbir2and 712 |
. 2
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β Top) |
82 | | eleq2 2827 |
. . . . . 6
β’ (π₯ = π΄ β (π β π₯ β π β π΄)) |
83 | | eqeq1 2741 |
. . . . . 6
β’ (π₯ = π΄ β (π₯ = β
β π΄ = β
)) |
84 | 82, 83 | orbi12d 918 |
. . . . 5
β’ (π₯ = π΄ β ((π β π₯ β¨ π₯ = β
) β (π β π΄ β¨ π΄ = β
))) |
85 | | pwidg 4585 |
. . . . . 6
β’ (π΄ β π β π΄ β π« π΄) |
86 | 85 | adantr 482 |
. . . . 5
β’ ((π΄ β π β§ π β π΄) β π΄ β π« π΄) |
87 | | animorrl 980 |
. . . . 5
β’ ((π΄ β π β§ π β π΄) β (π β π΄ β¨ π΄ = β
)) |
88 | 84, 86, 87 | elrabd 3652 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β π΄ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}) |
89 | | elssuni 4903 |
. . . 4
β’ (π΄ β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β π΄ β βͺ {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}) |
90 | 88, 89 | syl 17 |
. . 3
β’ ((π΄ β π β§ π β π΄) β π΄ β βͺ {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}) |
91 | | ssrab2 4042 |
. . . . 5
β’ {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β π« π΄ |
92 | | sspwuni 5065 |
. . . . 5
β’ ({π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β π« π΄ β βͺ {π₯
β π« π΄ β£
(π β π₯ β¨ π₯ = β
)} β π΄) |
93 | 91, 92 | mpbi 229 |
. . . 4
β’ βͺ {π₯
β π« π΄ β£
(π β π₯ β¨ π₯ = β
)} β π΄ |
94 | 93 | a1i 11 |
. . 3
β’ ((π΄ β π β§ π β π΄) β βͺ {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β π΄) |
95 | 90, 94 | eqssd 3966 |
. 2
β’ ((π΄ β π β§ π β π΄) β π΄ = βͺ {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)}) |
96 | | istopon 22277 |
. 2
β’ ({π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β (TopOnβπ΄) β ({π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β Top β§ π΄ = βͺ
{π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)})) |
97 | 81, 95, 96 | sylanbrc 584 |
1
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} β (TopOnβπ΄)) |