Step | Hyp | Ref
| Expression |
1 | | elpwi 4609 |
. . . . . . . 8
β’ (π β π« π β π β π) |
2 | 1 | ad2antlr 724 |
. . . . . . 7
β’ (((π β βͺ π½
β§ π β π«
π) β§ π β π) β π β π) |
3 | | simpr 484 |
. . . . . . 7
β’ (((π β βͺ π½
β§ π β π«
π) β§ π β π) β π β π) |
4 | 2, 3 | sseldd 3983 |
. . . . . 6
β’ (((π β βͺ π½
β§ π β π«
π) β§ π β π) β π β π) |
5 | | neiptop.o |
. . . . . . . . . 10
β’ π½ = {π β π« π β£ βπ β π π β (πβπ)} |
6 | 5 | unieqi 4921 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ {π β π« π β£ βπ β π π β (πβπ)} |
7 | 6 | eleq2i 2824 |
. . . . . . . 8
β’ (π β βͺ π½
β π β βͺ {π
β π« π β£
βπ β π π β (πβπ)}) |
8 | | elunirab 4924 |
. . . . . . . 8
β’ (π β βͺ {π
β π« π β£
βπ β π π β (πβπ)} β βπ β π« π(π β π β§ βπ β π π β (πβπ))) |
9 | 7, 8 | bitri 275 |
. . . . . . 7
β’ (π β βͺ π½
β βπ β
π« π(π β π β§ βπ β π π β (πβπ))) |
10 | | simpl 482 |
. . . . . . . 8
β’ ((π β π β§ βπ β π π β (πβπ)) β π β π) |
11 | 10 | reximi 3083 |
. . . . . . 7
β’
(βπ β
π« π(π β π β§ βπ β π π β (πβπ)) β βπ β π« ππ β π) |
12 | 9, 11 | sylbi 216 |
. . . . . 6
β’ (π β βͺ π½
β βπ β
π« ππ β π) |
13 | 4, 12 | r19.29a 3161 |
. . . . 5
β’ (π β βͺ π½
β π β π) |
14 | 13 | a1i 11 |
. . . 4
β’ (π β (π β βͺ π½ β π β π)) |
15 | 14 | ssrdv 3988 |
. . 3
β’ (π β βͺ π½
β π) |
16 | | ssidd 4005 |
. . . 4
β’ (π β π β π) |
17 | | neiptop.5 |
. . . . 5
β’ ((π β§ π β π) β π β (πβπ)) |
18 | 17 | ralrimiva 3145 |
. . . 4
β’ (π β βπ β π π β (πβπ)) |
19 | 5 | neipeltop 22854 |
. . . 4
β’ (π β π½ β (π β π β§ βπ β π π β (πβπ))) |
20 | 16, 18, 19 | sylanbrc 582 |
. . 3
β’ (π β π β π½) |
21 | | unissel 4942 |
. . 3
β’ ((βͺ π½
β π β§ π β π½) β βͺ π½ = π) |
22 | 15, 20, 21 | syl2anc 583 |
. 2
β’ (π β βͺ π½ =
π) |
23 | 22 | eqcomd 2737 |
1
β’ (π β π = βͺ π½) |