Step | Hyp | Ref
| Expression |
1 | | elssuni 4941 |
. . . . . 6
β’ (π΄ β π β π΄ β βͺ π) |
2 | 1 | 3ad2ant3 1135 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π΄ β βͺ π) |
3 | 2 | unissd 4918 |
. . . 4
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π΄ β βͺ βͺ π) |
4 | | eqimss2 4041 |
. . . . . . . . . 10
β’ (π = βͺ
π¦ β βͺ π¦
β π) |
5 | | sspwuni 5103 |
. . . . . . . . . 10
β’ (π¦ β π« π β βͺ π¦
β π) |
6 | 4, 5 | sylibr 233 |
. . . . . . . . 9
β’ (π = βͺ
π¦ β π¦ β π« π) |
7 | 6 | ralimi 3083 |
. . . . . . . 8
β’
(βπ¦ β
π π = βͺ π¦ β βπ¦ β π π¦ β π« π) |
8 | 7 | 3ad2ant2 1134 |
. . . . . . 7
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βπ¦ β π π¦ β π« π) |
9 | | unissb 4943 |
. . . . . . 7
β’ (βͺ π
β π« π β
βπ¦ β π π¦ β π« π) |
10 | 8, 9 | sylibr 233 |
. . . . . 6
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π β π« π) |
11 | | sspwuni 5103 |
. . . . . 6
β’ (βͺ π
β π« π β
βͺ βͺ π β π) |
12 | 10, 11 | sylib 217 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ βͺ π
β π) |
13 | | unieq 4919 |
. . . . . . . 8
β’ (π¦ = π΄ β βͺ π¦ = βͺ
π΄) |
14 | 13 | eqeq2d 2743 |
. . . . . . 7
β’ (π¦ = π΄ β (π = βͺ π¦ β π = βͺ π΄)) |
15 | 14 | rspccva 3611 |
. . . . . 6
β’
((βπ¦ β
π π = βͺ π¦ β§ π΄ β π) β π = βͺ π΄) |
16 | 15 | 3adant1 1130 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π = βͺ π΄) |
17 | 12, 16 | sseqtrd 4022 |
. . . 4
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ βͺ π
β βͺ π΄) |
18 | 3, 17 | eqssd 3999 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π΄ = βͺ
βͺ π) |
19 | | pwexg 5376 |
. . . . . . 7
β’ (π β π β π« π β V) |
20 | 19 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π« π β V) |
21 | 20, 10 | ssexd 5324 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π β V) |
22 | | bastg 22468 |
. . . . 5
β’ (βͺ π
β V β βͺ π β (topGenββͺ π)) |
23 | 21, 22 | syl 17 |
. . . 4
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π β (topGenββͺ π)) |
24 | 2, 23 | sstrd 3992 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π΄ β (topGenββͺ π)) |
25 | | eqid 2732 |
. . . 4
β’ βͺ π΄ =
βͺ π΄ |
26 | | eqid 2732 |
. . . 4
β’ βͺ βͺ π = βͺ βͺ π |
27 | 25, 26 | isfne4 35220 |
. . 3
β’ (π΄Fneβͺ
π β (βͺ π΄ =
βͺ βͺ π β§ π΄ β (topGenββͺ π))) |
28 | 18, 24, 27 | sylanbrc 583 |
. 2
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π΄Fneβͺ π) |
29 | | ne0i 4334 |
. . . 4
β’ (π΄ β π β π β β
) |
30 | 29 | 3ad2ant3 1135 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π β β
) |
31 | | ifnefalse 4540 |
. . 3
β’ (π β β
β if(π = β
, {π}, βͺ π) = βͺ
π) |
32 | 30, 31 | syl 17 |
. 2
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β if(π = β
, {π}, βͺ π) = βͺ
π) |
33 | 28, 32 | breqtrrd 5176 |
1
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π΄Fneif(π = β
, {π}, βͺ π)) |