Step | Hyp | Ref
| Expression |
1 | | 1stccn.7 |
. . 3
β’ (π β πΉ:πβΆπ) |
2 | | 1stccnp.2 |
. . . 4
β’ (π β π½ β (TopOnβπ)) |
3 | | 1stccnp.3 |
. . . 4
β’ (π β πΎ β (TopOnβπ)) |
4 | | cncnp 22654 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)))) |
5 | 2, 3, 4 | syl2anc 585 |
. . 3
β’ (π β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)))) |
6 | 1, 5 | mpbirand 706 |
. 2
β’ (π β (πΉ β (π½ Cn πΎ) β βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯))) |
7 | 1 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π) β πΉ:πβΆπ) |
8 | | 1stccnp.1 |
. . . . . 6
β’ (π β π½ β
1stΟ) |
9 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β π½ β
1stΟ) |
10 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β π½ β (TopOnβπ)) |
11 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β πΎ β (TopOnβπ)) |
12 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β π) β π₯ β π) |
13 | 9, 10, 11, 12 | 1stccnp 22836 |
. . . 4
β’ ((π β§ π₯ β π) β (πΉ β ((π½ CnP πΎ)βπ₯) β (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))))) |
14 | 7, 13 | mpbirand 706 |
. . 3
β’ ((π β§ π₯ β π) β (πΉ β ((π½ CnP πΎ)βπ₯) β βπ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
15 | 14 | ralbidva 3169 |
. 2
β’ (π β (βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯) β βπ₯ β π βπ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
16 | | ralcom4 3268 |
. . 3
β’
(βπ₯ β
π βπ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β βπβπ₯ β π ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))) |
17 | | impexp 452 |
. . . . . . 7
β’ (((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β (π:ββΆπ β (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
18 | 17 | ralbii 3093 |
. . . . . 6
β’
(βπ₯ β
π ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β βπ₯ β π (π:ββΆπ β (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
19 | | r19.21v 3173 |
. . . . . 6
β’
(βπ₯ β
π (π:ββΆπ β (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))) β (π:ββΆπ β βπ₯ β π (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
20 | 18, 19 | bitri 275 |
. . . . 5
β’
(βπ₯ β
π ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β (π:ββΆπ β βπ₯ β π (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
21 | | df-ral 3062 |
. . . . . . 7
β’
(βπ₯ β
π (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β βπ₯(π₯ β π β (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
22 | | lmcl 22671 |
. . . . . . . . . . . . 13
β’ ((π½ β (TopOnβπ) β§ π(βπ‘βπ½)π₯) β π₯ β π) |
23 | 2, 22 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β§ π(βπ‘βπ½)π₯) β π₯ β π) |
24 | 23 | ex 414 |
. . . . . . . . . . 11
β’ (π β (π(βπ‘βπ½)π₯ β π₯ β π)) |
25 | 24 | pm4.71rd 564 |
. . . . . . . . . 10
β’ (π β (π(βπ‘βπ½)π₯ β (π₯ β π β§ π(βπ‘βπ½)π₯))) |
26 | 25 | imbi1d 342 |
. . . . . . . . 9
β’ (π β ((π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β ((π₯ β π β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
27 | | impexp 452 |
. . . . . . . . 9
β’ (((π₯ β π β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β (π₯ β π β (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
28 | 26, 27 | bitr2di 288 |
. . . . . . . 8
β’ (π β ((π₯ β π β (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))) β (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
29 | 28 | albidv 1924 |
. . . . . . 7
β’ (π β (βπ₯(π₯ β π β (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))) β βπ₯(π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
30 | 21, 29 | bitrid 283 |
. . . . . 6
β’ (π β (βπ₯ β π (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β βπ₯(π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)))) |
31 | 30 | imbi2d 341 |
. . . . 5
β’ (π β ((π:ββΆπ β βπ₯ β π (π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))) β (π:ββΆπ β βπ₯(π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))))) |
32 | 20, 31 | bitrid 283 |
. . . 4
β’ (π β (βπ₯ β π ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β (π:ββΆπ β βπ₯(π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))))) |
33 | 32 | albidv 1924 |
. . 3
β’ (π β (βπβπ₯ β π ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β βπ(π:ββΆπ β βπ₯(π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))))) |
34 | 16, 33 | bitrid 283 |
. 2
β’ (π β (βπ₯ β π βπ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯)) β βπ(π:ββΆπ β βπ₯(π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))))) |
35 | 6, 15, 34 | 3bitrd 305 |
1
β’ (π β (πΉ β (π½ Cn πΎ) β βπ(π:ββΆπ β βπ₯(π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))))) |