Step | Hyp | Ref
| Expression |
1 | | elpwi 4608 |
. . . . . . . 8
β’ (π β π« π β π β π) |
2 | 1 | ad2antlr 723 |
. . . . . . 7
β’ (((π β βͺ π½
β§ π β π«
π) β§ π β π) β π β π) |
3 | | simpr 483 |
. . . . . . 7
β’ (((π β βͺ π½
β§ π β π«
π) β§ π β π) β π β π) |
4 | 2, 3 | sseldd 3982 |
. . . . . 6
β’ (((π β βͺ π½
β§ π β π«
π) β§ π β π) β π β π) |
5 | | neiptop.o |
. . . . . . . . . 10
β’ π½ = {π β π« π β£ βπ β π π β (πβπ)} |
6 | 5 | unieqi 4920 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ {π β π« π β£ βπ β π π β (πβπ)} |
7 | 6 | eleq2i 2823 |
. . . . . . . 8
β’ (π β βͺ π½
β π β βͺ {π
β π« π β£
βπ β π π β (πβπ)}) |
8 | | elunirab 4923 |
. . . . . . . 8
β’ (π β βͺ {π
β π« π β£
βπ β π π β (πβπ)} β βπ β π« π(π β π β§ βπ β π π β (πβπ))) |
9 | 7, 8 | bitri 274 |
. . . . . . 7
β’ (π β βͺ π½
β βπ β
π« π(π β π β§ βπ β π π β (πβπ))) |
10 | | simpl 481 |
. . . . . . . 8
β’ ((π β π β§ βπ β π π β (πβπ)) β π β π) |
11 | 10 | reximi 3082 |
. . . . . . 7
β’
(βπ β
π« π(π β π β§ βπ β π π β (πβπ)) β βπ β π« ππ β π) |
12 | 9, 11 | sylbi 216 |
. . . . . 6
β’ (π β βͺ π½
β βπ β
π« ππ β π) |
13 | 4, 12 | r19.29a 3160 |
. . . . 5
β’ (π β βͺ π½
β π β π) |
14 | 13 | a1i 11 |
. . . 4
β’ (π β (π β βͺ π½ β π β π)) |
15 | 14 | ssrdv 3987 |
. . 3
β’ (π β βͺ π½
β π) |
16 | | ssidd 4004 |
. . . 4
β’ (π β π β π) |
17 | | neiptop.5 |
. . . . 5
β’ ((π β§ π β π) β π β (πβπ)) |
18 | 17 | ralrimiva 3144 |
. . . 4
β’ (π β βπ β π π β (πβπ)) |
19 | 5 | neipeltop 22853 |
. . . 4
β’ (π β π½ β (π β π β§ βπ β π π β (πβπ))) |
20 | 16, 18, 19 | sylanbrc 581 |
. . 3
β’ (π β π β π½) |
21 | | unissel 4941 |
. . 3
β’ ((βͺ π½
β π β§ π β π½) β βͺ π½ = π) |
22 | 15, 20, 21 | syl2anc 582 |
. 2
β’ (π β βͺ π½ =
π) |
23 | 22 | eqcomd 2736 |
1
β’ (π β π = βͺ π½) |