Step | Hyp | Ref
| Expression |
1 | | reconnlem1 24212 |
. . . 4
β’ (((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯[,]π¦) β π΄) |
2 | 1 | ralrimivva 3194 |
. . 3
β’ ((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) |
3 | 2 | ex 414 |
. 2
β’ (π΄ β β β
(((topGenβran (,)) βΎt π΄) β Conn β βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄)) |
4 | | n0 4310 |
. . . . . . . . 9
β’ ((π’ β© π΄) β β
β βπ π β (π’ β© π΄)) |
5 | | n0 4310 |
. . . . . . . . 9
β’ ((π£ β© π΄) β β
β βπ π β (π£ β© π΄)) |
6 | 4, 5 | anbi12i 628 |
. . . . . . . 8
β’ (((π’ β© π΄) β β
β§ (π£ β© π΄) β β
) β (βπ π β (π’ β© π΄) β§ βπ π β (π£ β© π΄))) |
7 | | exdistrv 1960 |
. . . . . . . . 9
β’
(βπβπ(π β (π’ β© π΄) β§ π β (π£ β© π΄)) β (βπ π β (π’ β© π΄) β§ βπ π β (π£ β© π΄))) |
8 | | simplll 774 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β π΄ β β) |
9 | | simprll 778 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β π β (π’ β© π΄)) |
10 | 9 | elin2d 4163 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β π β π΄) |
11 | 8, 10 | sseldd 3949 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β π β β) |
12 | | simprlr 779 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β π β (π£ β© π΄)) |
13 | 12 | elin2d 4163 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β π β π΄) |
14 | 8, 13 | sseldd 3949 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β π β β) |
15 | 8 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π΄ β β) |
16 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β π’ β (topGenβran
(,))) |
17 | 16 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π’ β (topGenβran
(,))) |
18 | | simplrr 777 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β π£ β (topGenβran
(,))) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π£ β (topGenβran
(,))) |
20 | | simpllr 775 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) |
21 | 9 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π β (π’ β© π΄)) |
22 | 12 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π β (π£ β© π΄)) |
23 | | simplrr 777 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β (π’ β© π£) β (β β π΄)) |
24 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π β€ π) |
25 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
sup((π’ β© (π[,]π)), β, < ) = sup((π’ β© (π[,]π)), β, < ) |
26 | 15, 17, 19, 20, 21, 22, 23, 24, 25 | reconnlem2 24213 |
. . . . . . . . . . . 12
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β Β¬ π΄ β (π’ βͺ π£)) |
27 | 8 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π΄ β β) |
28 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π£ β (topGenβran
(,))) |
29 | 16 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π’ β (topGenβran
(,))) |
30 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) |
31 | 12 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π β (π£ β© π΄)) |
32 | 9 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π β (π’ β© π΄)) |
33 | | incom 4165 |
. . . . . . . . . . . . . . 15
β’ (π£ β© π’) = (π’ β© π£) |
34 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β (π’ β© π£) β (β β π΄)) |
35 | 33, 34 | eqsstrid 3996 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β (π£ β© π’) β (β β π΄)) |
36 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β π β€ π) |
37 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
sup((π£ β© (π[,]π)), β, < ) = sup((π£ β© (π[,]π)), β, < ) |
38 | 27, 28, 29, 30, 31, 32, 35, 36, 37 | reconnlem2 24213 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β Β¬ π΄ β (π£ βͺ π’)) |
39 | | uncom 4117 |
. . . . . . . . . . . . . 14
β’ (π£ βͺ π’) = (π’ βͺ π£) |
40 | 39 | sseq2i 3977 |
. . . . . . . . . . . . 13
β’ (π΄ β (π£ βͺ π’) β π΄ β (π’ βͺ π£)) |
41 | 38, 40 | sylnib 328 |
. . . . . . . . . . . 12
β’
(((((π΄ β
β β§ (π’ β
(topGenβran (,)) β§ π£ β (topGenβran (,)))) β§
βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β§ π β€ π) β Β¬ π΄ β (π’ βͺ π£)) |
42 | 11, 14, 26, 41 | lecasei 11269 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β§ ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β§ (π’ β© π£) β (β β π΄))) β Β¬ π΄ β (π’ βͺ π£)) |
43 | 42 | exp32 422 |
. . . . . . . . . 10
β’ (((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β ((π β (π’ β© π΄) β§ π β (π£ β© π΄)) β ((π’ β© π£) β (β β π΄) β Β¬ π΄ β (π’ βͺ π£)))) |
44 | 43 | exlimdvv 1938 |
. . . . . . . . 9
β’ (((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β (βπβπ(π β (π’ β© π΄) β§ π β (π£ β© π΄)) β ((π’ β© π£) β (β β π΄) β Β¬ π΄ β (π’ βͺ π£)))) |
45 | 7, 44 | biimtrrid 242 |
. . . . . . . 8
β’ (((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β ((βπ π β (π’ β© π΄) β§ βπ π β (π£ β© π΄)) β ((π’ β© π£) β (β β π΄) β Β¬ π΄ β (π’ βͺ π£)))) |
46 | 6, 45 | biimtrid 241 |
. . . . . . 7
β’ (((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β (((π’ β© π΄) β β
β§ (π£ β© π΄) β β
) β ((π’ β© π£) β (β β π΄) β Β¬ π΄ β (π’ βͺ π£)))) |
47 | 46 | expd 417 |
. . . . . 6
β’ (((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β ((π’ β© π΄) β β
β ((π£ β© π΄) β β
β ((π’ β© π£) β (β β π΄) β Β¬ π΄ β (π’ βͺ π£))))) |
48 | 47 | 3impd 1349 |
. . . . 5
β’ (((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β§ βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) β (((π’ β© π΄) β β
β§ (π£ β© π΄) β β
β§ (π’ β© π£) β (β β π΄)) β Β¬ π΄ β (π’ βͺ π£))) |
49 | 48 | ex 414 |
. . . 4
β’ ((π΄ β β β§ (π’ β (topGenβran (,))
β§ π£ β
(topGenβran (,)))) β (βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄ β (((π’ β© π΄) β β
β§ (π£ β© π΄) β β
β§ (π’ β© π£) β (β β π΄)) β Β¬ π΄ β (π’ βͺ π£)))) |
50 | 49 | ralrimdvva 3200 |
. . 3
β’ (π΄ β β β
(βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄ β βπ’ β (topGenβran (,))βπ£ β (topGenβran
(,))(((π’ β© π΄) β β
β§ (π£ β© π΄) β β
β§ (π’ β© π£) β (β β π΄)) β Β¬ π΄ β (π’ βͺ π£)))) |
51 | | retopon 24150 |
. . . 4
β’
(topGenβran (,)) β (TopOnββ) |
52 | | connsub 22795 |
. . . 4
β’
(((topGenβran (,)) β (TopOnββ) β§ π΄ β β) β
(((topGenβran (,)) βΎt π΄) β Conn β βπ’ β (topGenβran
(,))βπ£ β
(topGenβran (,))(((π’
β© π΄) β β
β§
(π£ β© π΄) β β
β§ (π’ β© π£) β (β β π΄)) β Β¬ π΄ β (π’ βͺ π£)))) |
53 | 51, 52 | mpan 689 |
. . 3
β’ (π΄ β β β
(((topGenβran (,)) βΎt π΄) β Conn β βπ’ β (topGenβran
(,))βπ£ β
(topGenβran (,))(((π’
β© π΄) β β
β§
(π£ β© π΄) β β
β§ (π’ β© π£) β (β β π΄)) β Β¬ π΄ β (π’ βͺ π£)))) |
54 | 50, 53 | sylibrd 259 |
. 2
β’ (π΄ β β β
(βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄ β ((topGenβran (,))
βΎt π΄)
β Conn)) |
55 | 3, 54 | impbid 211 |
1
β’ (π΄ β β β
(((topGenβran (,)) βΎt π΄) β Conn β βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄)) |