Step | Hyp | Ref
| Expression |
1 | | simpr3 1006 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄)) β (πΉβπ) β π΄) |
2 | | eleq2 2251 |
. . . 4
β’ (π¦ = π΄ β ((πΉβπ) β π¦ β (πΉβπ) β π΄)) |
3 | | sseq2 3191 |
. . . . . 6
β’ (π¦ = π΄ β ((πΉ β π₯) β π¦ β (πΉ β π₯) β π΄)) |
4 | 3 | anbi2d 464 |
. . . . 5
β’ (π¦ = π΄ β ((π β π₯ β§ (πΉ β π₯) β π¦) β (π β π₯ β§ (πΉ β π₯) β π΄))) |
5 | 4 | rexbidv 2488 |
. . . 4
β’ (π¦ = π΄ β (βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π΄))) |
6 | 2, 5 | imbi12d 234 |
. . 3
β’ (π¦ = π΄ β (((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β ((πΉβπ) β π΄ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π΄)))) |
7 | | simpr1 1004 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄)) β πΉ β ((π½ CnP πΎ)βπ)) |
8 | | iscnp 13970 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))))) |
9 | 8 | adantr 276 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄)) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))))) |
10 | 7, 9 | mpbid 147 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄)) β (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)))) |
11 | 10 | simprd 114 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄)) β βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))) |
12 | | simpr2 1005 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄)) β π΄ β πΎ) |
13 | 6, 11, 12 | rspcdva 2858 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄)) β ((πΉβπ) β π΄ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π΄))) |
14 | 1, 13 | mpd 13 |
1
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄)) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π΄)) |