Step | Hyp | Ref
| Expression |
1 | | ssrab 4035 |
. . . . 5
β’ (π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β π₯ = π΄))) |
2 | | eleq2 2827 |
. . . . . . . 8
β’ (π₯ = βͺ
π¦ β (π β π₯ β π β βͺ π¦)) |
3 | | eqeq1 2741 |
. . . . . . . 8
β’ (π₯ = βͺ
π¦ β (π₯ = π΄ β βͺ π¦ = π΄)) |
4 | 2, 3 | imbi12d 345 |
. . . . . . 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 | | eluni2 4874 |
. . . . . . . . . 10
β’ (π β βͺ π¦
β βπ₯ β
π¦ π β π₯) |
12 | | r19.29 3118 |
. . . . . . . . . . . . 13
β’
((βπ₯ β
π¦ (π β π₯ β π₯ = π΄) β§ βπ₯ β π¦ π β π₯) β βπ₯ β π¦ ((π β π₯ β π₯ = π΄) β§ π β π₯)) |
13 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π¦ β§ (π β π₯ β π₯ = π΄)) β (π β π₯ β π₯ = π΄)) |
14 | 13 | impr 456 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π¦ β§ ((π β π₯ β π₯ = π΄) β§ π β π₯)) β π₯ = π΄) |
15 | | elssuni 4903 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π¦ β π₯ β βͺ π¦) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π¦ β§ ((π β π₯ β π₯ = π΄) β§ π β π₯)) β π₯ β βͺ π¦) |
17 | 14, 16 | eqsstrrd 3988 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π¦ β§ ((π β π₯ β π₯ = π΄) β§ π β π₯)) β π΄ β βͺ π¦) |
18 | 17 | rexlimiva 3145 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
π¦ ((π β π₯ β π₯ = π΄) β§ π β π₯) β π΄ β βͺ π¦) |
19 | 12, 18 | syl 17 |
. . . . . . . . . . . 12
β’
((βπ₯ β
π¦ (π β π₯ β π₯ = π΄) β§ βπ₯ β π¦ π β π₯) β π΄ β βͺ π¦) |
20 | 19 | ex 414 |
. . . . . . . . . . 11
β’
(βπ₯ β
π¦ (π β π₯ β π₯ = π΄) β (βπ₯ β π¦ π β π₯ β π΄ β βͺ π¦)) |
21 | 20 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β π₯ = π΄))) β (βπ₯ β π¦ π β π₯ β π΄ β βͺ π¦)) |
22 | 11, 21 | biimtrid 241 |
. . . . . . . . 9
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β π₯ = π΄))) β (π β βͺ π¦ β π΄ β βͺ π¦)) |
23 | 22, 7 | jctild 527 |
. . . . . . . 8
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β π₯ = π΄))) β (π β βͺ π¦ β (βͺ π¦
β π΄ β§ π΄ β βͺ π¦))) |
24 | | eqss 3964 |
. . . . . . . 8
β’ (βͺ π¦ =
π΄ β (βͺ π¦
β π΄ β§ π΄ β βͺ π¦)) |
25 | 23, 24 | syl6ibr 252 |
. . . . . . 7
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β π₯ = π΄))) β (π β βͺ π¦ β βͺ π¦ =
π΄)) |
26 | 4, 10, 25 | elrabd 3652 |
. . . . . 6
β’ (((π΄ β π β§ π β π΄) β§ (π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β π₯ = π΄))) β βͺ
π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}) |
27 | 26 | ex 414 |
. . . . 5
β’ ((π΄ β π β§ π β π΄) β ((π¦ β π« π΄ β§ βπ₯ β π¦ (π β π₯ β π₯ = π΄)) β βͺ π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)})) |
28 | 1, 27 | biimtrid 241 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β (π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β βͺ π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)})) |
29 | 28 | alrimiv 1931 |
. . 3
β’ ((π΄ β π β§ π β π΄) β βπ¦(π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β βͺ π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)})) |
30 | | inss1 4193 |
. . . . . . . . 9
β’ (π¦ β© π§) β π¦ |
31 | | simprll 778 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) β π¦ β π« π΄) |
32 | 31 | elpwid 4574 |
. . . . . . . . 9
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) β π¦ β π΄) |
33 | 30, 32 | sstrid 3960 |
. . . . . . . 8
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) β (π¦ β© π§) β π΄) |
34 | | vex 3452 |
. . . . . . . . . 10
β’ π¦ β V |
35 | 34 | inex1 5279 |
. . . . . . . . 9
β’ (π¦ β© π§) β V |
36 | 35 | elpw 4569 |
. . . . . . . 8
β’ ((π¦ β© π§) β π« π΄ β (π¦ β© π§) β π΄) |
37 | 33, 36 | sylibr 233 |
. . . . . . 7
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) β (π¦ β© π§) β π« π΄) |
38 | | elin 3931 |
. . . . . . . 8
β’ (π β (π¦ β© π§) β (π β π¦ β§ π β π§)) |
39 | | simprlr 779 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) β (π β π¦ β π¦ = π΄)) |
40 | | simprrr 781 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) β (π β π§ β π§ = π΄)) |
41 | 39, 40 | anim12d 610 |
. . . . . . . . 9
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) β ((π β π¦ β§ π β π§) β (π¦ = π΄ β§ π§ = π΄))) |
42 | | ineq12 4172 |
. . . . . . . . . 10
β’ ((π¦ = π΄ β§ π§ = π΄) β (π¦ β© π§) = (π΄ β© π΄)) |
43 | | inidm 4183 |
. . . . . . . . . 10
β’ (π΄ β© π΄) = π΄ |
44 | 42, 43 | eqtrdi 2793 |
. . . . . . . . 9
β’ ((π¦ = π΄ β§ π§ = π΄) β (π¦ β© π§) = π΄) |
45 | 41, 44 | syl6 35 |
. . . . . . . 8
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) β ((π β π¦ β§ π β π§) β (π¦ β© π§) = π΄)) |
46 | 38, 45 | biimtrid 241 |
. . . . . . 7
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) β (π β (π¦ β© π§) β (π¦ β© π§) = π΄)) |
47 | 37, 46 | jca 513 |
. . . . . 6
β’ (((π΄ β π β§ π β π΄) β§ ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) β ((π¦ β© π§) β π« π΄ β§ (π β (π¦ β© π§) β (π¦ β© π§) = π΄))) |
48 | 47 | ex 414 |
. . . . 5
β’ ((π΄ β π β§ π β π΄) β (((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄))) β ((π¦ β© π§) β π« π΄ β§ (π β (π¦ β© π§) β (π¦ β© π§) = π΄)))) |
49 | | eleq2 2827 |
. . . . . . . 8
β’ (π₯ = π¦ β (π β π₯ β π β π¦)) |
50 | | eqeq1 2741 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯ = π΄ β π¦ = π΄)) |
51 | 49, 50 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = π¦ β ((π β π₯ β π₯ = π΄) β (π β π¦ β π¦ = π΄))) |
52 | 51 | elrab 3650 |
. . . . . 6
β’ (π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β (π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄))) |
53 | | eleq2 2827 |
. . . . . . . 8
β’ (π₯ = π§ β (π β π₯ β π β π§)) |
54 | | eqeq1 2741 |
. . . . . . . 8
β’ (π₯ = π§ β (π₯ = π΄ β π§ = π΄)) |
55 | 53, 54 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = π§ β ((π β π₯ β π₯ = π΄) β (π β π§ β π§ = π΄))) |
56 | 55 | elrab 3650 |
. . . . . 6
β’ (π§ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β (π§ β π« π΄ β§ (π β π§ β π§ = π΄))) |
57 | 52, 56 | anbi12i 628 |
. . . . 5
β’ ((π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β§ π§ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}) β ((π¦ β π« π΄ β§ (π β π¦ β π¦ = π΄)) β§ (π§ β π« π΄ β§ (π β π§ β π§ = π΄)))) |
58 | | eleq2 2827 |
. . . . . . 7
β’ (π₯ = (π¦ β© π§) β (π β π₯ β π β (π¦ β© π§))) |
59 | | eqeq1 2741 |
. . . . . . 7
β’ (π₯ = (π¦ β© π§) β (π₯ = π΄ β (π¦ β© π§) = π΄)) |
60 | 58, 59 | imbi12d 345 |
. . . . . 6
β’ (π₯ = (π¦ β© π§) β ((π β π₯ β π₯ = π΄) β (π β (π¦ β© π§) β (π¦ β© π§) = π΄))) |
61 | 60 | elrab 3650 |
. . . . 5
β’ ((π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β ((π¦ β© π§) β π« π΄ β§ (π β (π¦ β© π§) β (π¦ β© π§) = π΄))) |
62 | 48, 57, 61 | 3imtr4g 296 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β ((π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β§ π§ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}) β (π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)})) |
63 | 62 | ralrimivv 3196 |
. . 3
β’ ((π΄ β π β§ π β π΄) β βπ¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}βπ§ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} (π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}) |
64 | | pwexg 5338 |
. . . . . 6
β’ (π΄ β π β π« π΄ β V) |
65 | 64 | adantr 482 |
. . . . 5
β’ ((π΄ β π β§ π β π΄) β π« π΄ β V) |
66 | | rabexg 5293 |
. . . . 5
β’
(π« π΄ β
V β {π₯ β
π« π΄ β£ (π β π₯ β π₯ = π΄)} β V) |
67 | 65, 66 | syl 17 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β V) |
68 | | istopg 22260 |
. . . 4
β’ ({π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β V β ({π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β Top β (βπ¦(π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β βͺ π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}) β§ βπ¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}βπ§ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} (π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}))) |
69 | 67, 68 | syl 17 |
. . 3
β’ ((π΄ β π β§ π β π΄) β ({π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β Top β (βπ¦(π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β βͺ π¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}) β§ βπ¦ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}βπ§ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} (π¦ β© π§) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}))) |
70 | 29, 63, 69 | mpbir2and 712 |
. 2
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β Top) |
71 | | eleq2 2827 |
. . . . . 6
β’ (π₯ = π΄ β (π β π₯ β π β π΄)) |
72 | | eqeq1 2741 |
. . . . . 6
β’ (π₯ = π΄ β (π₯ = π΄ β π΄ = π΄)) |
73 | 71, 72 | imbi12d 345 |
. . . . 5
β’ (π₯ = π΄ β ((π β π₯ β π₯ = π΄) β (π β π΄ β π΄ = π΄))) |
74 | | pwidg 4585 |
. . . . . 6
β’ (π΄ β π β π΄ β π« π΄) |
75 | 74 | adantr 482 |
. . . . 5
β’ ((π΄ β π β§ π β π΄) β π΄ β π« π΄) |
76 | | eqidd 2738 |
. . . . . 6
β’ ((π΄ β π β§ π β π΄) β π΄ = π΄) |
77 | 76 | a1d 25 |
. . . . 5
β’ ((π΄ β π β§ π β π΄) β (π β π΄ β π΄ = π΄)) |
78 | 73, 75, 77 | elrabd 3652 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β π΄ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}) |
79 | | elssuni 4903 |
. . . 4
β’ (π΄ β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β π΄ β βͺ {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}) |
80 | 78, 79 | syl 17 |
. . 3
β’ ((π΄ β π β§ π β π΄) β π΄ β βͺ {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}) |
81 | | ssrab2 4042 |
. . . . 5
β’ {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β π« π΄ |
82 | | sspwuni 5065 |
. . . . 5
β’ ({π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β π« π΄ β βͺ {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β π΄) |
83 | 81, 82 | mpbi 229 |
. . . 4
β’ βͺ {π₯
β π« π΄ β£
(π β π₯ β π₯ = π΄)} β π΄ |
84 | 83 | a1i 11 |
. . 3
β’ ((π΄ β π β§ π β π΄) β βͺ {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β π΄) |
85 | 80, 84 | eqssd 3966 |
. 2
β’ ((π΄ β π β§ π β π΄) β π΄ = βͺ {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)}) |
86 | | istopon 22277 |
. 2
β’ ({π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β (TopOnβπ΄) β ({π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β Top β§ π΄ = βͺ {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)})) |
87 | 70, 85, 86 | sylanbrc 584 |
1
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β π₯ = π΄)} β (TopOnβπ΄)) |