Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . 4
β’ (((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β ((topGenβran (,))
βΎt π΄)
β Conn) |
2 | | retopon 24150 |
. . . . . . 7
β’
(topGenβran (,)) β (TopOnββ) |
3 | 2 | a1i 11 |
. . . . . 6
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (topGenβran (,)) β
(TopOnββ)) |
4 | | simplll 774 |
. . . . . 6
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π΄ β β) |
5 | | iooretop 24152 |
. . . . . . 7
β’
(-β(,)π§)
β (topGenβran (,)) |
6 | 5 | a1i 11 |
. . . . . 6
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (-β(,)π§) β (topGenβran
(,))) |
7 | | iooretop 24152 |
. . . . . . 7
β’ (π§(,)+β) β
(topGenβran (,)) |
8 | 7 | a1i 11 |
. . . . . 6
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π§(,)+β) β (topGenβran
(,))) |
9 | | simplrl 776 |
. . . . . . . . 9
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π β π΄) |
10 | 4, 9 | sseldd 3949 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π β β) |
11 | 10 | mnfltd 13053 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β -β < π) |
12 | | eldifn 4091 |
. . . . . . . . . . 11
β’ (π§ β ((π[,]π) β π΄) β Β¬ π§ β π΄) |
13 | 12 | adantl 483 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β Β¬ π§ β π΄) |
14 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π = π§ β (π β π΄ β π§ β π΄)) |
15 | 9, 14 | syl5ibcom 244 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π = π§ β π§ β π΄)) |
16 | 13, 15 | mtod 197 |
. . . . . . . . 9
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β Β¬ π = π§) |
17 | | eldifi 4090 |
. . . . . . . . . . . . . 14
β’ (π§ β ((π[,]π) β π΄) β π§ β (π[,]π)) |
18 | 17 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π§ β (π[,]π)) |
19 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π β π΄) |
20 | 4, 19 | sseldd 3949 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π β β) |
21 | | elicc2 13338 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β) β (π§ β (π[,]π) β (π§ β β β§ π β€ π§ β§ π§ β€ π))) |
22 | 10, 20, 21 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π§ β (π[,]π) β (π§ β β β§ π β€ π§ β§ π§ β€ π))) |
23 | 18, 22 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π§ β β β§ π β€ π§ β§ π§ β€ π)) |
24 | 23 | simp2d 1144 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π β€ π§) |
25 | 23 | simp1d 1143 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π§ β β) |
26 | 10, 25 | leloed 11306 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π β€ π§ β (π < π§ β¨ π = π§))) |
27 | 24, 26 | mpbid 231 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π < π§ β¨ π = π§)) |
28 | 27 | ord 863 |
. . . . . . . . 9
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (Β¬ π < π§ β π = π§)) |
29 | 16, 28 | mt3d 148 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π < π§) |
30 | | mnfxr 11220 |
. . . . . . . . 9
β’ -β
β β* |
31 | 25 | rexrd 11213 |
. . . . . . . . 9
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π§ β β*) |
32 | | elioo2 13314 |
. . . . . . . . 9
β’
((-β β β* β§ π§ β β*) β (π β (-β(,)π§) β (π β β β§ -β < π β§ π < π§))) |
33 | 30, 31, 32 | sylancr 588 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π β (-β(,)π§) β (π β β β§ -β < π β§ π < π§))) |
34 | 10, 11, 29, 33 | mpbir3and 1343 |
. . . . . . 7
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π β (-β(,)π§)) |
35 | | inelcm 4428 |
. . . . . . 7
β’ ((π β (-β(,)π§) β§ π β π΄) β ((-β(,)π§) β© π΄) β β
) |
36 | 34, 9, 35 | syl2anc 585 |
. . . . . 6
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β ((-β(,)π§) β© π΄) β β
) |
37 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π§ = π β (π§ β π΄ β π β π΄)) |
38 | 19, 37 | syl5ibrcom 247 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π§ = π β π§ β π΄)) |
39 | 13, 38 | mtod 197 |
. . . . . . . . 9
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β Β¬ π§ = π) |
40 | 23 | simp3d 1145 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π§ β€ π) |
41 | 25, 20 | leloed 11306 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π§ β€ π β (π§ < π β¨ π§ = π))) |
42 | 40, 41 | mpbid 231 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π§ < π β¨ π§ = π)) |
43 | 42 | ord 863 |
. . . . . . . . 9
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (Β¬ π§ < π β π§ = π)) |
44 | 39, 43 | mt3d 148 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π§ < π) |
45 | 20 | ltpnfd 13050 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π < +β) |
46 | | pnfxr 11217 |
. . . . . . . . 9
β’ +β
β β* |
47 | | elioo2 13314 |
. . . . . . . . 9
β’ ((π§ β β*
β§ +β β β*) β (π β (π§(,)+β) β (π β β β§ π§ < π β§ π < +β))) |
48 | 31, 46, 47 | sylancl 587 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π β (π§(,)+β) β (π β β β§ π§ < π β§ π < +β))) |
49 | 20, 44, 45, 48 | mpbir3and 1343 |
. . . . . . 7
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π β (π§(,)+β)) |
50 | | inelcm 4428 |
. . . . . . 7
β’ ((π β (π§(,)+β) β§ π β π΄) β ((π§(,)+β) β© π΄) β β
) |
51 | 49, 19, 50 | syl2anc 585 |
. . . . . 6
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β ((π§(,)+β) β© π΄) β β
) |
52 | | inss1 4192 |
. . . . . . 7
β’
(((-β(,)π§)
β© (π§(,)+β)) β©
π΄) β
((-β(,)π§) β©
(π§(,)+β)) |
53 | 31, 30 | jctil 521 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (-β β
β* β§ π§
β β*)) |
54 | 31, 46 | jctir 522 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π§ β β* β§ +β
β β*)) |
55 | 25 | leidd 11729 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π§ β€ π§) |
56 | | ioodisj 13408 |
. . . . . . . 8
β’
((((-β β β* β§ π§ β β*) β§ (π§ β β*
β§ +β β β*)) β§ π§ β€ π§) β ((-β(,)π§) β© (π§(,)+β)) = β
) |
57 | 53, 54, 55, 56 | syl21anc 837 |
. . . . . . 7
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β ((-β(,)π§) β© (π§(,)+β)) = β
) |
58 | | sseq0 4363 |
. . . . . . 7
β’
(((((-β(,)π§)
β© (π§(,)+β)) β©
π΄) β
((-β(,)π§) β©
(π§(,)+β)) β§
((-β(,)π§) β©
(π§(,)+β)) = β
)
β (((-β(,)π§)
β© (π§(,)+β)) β©
π΄) =
β
) |
59 | 52, 57, 58 | sylancr 588 |
. . . . . 6
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (((-β(,)π§) β© (π§(,)+β)) β© π΄) = β
) |
60 | 30 | a1i 11 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β -β β
β*) |
61 | 46 | a1i 11 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β +β β
β*) |
62 | 25 | mnfltd 13053 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β -β < π§) |
63 | 25 | ltpnfd 13050 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π§ < +β) |
64 | | ioojoin 13409 |
. . . . . . . . . 10
β’
(((-β β β* β§ π§ β β* β§ +β
β β*) β§ (-β < π§ β§ π§ < +β)) β (((-β(,)π§) βͺ {π§}) βͺ (π§(,)+β)) =
(-β(,)+β)) |
65 | 60, 31, 61, 62, 63, 64 | syl32anc 1379 |
. . . . . . . . 9
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (((-β(,)π§) βͺ {π§}) βͺ (π§(,)+β)) =
(-β(,)+β)) |
66 | | unass 4130 |
. . . . . . . . . 10
β’
(((-β(,)π§)
βͺ {π§}) βͺ (π§(,)+β)) =
((-β(,)π§) βͺ
({π§} βͺ (π§(,)+β))) |
67 | | un12 4131 |
. . . . . . . . . 10
β’
((-β(,)π§)
βͺ ({π§} βͺ (π§(,)+β))) = ({π§} βͺ ((-β(,)π§) βͺ (π§(,)+β))) |
68 | 66, 67 | eqtri 2761 |
. . . . . . . . 9
β’
(((-β(,)π§)
βͺ {π§}) βͺ (π§(,)+β)) = ({π§} βͺ ((-β(,)π§) βͺ (π§(,)+β))) |
69 | | ioomax 13348 |
. . . . . . . . 9
β’
(-β(,)+β) = β |
70 | 65, 68, 69 | 3eqtr3g 2796 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β ({π§} βͺ ((-β(,)π§) βͺ (π§(,)+β))) = β) |
71 | 4, 70 | sseqtrrd 3989 |
. . . . . . 7
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π΄ β ({π§} βͺ ((-β(,)π§) βͺ (π§(,)+β)))) |
72 | | disjsn 4676 |
. . . . . . . . 9
β’ ((π΄ β© {π§}) = β
β Β¬ π§ β π΄) |
73 | 13, 72 | sylibr 233 |
. . . . . . . 8
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π΄ β© {π§}) = β
) |
74 | | disjssun 4431 |
. . . . . . . 8
β’ ((π΄ β© {π§}) = β
β (π΄ β ({π§} βͺ ((-β(,)π§) βͺ (π§(,)+β))) β π΄ β ((-β(,)π§) βͺ (π§(,)+β)))) |
75 | 73, 74 | syl 17 |
. . . . . . 7
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β (π΄ β ({π§} βͺ ((-β(,)π§) βͺ (π§(,)+β))) β π΄ β ((-β(,)π§) βͺ (π§(,)+β)))) |
76 | 71, 75 | mpbid 231 |
. . . . . 6
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β π΄ β ((-β(,)π§) βͺ (π§(,)+β))) |
77 | 3, 4, 6, 8, 36, 51, 59, 76 | nconnsubb 22797 |
. . . . 5
β’ ((((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β§ π§ β ((π[,]π) β π΄)) β Β¬ ((topGenβran (,))
βΎt π΄)
β Conn) |
78 | 77 | ex 414 |
. . . 4
β’ (((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β (π§ β ((π[,]π) β π΄) β Β¬ ((topGenβran (,))
βΎt π΄)
β Conn)) |
79 | 1, 78 | mt2d 136 |
. . 3
β’ (((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β Β¬ π§ β ((π[,]π) β π΄)) |
80 | 79 | eq0rdv 4368 |
. 2
β’ (((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β ((π[,]π) β π΄) = β
) |
81 | | ssdif0 4327 |
. 2
β’ ((π[,]π) β π΄ β ((π[,]π) β π΄) = β
) |
82 | 80, 81 | sylibr 233 |
1
β’ (((π΄ β β β§
((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β (π[,]π) β π΄) |