Step | Hyp | Ref
| Expression |
1 | | dfsn2 4642 |
. . 3
β’ {β
}
= {β
, β
} |
2 | | indislem 22503 |
. . . . . . 7
β’ {β
,
( I βπ΄)} = {β
,
π΄} |
3 | | preq2 4739 |
. . . . . . . 8
β’ (( I
βπ΄) = β
β
{β
, ( I βπ΄)} =
{β
, β
}) |
4 | 3, 1 | eqtr4di 2791 |
. . . . . . 7
β’ (( I
βπ΄) = β
β
{β
, ( I βπ΄)} =
{β
}) |
5 | 2, 4 | eqtr3id 2787 |
. . . . . 6
β’ (( I
βπ΄) = β
β
{β
, π΄} =
{β
}) |
6 | 5 | breq2d 5161 |
. . . . 5
β’ (( I
βπ΄) = β
β
(π½ β {β
, π΄} β π½ β {β
})) |
7 | 6 | biimpac 480 |
. . . 4
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) = β
) β π½ β
{β
}) |
8 | | hmph0 23299 |
. . . 4
β’ (π½ β {β
} β π½ = {β
}) |
9 | 7, 8 | sylib 217 |
. . 3
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) = β
) β π½ = {β
}) |
10 | 9 | unieqd 4923 |
. . . . 5
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) = β
) β βͺ π½ =
βͺ {β
}) |
11 | | hmphdis.1 |
. . . . 5
β’ π = βͺ
π½ |
12 | | 0ex 5308 |
. . . . . . 7
β’ β
β V |
13 | 12 | unisn 4931 |
. . . . . 6
β’ βͺ {β
} = β
|
14 | 13 | eqcomi 2742 |
. . . . 5
β’ β
=
βͺ {β
} |
15 | 10, 11, 14 | 3eqtr4g 2798 |
. . . 4
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) = β
) β π = β
) |
16 | 15 | preq2d 4745 |
. . 3
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) = β
) β {β
,
π} = {β
,
β
}) |
17 | 1, 9, 16 | 3eqtr4a 2799 |
. 2
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) = β
) β π½ = {β
, π}) |
18 | | hmphen 23289 |
. . . . 5
β’ (π½ β {β
, π΄} β π½ β {β
, π΄}) |
19 | | necom 2995 |
. . . . . . . 8
β’ (( I
βπ΄) β β
β β
β ( I βπ΄)) |
20 | | fvex 6905 |
. . . . . . . . 9
β’ ( I
βπ΄) β
V |
21 | | enpr2 9997 |
. . . . . . . . 9
β’ ((β
β V β§ ( I βπ΄) β V β§ β
β ( I
βπ΄)) β {β
,
( I βπ΄)} β
2o) |
22 | 12, 20, 21 | mp3an12 1452 |
. . . . . . . 8
β’ (β
β ( I βπ΄) β
{β
, ( I βπ΄)}
β 2o) |
23 | 19, 22 | sylbi 216 |
. . . . . . 7
β’ (( I
βπ΄) β β
β {β
, ( I βπ΄)} β 2o) |
24 | 23 | adantl 483 |
. . . . . 6
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) β β
) β {β
,
( I βπ΄)} β
2o) |
25 | 2, 24 | eqbrtrrid 5185 |
. . . . 5
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) β β
) β {β
,
π΄} β
2o) |
26 | | entr 9002 |
. . . . 5
β’ ((π½ β {β
, π΄} β§ {β
, π΄} β 2o) β
π½ β
2o) |
27 | 18, 25, 26 | syl2an2r 684 |
. . . 4
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) β β
) β π½ β
2o) |
28 | | hmphtop1 23283 |
. . . . . . 7
β’ (π½ β {β
, π΄} β π½ β Top) |
29 | 28 | adantr 482 |
. . . . . 6
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) β β
) β π½ β Top) |
30 | 11 | toptopon 22419 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnβπ)) |
31 | 29, 30 | sylib 217 |
. . . . 5
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) β β
) β π½ β (TopOnβπ)) |
32 | | en2top 22488 |
. . . . 5
β’ (π½ β (TopOnβπ) β (π½ β 2o β (π½ = {β
, π} β§ π β β
))) |
33 | 31, 32 | syl 17 |
. . . 4
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) β β
) β (π½ β 2o β
(π½ = {β
, π} β§ π β β
))) |
34 | 27, 33 | mpbid 231 |
. . 3
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) β β
) β (π½ = {β
, π} β§ π β β
)) |
35 | 34 | simpld 496 |
. 2
β’ ((π½ β {β
, π΄} β§ ( I βπ΄) β β
) β π½ = {β
, π}) |
36 | 17, 35 | pm2.61dane 3030 |
1
β’ (π½ β {β
, π΄} β π½ = {β
, π}) |