Step | Hyp | Ref
| Expression |
1 | | retop 24141 |
. 2
β’
(topGenβran (,)) β Top |
2 | | tg2 22331 |
. . . 4
β’ ((π₯ β (topGenβran (,))
β§ π¦ β π₯) β βπ§ β ran (,)(π¦ β π§ β§ π§ β π₯)) |
3 | | retopbas 24140 |
. . . . . . . . . 10
β’ ran (,)
β TopBases |
4 | | bastg 22332 |
. . . . . . . . . 10
β’ (ran (,)
β TopBases β ran (,) β (topGenβran (,))) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . 9
β’ ran (,)
β (topGenβran (,)) |
6 | | simprl 770 |
. . . . . . . . 9
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β ran (,)) |
7 | 5, 6 | sselid 3943 |
. . . . . . . 8
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β (topGenβran
(,))) |
8 | | simprrr 781 |
. . . . . . . . 9
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β π₯) |
9 | | velpw 4566 |
. . . . . . . . 9
β’ (π§ β π« π₯ β π§ β π₯) |
10 | 8, 9 | sylibr 233 |
. . . . . . . 8
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β π« π₯) |
11 | 7, 10 | elind 4155 |
. . . . . . 7
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β ((topGenβran (,)) β©
π« π₯)) |
12 | | simprrl 780 |
. . . . . . 7
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π¦ β π§) |
13 | | ioof 13370 |
. . . . . . . . . 10
β’
(,):(β* Γ β*)βΆπ«
β |
14 | | ffn 6669 |
. . . . . . . . . 10
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
15 | | ovelrn 7531 |
. . . . . . . . . 10
β’ ((,) Fn
(β* Γ β*) β (π§ β ran (,) β βπ β β*
βπ β
β* π§ =
(π(,)π))) |
16 | 13, 14, 15 | mp2b 10 |
. . . . . . . . 9
β’ (π§ β ran (,) β
βπ β
β* βπ β β* π§ = (π(,)π)) |
17 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π§ = (π(,)π) β ((topGenβran (,))
βΎt π§) =
((topGenβran (,)) βΎt (π(,)π))) |
18 | | ioosconn 33898 |
. . . . . . . . . . . 12
β’
((topGenβran (,)) βΎt (π(,)π)) β SConn |
19 | 17, 18 | eqeltrdi 2842 |
. . . . . . . . . . 11
β’ (π§ = (π(,)π) β ((topGenβran (,))
βΎt π§)
β SConn) |
20 | 19 | rexlimivw 3145 |
. . . . . . . . . 10
β’
(βπ β
β* π§ =
(π(,)π) β ((topGenβran (,))
βΎt π§)
β SConn) |
21 | 20 | rexlimivw 3145 |
. . . . . . . . 9
β’
(βπ β
β* βπ β β* π§ = (π(,)π) β ((topGenβran (,))
βΎt π§)
β SConn) |
22 | 16, 21 | sylbi 216 |
. . . . . . . 8
β’ (π§ β ran (,) β
((topGenβran (,)) βΎt π§) β SConn) |
23 | 22 | ad2antrl 727 |
. . . . . . 7
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β ((topGenβran (,))
βΎt π§)
β SConn) |
24 | 11, 12, 23 | jca32 517 |
. . . . . 6
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β (π§ β ((topGenβran (,)) β©
π« π₯) β§ (π¦ β π§ β§ ((topGenβran (,))
βΎt π§)
β SConn))) |
25 | 24 | ex 414 |
. . . . 5
β’ ((π₯ β (topGenβran (,))
β§ π¦ β π₯) β ((π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯)) β (π§ β ((topGenβran (,)) β©
π« π₯) β§ (π¦ β π§ β§ ((topGenβran (,))
βΎt π§)
β SConn)))) |
26 | 25 | reximdv2 3158 |
. . . 4
β’ ((π₯ β (topGenβran (,))
β§ π¦ β π₯) β (βπ§ β ran (,)(π¦ β π§ β§ π§ β π₯) β βπ§ β ((topGenβran (,)) β©
π« π₯)(π¦ β π§ β§ ((topGenβran (,))
βΎt π§)
β SConn))) |
27 | 2, 26 | mpd 15 |
. . 3
β’ ((π₯ β (topGenβran (,))
β§ π¦ β π₯) β βπ§ β ((topGenβran (,))
β© π« π₯)(π¦ β π§ β§ ((topGenβran (,))
βΎt π§)
β SConn)) |
28 | 27 | rgen2 3191 |
. 2
β’
βπ₯ β
(topGenβran (,))βπ¦ β π₯ βπ§ β ((topGenβran (,)) β©
π« π₯)(π¦ β π§ β§ ((topGenβran (,))
βΎt π§)
β SConn) |
29 | | islly 22835 |
. 2
β’
((topGenβran (,)) β Locally SConn β ((topGenβran
(,)) β Top β§ βπ₯ β (topGenβran (,))βπ¦ β π₯ βπ§ β ((topGenβran (,)) β©
π« π₯)(π¦ β π§ β§ ((topGenβran (,))
βΎt π§)
β SConn))) |
30 | 1, 28, 29 | mpbir2an 710 |
1
β’
(topGenβran (,)) β Locally SConn |