Step | Hyp | Ref
| Expression |
1 | | ssexg 5323 |
. . . . . 6
β’ ((π β π½ β§ π½ β Paracomp) β π β V) |
2 | 1 | ancoms 459 |
. . . . 5
β’ ((π½ β Paracomp β§ π β π½) β π β V) |
3 | 2 | 3adant3 1132 |
. . . 4
β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β π β V) |
4 | | simp2 1137 |
. . . 4
β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β π β π½) |
5 | 3, 4 | elpwd 4608 |
. . 3
β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β π β π« π½) |
6 | | ispcmp 32906 |
. . . . . 6
β’ (π½ β Paracomp β π½ β
CovHasRef(LocFinβπ½)) |
7 | | pcmplfin.x |
. . . . . . 7
β’ π = βͺ
π½ |
8 | 7 | iscref 32893 |
. . . . . 6
β’ (π½ β
CovHasRef(LocFinβπ½)
β (π½ β Top β§
βπ’ β π«
π½(π = βͺ π’ β βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ’))) |
9 | 6, 8 | bitri 274 |
. . . . 5
β’ (π½ β Paracomp β (π½ β Top β§ βπ’ β π« π½(π = βͺ π’ β βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ’))) |
10 | 9 | simprbi 497 |
. . . 4
β’ (π½ β Paracomp β
βπ’ β π«
π½(π = βͺ π’ β βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ’)) |
11 | 10 | 3ad2ant1 1133 |
. . 3
β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β βπ’ β π« π½(π = βͺ π’ β βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ’)) |
12 | | simp3 1138 |
. . 3
β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β π = βͺ π) |
13 | | unieq 4919 |
. . . . . 6
β’ (π’ = π β βͺ π’ = βͺ
π) |
14 | 13 | eqeq2d 2743 |
. . . . 5
β’ (π’ = π β (π = βͺ π’ β π = βͺ π)) |
15 | | breq2 5152 |
. . . . . 6
β’ (π’ = π β (π£Refπ’ β π£Refπ)) |
16 | 15 | rexbidv 3178 |
. . . . 5
β’ (π’ = π β (βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ’ β βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ)) |
17 | 14, 16 | imbi12d 344 |
. . . 4
β’ (π’ = π β ((π = βͺ π’ β βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ’) β (π = βͺ π β βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ))) |
18 | 17 | rspcv 3608 |
. . 3
β’ (π β π« π½ β (βπ’ β π« π½(π = βͺ π’ β βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ’) β (π = βͺ π β βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ))) |
19 | 5, 11, 12, 18 | syl3c 66 |
. 2
β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β βπ£ β (π« π½ β© (LocFinβπ½))π£Refπ) |
20 | | rexin 4239 |
. 2
β’
(βπ£ β
(π« π½ β©
(LocFinβπ½))π£Refπ β βπ£ β π« π½(π£ β (LocFinβπ½) β§ π£Refπ)) |
21 | 19, 20 | sylib 217 |
1
β’ ((π½ β Paracomp β§ π β π½ β§ π = βͺ π) β βπ£ β π« π½(π£ β (LocFinβπ½) β§ π£Refπ)) |