Step | Hyp | Ref
| Expression |
1 | | orvcgteel.1 |
. 2
β’ (π β π β Prob) |
2 | | orvcgteel.2 |
. 2
β’ (π β π β (rRndVarβπ)) |
3 | | orvcgteel.3 |
. 2
β’ (π β π΄ β β) |
4 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β π₯ β β) |
5 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β π΄ β β) |
6 | | brcnvg 5836 |
. . . . . . . 8
β’ ((π₯ β β β§ π΄ β β) β (π₯β‘ β€ π΄ β π΄ β€ π₯)) |
7 | 4, 5, 6 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (π₯β‘
β€ π΄ β π΄ β€ π₯)) |
8 | 7 | pm5.32da 580 |
. . . . . 6
β’ (π β ((π₯ β β β§ π₯β‘
β€ π΄) β (π₯ β β β§ π΄ β€ π₯))) |
9 | | rexr 11206 |
. . . . . . . . 9
β’ (π₯ β β β π₯ β
β*) |
10 | 9 | ad2antrl 727 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ π΄ β€ π₯)) β π₯ β β*) |
11 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ π΄ β€ π₯)) β π΄ β€ π₯) |
12 | | ltpnf 13046 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ < +β) |
13 | 12 | ad2antrl 727 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ π΄ β€ π₯)) β π₯ < +β) |
14 | 11, 13 | jca 513 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ π΄ β€ π₯)) β (π΄ β€ π₯ β§ π₯ < +β)) |
15 | 10, 14 | jca 513 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ π΄ β€ π₯)) β (π₯ β β* β§ (π΄ β€ π₯ β§ π₯ < +β))) |
16 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β* β§ (π΄ β€ π₯ β§ π₯ < +β))) β π₯ β β*) |
17 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β* β§ (π΄ β€ π₯ β§ π₯ < +β))) β π΄ β β) |
18 | | simprrl 780 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β* β§ (π΄ β€ π₯ β§ π₯ < +β))) β π΄ β€ π₯) |
19 | | simprrr 781 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β* β§ (π΄ β€ π₯ β§ π₯ < +β))) β π₯ < +β) |
20 | | xrre3 13096 |
. . . . . . . . 9
β’ (((π₯ β β*
β§ π΄ β β)
β§ (π΄ β€ π₯ β§ π₯ < +β)) β π₯ β β) |
21 | 16, 17, 18, 19, 20 | syl22anc 838 |
. . . . . . . 8
β’ ((π β§ (π₯ β β* β§ (π΄ β€ π₯ β§ π₯ < +β))) β π₯ β β) |
22 | 21, 18 | jca 513 |
. . . . . . 7
β’ ((π β§ (π₯ β β* β§ (π΄ β€ π₯ β§ π₯ < +β))) β (π₯ β β β§ π΄ β€ π₯)) |
23 | 15, 22 | impbida 800 |
. . . . . 6
β’ (π β ((π₯ β β β§ π΄ β€ π₯) β (π₯ β β* β§ (π΄ β€ π₯ β§ π₯ < +β)))) |
24 | 8, 23 | bitrd 279 |
. . . . 5
β’ (π β ((π₯ β β β§ π₯β‘
β€ π΄) β (π₯ β β*
β§ (π΄ β€ π₯ β§ π₯ < +β)))) |
25 | 24 | rabbidva2 3408 |
. . . 4
β’ (π β {π₯ β β β£ π₯β‘
β€ π΄} = {π₯ β β*
β£ (π΄ β€ π₯ β§ π₯ < +β)}) |
26 | 3 | rexrd 11210 |
. . . . 5
β’ (π β π΄ β
β*) |
27 | | pnfxr 11214 |
. . . . 5
β’ +β
β β* |
28 | | icoval 13308 |
. . . . 5
β’ ((π΄ β β*
β§ +β β β*) β (π΄[,)+β) = {π₯ β β* β£ (π΄ β€ π₯ β§ π₯ < +β)}) |
29 | 26, 27, 28 | sylancl 587 |
. . . 4
β’ (π β (π΄[,)+β) = {π₯ β β* β£ (π΄ β€ π₯ β§ π₯ < +β)}) |
30 | 25, 29 | eqtr4d 2776 |
. . 3
β’ (π β {π₯ β β β£ π₯β‘
β€ π΄} = (π΄[,)+β)) |
31 | | icopnfcld 24147 |
. . . 4
β’ (π΄ β β β (π΄[,)+β) β
(Clsdβ(topGenβran (,)))) |
32 | 3, 31 | syl 17 |
. . 3
β’ (π β (π΄[,)+β) β
(Clsdβ(topGenβran (,)))) |
33 | 30, 32 | eqeltrd 2834 |
. 2
β’ (π β {π₯ β β β£ π₯β‘
β€ π΄} β
(Clsdβ(topGenβran (,)))) |
34 | 1, 2, 3, 33 | orrvccel 33123 |
1
β’ (π β (πβRV/πβ‘ β€ π΄) β dom π) |