| Step | Hyp | Ref
| Expression |
|---|
| 1 | | retop 24694 |
. 2
β’
(topGenβran (,)) β Top |
| 2 | | tg2 22884 |
. . . 4
β’ ((π₯ β (topGenβran (,))
β§ π¦ β π₯) β βπ§ β ran (,)(π¦ β π§ β§ π§ β π₯)) |
| 3 | | retopbas 24693 |
. . . . . . . . . 10
β’ ran (,)
β TopBases |
| 4 | | bastg 22885 |
. . . . . . . . . 10
β’ (ran (,)
β TopBases β ran (,) β (topGenβran (,))) |
| 5 | 3, 4 | ax-mp 5 |
. . . . . . . . 9
β’ ran (,)
β (topGenβran (,)) |
| 6 | | simprl 769 |
. . . . . . . . 9
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β ran (,)) |
| 7 | 5, 6 | sselid 3970 |
. . . . . . . 8
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β (topGenβran
(,))) |
| 8 | | simprrr 780 |
. . . . . . . . 9
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β π₯) |
| 9 | | velpw 4603 |
. . . . . . . . 9
β’ (π§ β π« π₯ β π§ β π₯) |
| 10 | 8, 9 | sylibr 233 |
. . . . . . . 8
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β π« π₯) |
| 11 | 7, 10 | elind 4188 |
. . . . . . 7
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β ((topGenβran (,)) β©
π« π₯)) |
| 12 | | simprrl 779 |
. . . . . . 7
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β π¦ β π§) |
| 13 | | ioof 13454 |
. . . . . . . . . 10
β’
(,):(β* Γ β*)βΆπ«
β |
| 14 | | ffn 6716 |
. . . . . . . . . 10
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
| 15 | | ovelrn 7593 |
. . . . . . . . . 10
β’ ((,) Fn
(β* Γ β*) β (π§ β ran (,) β βπ β β*
βπ β
β* π§ =
(π(,)π))) |
| 16 | 13, 14, 15 | mp2b 10 |
. . . . . . . . 9
β’ (π§ β ran (,) β
βπ β
β* βπ β β* π§ = (π(,)π)) |
| 17 | | oveq2 7423 |
. . . . . . . . . . . 12
β’ (π§ = (π(,)π) β ((topGenβran (,))
βΎt π§) =
((topGenβran (,)) βΎt (π(,)π))) |
| 18 | | ioosconn 34913 |
. . . . . . . . . . . 12
β’
((topGenβran (,)) βΎt (π(,)π)) β SConn |
| 19 | 17, 18 | eqeltrdi 2833 |
. . . . . . . . . . 11
β’ (π§ = (π(,)π) β ((topGenβran (,))
βΎt π§)
β SConn) |
| 20 | 19 | rexlimivw 3141 |
. . . . . . . . . 10
β’
(βπ β
β* π§ =
(π(,)π) β ((topGenβran (,))
βΎt π§)
β SConn) |
| 21 | 20 | rexlimivw 3141 |
. . . . . . . . 9
β’
(βπ β
β* βπ β β* π§ = (π(,)π) β ((topGenβran (,))
βΎt π§)
β SConn) |
| 22 | 16, 21 | sylbi 216 |
. . . . . . . 8
β’ (π§ β ran (,) β
((topGenβran (,)) βΎt π§) β SConn) |
| 23 | 22 | ad2antrl 726 |
. . . . . . 7
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β ((topGenβran (,))
βΎt π§)
β SConn) |
| 24 | 11, 12, 23 | jca32 514 |
. . . . . 6
β’ (((π₯ β (topGenβran (,))
β§ π¦ β π₯) β§ (π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯))) β (π§ β ((topGenβran (,)) β©
π« π₯) β§ (π¦ β π§ β§ ((topGenβran (,))
βΎt π§)
β SConn))) |
| 25 | 24 | ex 411 |
. . . . 5
β’ ((π₯ β (topGenβran (,))
β§ π¦ β π₯) β ((π§ β ran (,) β§ (π¦ β π§ β§ π§ β π₯)) β (π§ β ((topGenβran (,)) β©
π« π₯) β§ (π¦ β π§ β§ ((topGenβran (,))
βΎt π§)
β SConn)))) |
| 26 | 25 | reximdv2 3154 |
. . . 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 3188 |
. 2
β’
βπ₯ β
(topGenβran (,))βπ¦ β π₯ βπ§ β ((topGenβran (,)) β©
π« π₯)(π¦ β π§ β§ ((topGenβran (,))
βΎt π§)
β SConn) |
| 29 | | islly 23388 |
. 2
β’
((topGenβran (,)) β Locally SConn β ((topGenβran
(,)) β Top β§ βπ₯ β (topGenβran (,))βπ¦ β π₯ βπ§ β ((topGenβran (,)) β©
π« π₯)(π¦ β π§ β§ ((topGenβran (,))
βΎt π§)
β SConn))) |
| 30 | 1, 28, 29 | mpbir2an 709 |
1
β’
(topGenβran (,)) β Locally SConn |
