Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β π₯ β (topGenβran
(,))) |
2 | | inss1 4189 |
. . . . . 6
β’ (π₯ β© (π΄[,]π΅)) β π₯ |
3 | | simprr 772 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β π¦ β (π₯ β© (π΄[,]π΅))) |
4 | 2, 3 | sselid 3943 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β π¦ β π₯) |
5 | | tg2 22331 |
. . . . 5
β’ ((π₯ β (topGenβran (,))
β§ π¦ β π₯) β βπ§ β ran (,)(π¦ β π§ β§ π§ β π₯)) |
6 | 1, 4, 5 | syl2anc 585 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β βπ§ β ran (,)(π¦ β π§ β§ π§ β π₯)) |
7 | | ioof 13370 |
. . . . . . . 8
β’
(,):(β* Γ β*)βΆπ«
β |
8 | | ffn 6669 |
. . . . . . . 8
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
9 | | ovelrn 7531 |
. . . . . . . 8
β’ ((,) Fn
(β* Γ β*) β (π§ β ran (,) β βπ β β*
βπ β
β* π§ =
(π(,)π))) |
10 | 7, 8, 9 | mp2b 10 |
. . . . . . 7
β’ (π§ β ran (,) β
βπ β
β* βπ β β* π§ = (π(,)π)) |
11 | | inss1 4189 |
. . . . . . . . . . . 12
β’ (π§ β© (π΄[,]π΅)) β π§ |
12 | | simprrr 781 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β π§ β π₯) |
13 | 11, 12 | sstrid 3956 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β (π§ β© (π΄[,]π΅)) β π₯) |
14 | | simprrl 780 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β π¦ β π§) |
15 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β π§ = (π(,)π)) |
16 | 15 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β (π§ β© (π΄[,]π΅)) = ((π(,)π) β© (π΄[,]π΅))) |
17 | 16 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) = ((topGenβran (,))
βΎt ((π(,)π) β© (π΄[,]π΅)))) |
18 | | ioosconn 33898 |
. . . . . . . . . . . . . . . 16
β’
((topGenβran (,)) βΎt (π(,)π)) β SConn |
19 | | ioossre 13331 |
. . . . . . . . . . . . . . . . 17
β’ (π(,)π) β β |
20 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
((topGenβran (,)) βΎt (π(,)π)) = ((topGenβran (,))
βΎt (π(,)π)) |
21 | 20 | resconn 33897 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(,)π) β β β (((topGenβran
(,)) βΎt (π(,)π)) β SConn β ((topGenβran
(,)) βΎt (π(,)π)) β Conn)) |
22 | | reconn 24207 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(,)π) β β β (((topGenβran
(,)) βΎt (π(,)π)) β Conn β βπ’ β (π(,)π)βπ£ β (π(,)π)(π’[,]π£) β (π(,)π))) |
23 | 21, 22 | bitrd 279 |
. . . . . . . . . . . . . . . . 17
β’ ((π(,)π) β β β (((topGenβran
(,)) βΎt (π(,)π)) β SConn β βπ’ β (π(,)π)βπ£ β (π(,)π)(π’[,]π£) β (π(,)π))) |
24 | 19, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(((topGenβran (,)) βΎt (π(,)π)) β SConn β βπ’ β (π(,)π)βπ£ β (π(,)π)(π’[,]π£) β (π(,)π)) |
25 | 18, 24 | mpbi 229 |
. . . . . . . . . . . . . . 15
β’
βπ’ β
(π(,)π)βπ£ β (π(,)π)(π’[,]π£) β (π(,)π) |
26 | | inss1 4189 |
. . . . . . . . . . . . . . . 16
β’ ((π(,)π) β© (π΄[,]π΅)) β (π(,)π) |
27 | | ssralv 4011 |
. . . . . . . . . . . . . . . . . 18
β’ (((π(,)π) β© (π΄[,]π΅)) β (π(,)π) β (βπ£ β (π(,)π)(π’[,]π£) β (π(,)π) β βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π(,)π))) |
28 | 27 | ralimdv 3163 |
. . . . . . . . . . . . . . . . 17
β’ (((π(,)π) β© (π΄[,]π΅)) β (π(,)π) β (βπ’ β (π(,)π)βπ£ β (π(,)π)(π’[,]π£) β (π(,)π) β βπ’ β (π(,)π)βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π(,)π))) |
29 | | ssralv 4011 |
. . . . . . . . . . . . . . . . 17
β’ (((π(,)π) β© (π΄[,]π΅)) β (π(,)π) β (βπ’ β (π(,)π)βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π(,)π) β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π(,)π))) |
30 | 28, 29 | syld 47 |
. . . . . . . . . . . . . . . 16
β’ (((π(,)π) β© (π΄[,]π΅)) β (π(,)π) β (βπ’ β (π(,)π)βπ£ β (π(,)π)(π’[,]π£) β (π(,)π) β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π(,)π))) |
31 | 26, 30 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
(βπ’ β
(π(,)π)βπ£ β (π(,)π)(π’[,]π£) β (π(,)π) β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π(,)π)) |
32 | 25, 31 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π(,)π)) |
33 | | inss2 4190 |
. . . . . . . . . . . . . . 15
β’ ((π(,)π) β© (π΄[,]π΅)) β (π΄[,]π΅) |
34 | | iccconn 24209 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ π΅ β β) β
((topGenβran (,)) βΎt (π΄[,]π΅)) β Conn) |
35 | | iccssre 13352 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
36 | | reconn 24207 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄[,]π΅) β β β (((topGenβran
(,)) βΎt (π΄[,]π΅)) β Conn β βπ’ β (π΄[,]π΅)βπ£ β (π΄[,]π΅)(π’[,]π£) β (π΄[,]π΅))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ π΅ β β) β
(((topGenβran (,)) βΎt (π΄[,]π΅)) β Conn β βπ’ β (π΄[,]π΅)βπ£ β (π΄[,]π΅)(π’[,]π£) β (π΄[,]π΅))) |
38 | 34, 37 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§ π΅ β β) β
βπ’ β (π΄[,]π΅)βπ£ β (π΄[,]π΅)(π’[,]π£) β (π΄[,]π΅)) |
39 | 38 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β βπ’ β (π΄[,]π΅)βπ£ β (π΄[,]π΅)(π’[,]π£) β (π΄[,]π΅)) |
40 | | ssralv 4011 |
. . . . . . . . . . . . . . . . 17
β’ (((π(,)π) β© (π΄[,]π΅)) β (π΄[,]π΅) β (βπ£ β (π΄[,]π΅)(π’[,]π£) β (π΄[,]π΅) β βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π΄[,]π΅))) |
41 | 40 | ralimdv 3163 |
. . . . . . . . . . . . . . . 16
β’ (((π(,)π) β© (π΄[,]π΅)) β (π΄[,]π΅) β (βπ’ β (π΄[,]π΅)βπ£ β (π΄[,]π΅)(π’[,]π£) β (π΄[,]π΅) β βπ’ β (π΄[,]π΅)βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π΄[,]π΅))) |
42 | | ssralv 4011 |
. . . . . . . . . . . . . . . 16
β’ (((π(,)π) β© (π΄[,]π΅)) β (π΄[,]π΅) β (βπ’ β (π΄[,]π΅)βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π΄[,]π΅) β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π΄[,]π΅))) |
43 | 41, 42 | syld 47 |
. . . . . . . . . . . . . . 15
β’ (((π(,)π) β© (π΄[,]π΅)) β (π΄[,]π΅) β (βπ’ β (π΄[,]π΅)βπ£ β (π΄[,]π΅)(π’[,]π£) β (π΄[,]π΅) β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π΄[,]π΅))) |
44 | 33, 39, 43 | mpsyl 68 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π΄[,]π΅)) |
45 | | ssin 4191 |
. . . . . . . . . . . . . . . 16
β’ (((π’[,]π£) β (π(,)π) β§ (π’[,]π£) β (π΄[,]π΅)) β (π’[,]π£) β ((π(,)π) β© (π΄[,]π΅))) |
46 | 45 | 2ralbii 3124 |
. . . . . . . . . . . . . . 15
β’
(βπ’ β
((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))((π’[,]π£) β (π(,)π) β§ (π’[,]π£) β (π΄[,]π΅)) β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β ((π(,)π) β© (π΄[,]π΅))) |
47 | | r19.26-2 3132 |
. . . . . . . . . . . . . . 15
β’
(βπ’ β
((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))((π’[,]π£) β (π(,)π) β§ (π’[,]π£) β (π΄[,]π΅)) β (βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π(,)π) β§ βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π΄[,]π΅))) |
48 | 46, 47 | bitr3i 277 |
. . . . . . . . . . . . . 14
β’
(βπ’ β
((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β ((π(,)π) β© (π΄[,]π΅)) β (βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π(,)π) β§ βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β (π΄[,]π΅))) |
49 | 32, 44, 48 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β ((π(,)π) β© (π΄[,]π΅))) |
50 | 26, 19 | sstri 3954 |
. . . . . . . . . . . . . 14
β’ ((π(,)π) β© (π΄[,]π΅)) β β |
51 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
((topGenβran (,)) βΎt ((π(,)π) β© (π΄[,]π΅))) = ((topGenβran (,))
βΎt ((π(,)π) β© (π΄[,]π΅))) |
52 | 51 | resconn 33897 |
. . . . . . . . . . . . . . 15
β’ (((π(,)π) β© (π΄[,]π΅)) β β β
(((topGenβran (,)) βΎt ((π(,)π) β© (π΄[,]π΅))) β SConn β ((topGenβran
(,)) βΎt ((π(,)π) β© (π΄[,]π΅))) β Conn)) |
53 | | reconn 24207 |
. . . . . . . . . . . . . . 15
β’ (((π(,)π) β© (π΄[,]π΅)) β β β
(((topGenβran (,)) βΎt ((π(,)π) β© (π΄[,]π΅))) β Conn β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β ((π(,)π) β© (π΄[,]π΅)))) |
54 | 52, 53 | bitrd 279 |
. . . . . . . . . . . . . 14
β’ (((π(,)π) β© (π΄[,]π΅)) β β β
(((topGenβran (,)) βΎt ((π(,)π) β© (π΄[,]π΅))) β SConn β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β ((π(,)π) β© (π΄[,]π΅)))) |
55 | 50, 54 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(((topGenβran (,)) βΎt ((π(,)π) β© (π΄[,]π΅))) β SConn β βπ’ β ((π(,)π) β© (π΄[,]π΅))βπ£ β ((π(,)π) β© (π΄[,]π΅))(π’[,]π£) β ((π(,)π) β© (π΄[,]π΅))) |
56 | 49, 55 | sylibr 233 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β ((topGenβran (,))
βΎt ((π(,)π) β© (π΄[,]π΅))) β SConn) |
57 | 17, 56 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn) |
58 | 13, 14, 57 | 3jca 1129 |
. . . . . . . . . 10
β’ ((((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β§ (π§ = (π(,)π) β§ (π¦ β π§ β§ π§ β π₯))) β ((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn)) |
59 | 58 | exp32 422 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β (π§ = (π(,)π) β ((π¦ β π§ β§ π§ β π₯) β ((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn)))) |
60 | 59 | rexlimdvw 3154 |
. . . . . . . 8
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β (βπ β β* π§ = (π(,)π) β ((π¦ β π§ β§ π§ β π₯) β ((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn)))) |
61 | 60 | rexlimdvw 3154 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β (βπ β β* βπ β β*
π§ = (π(,)π) β ((π¦ β π§ β§ π§ β π₯) β ((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn)))) |
62 | 10, 61 | biimtrid 241 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β (π§ β ran (,) β ((π¦ β π§ β§ π§ β π₯) β ((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn)))) |
63 | 62 | reximdvai 3159 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β (βπ§ β ran (,)(π¦ β π§ β§ π§ β π₯) β βπ§ β ran (,)((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn))) |
64 | | retopbas 24140 |
. . . . . 6
β’ ran (,)
β TopBases |
65 | | bastg 22332 |
. . . . . 6
β’ (ran (,)
β TopBases β ran (,) β (topGenβran (,))) |
66 | | ssrexv 4012 |
. . . . . 6
β’ (ran (,)
β (topGenβran (,)) β (βπ§ β ran (,)((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β SConn) β
βπ§ β
(topGenβran (,))((π§
β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn))) |
67 | 64, 65, 66 | mp2b 10 |
. . . . 5
β’
(βπ§ β ran
(,)((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β SConn) β
βπ§ β
(topGenβran (,))((π§
β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn)) |
68 | 63, 67 | syl6 35 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β (βπ§ β ran (,)(π¦ β π§ β§ π§ β π₯) β βπ§ β (topGenβran (,))((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn))) |
69 | 6, 68 | mpd 15 |
. . 3
β’ (((π΄ β β β§ π΅ β β) β§ (π₯ β (topGenβran (,))
β§ π¦ β (π₯ β© (π΄[,]π΅)))) β βπ§ β (topGenβran (,))((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn)) |
70 | 69 | ralrimivva 3194 |
. 2
β’ ((π΄ β β β§ π΅ β β) β
βπ₯ β
(topGenβran (,))βπ¦ β (π₯ β© (π΄[,]π΅))βπ§ β (topGenβran (,))((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn)) |
71 | | retop 24141 |
. . 3
β’
(topGenβran (,)) β Top |
72 | | ovex 7391 |
. . 3
β’ (π΄[,]π΅) β V |
73 | | subislly 22848 |
. . 3
β’
(((topGenβran (,)) β Top β§ (π΄[,]π΅) β V) β (((topGenβran (,))
βΎt (π΄[,]π΅)) β Locally SConn β βπ₯ β (topGenβran
(,))βπ¦ β (π₯ β© (π΄[,]π΅))βπ§ β (topGenβran (,))((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn))) |
74 | 71, 72, 73 | mp2an 691 |
. 2
β’
(((topGenβran (,)) βΎt (π΄[,]π΅)) β Locally SConn β βπ₯ β (topGenβran
(,))βπ¦ β (π₯ β© (π΄[,]π΅))βπ§ β (topGenβran (,))((π§ β© (π΄[,]π΅)) β π₯ β§ π¦ β π§ β§ ((topGenβran (,))
βΎt (π§
β© (π΄[,]π΅))) β
SConn)) |
75 | 70, 74 | sylibr 233 |
1
β’ ((π΄ β β β§ π΅ β β) β
((topGenβran (,)) βΎt (π΄[,]π΅)) β Locally SConn) |