Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
2 | | simpll 766 |
. . . . . 6
β’ (((π½ β Conn β§ (π₯ β π½ β§ π¦ β π½)) β§ (π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
)) β π½ β Conn) |
3 | | simplrl 776 |
. . . . . 6
β’ (((π½ β Conn β§ (π₯ β π½ β§ π¦ β π½)) β§ (π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
)) β π₯ β π½) |
4 | | simpr1 1195 |
. . . . . 6
β’ (((π½ β Conn β§ (π₯ β π½ β§ π¦ β π½)) β§ (π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
)) β π₯ β β
) |
5 | | simplrr 777 |
. . . . . 6
β’ (((π½ β Conn β§ (π₯ β π½ β§ π¦ β π½)) β§ (π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
)) β π¦ β π½) |
6 | | simpr2 1196 |
. . . . . 6
β’ (((π½ β Conn β§ (π₯ β π½ β§ π¦ β π½)) β§ (π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
)) β π¦ β β
) |
7 | | simpr3 1197 |
. . . . . 6
β’ (((π½ β Conn β§ (π₯ β π½ β§ π¦ β π½)) β§ (π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
)) β (π₯ β© π¦) = β
) |
8 | 1, 2, 3, 4, 5, 6, 7 | conndisj 22783 |
. . . . 5
β’ (((π½ β Conn β§ (π₯ β π½ β§ π¦ β π½)) β§ (π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
)) β (π₯ βͺ π¦) β βͺ π½) |
9 | 8 | ex 414 |
. . . 4
β’ ((π½ β Conn β§ (π₯ β π½ β§ π¦ β π½)) β ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½)) |
10 | 9 | ralrimivva 3198 |
. . 3
β’ (π½ β Conn β
βπ₯ β π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½)) |
11 | | topontop 22278 |
. . . 4
β’ (π½ β (TopOnβπ) β π½ β Top) |
12 | 1 | cldopn 22398 |
. . . . . . . . . . . . . 14
β’ (π₯ β (Clsdβπ½) β (βͺ π½
β π₯) β π½) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βͺ π½
β π₯) β π½) |
14 | | df-3an 1090 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β ((π₯ β β
β§ π¦ β β
) β§ (π₯ β© π¦) = β
)) |
15 | | ineq2 4171 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = (βͺ
π½ β π₯) β (π₯ β© π¦) = (π₯ β© (βͺ π½ β π₯))) |
16 | | disjdif 4436 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β© (βͺ π½
β π₯)) =
β
|
17 | 15, 16 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = (βͺ
π½ β π₯) β (π₯ β© π¦) = β
) |
18 | 17 | biantrud 533 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (βͺ
π½ β π₯) β ((π₯ β β
β§ π¦ β β
) β ((π₯ β β
β§ π¦ β β
) β§ (π₯ β© π¦) = β
))) |
19 | | neeq1 3007 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = (βͺ
π½ β π₯) β (π¦ β β
β (βͺ π½
β π₯) β
β
)) |
20 | 19 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (βͺ
π½ β π₯) β ((π₯ β β
β§ π¦ β β
) β (π₯ β β
β§ (βͺ π½
β π₯) β
β
))) |
21 | 18, 20 | bitr3d 281 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (βͺ
π½ β π₯) β (((π₯ β β
β§ π¦ β β
) β§ (π₯ β© π¦) = β
) β (π₯ β β
β§ (βͺ π½
β π₯) β
β
))) |
22 | 14, 21 | bitrid 283 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (βͺ
π½ β π₯) β ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ β β
β§ (βͺ π½
β π₯) β
β
))) |
23 | | uneq2 4122 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (βͺ
π½ β π₯) β (π₯ βͺ π¦) = (π₯ βͺ (βͺ π½ β π₯))) |
24 | | undif2 4441 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ βͺ (βͺ π½
β π₯)) = (π₯ βͺ βͺ π½) |
25 | 23, 24 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (βͺ
π½ β π₯) β (π₯ βͺ π¦) = (π₯ βͺ βͺ π½)) |
26 | 25 | neeq1d 3004 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (βͺ
π½ β π₯) β ((π₯ βͺ π¦) β βͺ π½ β (π₯ βͺ βͺ π½) β βͺ π½)) |
27 | 22, 26 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π¦ = (βͺ
π½ β π₯) β (((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½) β ((π₯ β β
β§ (βͺ π½
β π₯) β β
)
β (π₯ βͺ βͺ π½)
β βͺ π½))) |
28 | 27 | rspcv 3580 |
. . . . . . . . . . . . 13
β’ ((βͺ π½
β π₯) β π½ β (βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½) β ((π₯ β β
β§ (βͺ π½
β π₯) β β
)
β (π₯ βͺ βͺ π½)
β βͺ π½))) |
29 | 13, 28 | syl 17 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½) β ((π₯ β β
β§ (βͺ π½
β π₯) β β
)
β (π₯ βͺ βͺ π½)
β βͺ π½))) |
30 | 1 | cldss 22396 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (Clsdβπ½) β π₯ β βͺ π½) |
31 | 30 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β π₯ β βͺ π½) |
32 | | ssequn1 4145 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β βͺ π½
β (π₯ βͺ βͺ π½) =
βͺ π½) |
33 | 31, 32 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (π₯ βͺ βͺ π½) = βͺ
π½) |
34 | | ssdif0 4328 |
. . . . . . . . . . . . . . . 16
β’ (βͺ π½
β π₯ β (βͺ π½
β π₯) =
β
) |
35 | | idd 24 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βͺ π½
β π₯ β βͺ π½
β π₯)) |
36 | 35, 31 | jctild 527 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βͺ π½
β π₯ β (π₯ β βͺ π½
β§ βͺ π½ β π₯))) |
37 | | eqss 3964 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = βͺ
π½ β (π₯ β βͺ π½
β§ βͺ π½ β π₯)) |
38 | 36, 37 | syl6ibr 252 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βͺ π½
β π₯ β π₯ = βͺ
π½)) |
39 | 34, 38 | biimtrrid 242 |
. . . . . . . . . . . . . . 15
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β ((βͺ π½
β π₯) = β
β
π₯ = βͺ π½)) |
40 | 33, 39 | embantd 59 |
. . . . . . . . . . . . . 14
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (((π₯ βͺ βͺ π½) = βͺ
π½ β (βͺ π½
β π₯) = β
)
β π₯ = βͺ π½)) |
41 | 40 | orim2d 966 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β ((π₯ = β
β¨ ((π₯ βͺ βͺ π½) = βͺ
π½ β (βͺ π½
β π₯) = β
))
β (π₯ = β
β¨
π₯ = βͺ π½))) |
42 | | impexp 452 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β
β§ (βͺ π½
β π₯) β β
)
β (π₯ βͺ βͺ π½)
β βͺ π½) β (π₯ β β
β ((βͺ π½
β π₯) β β
β (π₯ βͺ βͺ π½)
β βͺ π½))) |
43 | | df-ne 2945 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β
β Β¬ π₯ = β
) |
44 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (((βͺ π½
β π₯) β β
β (π₯ βͺ βͺ π½)
β βͺ π½) β ((βͺ
π½ β π₯) β β
β (π₯ βͺ βͺ π½)
β βͺ π½)) |
45 | 44 | necon4d 2968 |
. . . . . . . . . . . . . . . . 17
β’ (((βͺ π½
β π₯) β β
β (π₯ βͺ βͺ π½)
β βͺ π½) β ((π₯ βͺ βͺ π½) = βͺ
π½ β (βͺ π½
β π₯) =
β
)) |
46 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ βͺ βͺ π½) =
βͺ π½ β (βͺ π½ β π₯) = β
) β ((π₯ βͺ βͺ π½) = βͺ
π½ β (βͺ π½
β π₯) =
β
)) |
47 | 46 | necon3d 2965 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ βͺ βͺ π½) =
βͺ π½ β (βͺ π½ β π₯) = β
) β ((βͺ π½
β π₯) β β
β (π₯ βͺ βͺ π½)
β βͺ π½)) |
48 | 45, 47 | impbii 208 |
. . . . . . . . . . . . . . . 16
β’ (((βͺ π½
β π₯) β β
β (π₯ βͺ βͺ π½)
β βͺ π½) β ((π₯ βͺ βͺ π½) = βͺ
π½ β (βͺ π½
β π₯) =
β
)) |
49 | 43, 48 | imbi12i 351 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β
β ((βͺ π½
β π₯) β β
β (π₯ βͺ βͺ π½)
β βͺ π½)) β (Β¬ π₯ = β
β ((π₯ βͺ βͺ π½) = βͺ
π½ β (βͺ π½
β π₯) =
β
))) |
50 | | pm4.64 848 |
. . . . . . . . . . . . . . 15
β’ ((Β¬
π₯ = β
β ((π₯ βͺ βͺ π½) =
βͺ π½ β (βͺ π½ β π₯) = β
)) β (π₯ = β
β¨ ((π₯ βͺ βͺ π½) = βͺ
π½ β (βͺ π½
β π₯) =
β
))) |
51 | 49, 50 | bitri 275 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β
β ((βͺ π½
β π₯) β β
β (π₯ βͺ βͺ π½)
β βͺ π½)) β (π₯ = β
β¨ ((π₯ βͺ βͺ π½) = βͺ
π½ β (βͺ π½
β π₯) =
β
))) |
52 | 42, 51 | bitri 275 |
. . . . . . . . . . . . 13
β’ (((π₯ β β
β§ (βͺ π½
β π₯) β β
)
β (π₯ βͺ βͺ π½)
β βͺ π½) β (π₯ = β
β¨ ((π₯ βͺ βͺ π½) = βͺ
π½ β (βͺ π½
β π₯) =
β
))) |
53 | | vex 3452 |
. . . . . . . . . . . . . 14
β’ π₯ β V |
54 | 53 | elpr 4614 |
. . . . . . . . . . . . 13
β’ (π₯ β {β
, βͺ π½}
β (π₯ = β
β¨
π₯ = βͺ π½)) |
55 | 41, 52, 54 | 3imtr4g 296 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (((π₯ β β
β§ (βͺ π½
β π₯) β β
)
β (π₯ βͺ βͺ π½)
β βͺ π½) β π₯ β {β
, βͺ π½})) |
56 | 29, 55 | syld 47 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π₯ β (Clsdβπ½)) β (βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½) β π₯ β {β
, βͺ π½})) |
57 | 56 | ex 414 |
. . . . . . . . . 10
β’ (π½ β Top β (π₯ β (Clsdβπ½) β (βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½) β π₯ β {β
, βͺ π½}))) |
58 | 57 | com23 86 |
. . . . . . . . 9
β’ (π½ β Top β
(βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½) β (π₯ β (Clsdβπ½) β π₯ β {β
, βͺ π½}))) |
59 | 58 | imim2d 57 |
. . . . . . . 8
β’ (π½ β Top β ((π₯ β π½ β βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½)) β (π₯ β π½ β (π₯ β (Clsdβπ½) β π₯ β {β
, βͺ π½})))) |
60 | | elin 3931 |
. . . . . . . . . 10
β’ (π₯ β (π½ β© (Clsdβπ½)) β (π₯ β π½ β§ π₯ β (Clsdβπ½))) |
61 | 60 | imbi1i 350 |
. . . . . . . . 9
β’ ((π₯ β (π½ β© (Clsdβπ½)) β π₯ β {β
, βͺ π½})
β ((π₯ β π½ β§ π₯ β (Clsdβπ½)) β π₯ β {β
, βͺ π½})) |
62 | | impexp 452 |
. . . . . . . . 9
β’ (((π₯ β π½ β§ π₯ β (Clsdβπ½)) β π₯ β {β
, βͺ π½})
β (π₯ β π½ β (π₯ β (Clsdβπ½) β π₯ β {β
, βͺ π½}))) |
63 | 61, 62 | bitri 275 |
. . . . . . . 8
β’ ((π₯ β (π½ β© (Clsdβπ½)) β π₯ β {β
, βͺ π½})
β (π₯ β π½ β (π₯ β (Clsdβπ½) β π₯ β {β
, βͺ π½}))) |
64 | 59, 63 | syl6ibr 252 |
. . . . . . 7
β’ (π½ β Top β ((π₯ β π½ β βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½)) β (π₯ β (π½ β© (Clsdβπ½)) β π₯ β {β
, βͺ π½}))) |
65 | 64 | alimdv 1920 |
. . . . . 6
β’ (π½ β Top β
(βπ₯(π₯ β π½ β βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½)) β βπ₯(π₯ β (π½ β© (Clsdβπ½)) β π₯ β {β
, βͺ π½}))) |
66 | | df-ral 3066 |
. . . . . 6
β’
(βπ₯ β
π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½) β βπ₯(π₯ β π½ β βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½))) |
67 | | dfss2 3935 |
. . . . . 6
β’ ((π½ β© (Clsdβπ½)) β {β
, βͺ π½}
β βπ₯(π₯ β (π½ β© (Clsdβπ½)) β π₯ β {β
, βͺ π½})) |
68 | 65, 66, 67 | 3imtr4g 296 |
. . . . 5
β’ (π½ β Top β
(βπ₯ β π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½) β (π½ β© (Clsdβπ½)) β {β
, βͺ π½})) |
69 | 1 | isconn2 22781 |
. . . . . 6
β’ (π½ β Conn β (π½ β Top β§ (π½ β© (Clsdβπ½)) β {β
, βͺ π½})) |
70 | 69 | baib 537 |
. . . . 5
β’ (π½ β Top β (π½ β Conn β (π½ β© (Clsdβπ½)) β {β
, βͺ π½})) |
71 | 68, 70 | sylibrd 259 |
. . . 4
β’ (π½ β Top β
(βπ₯ β π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½) β π½ β Conn)) |
72 | 11, 71 | syl 17 |
. . 3
β’ (π½ β (TopOnβπ) β (βπ₯ β π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½) β π½ β Conn)) |
73 | 10, 72 | impbid2 225 |
. 2
β’ (π½ β (TopOnβπ) β (π½ β Conn β βπ₯ β π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½))) |
74 | | toponuni 22279 |
. . . . 5
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
75 | 74 | neeq2d 3005 |
. . . 4
β’ (π½ β (TopOnβπ) β ((π₯ βͺ π¦) β π β (π₯ βͺ π¦) β βͺ π½)) |
76 | 75 | imbi2d 341 |
. . 3
β’ (π½ β (TopOnβπ) β (((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β π) β ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½))) |
77 | 76 | 2ralbidv 3213 |
. 2
β’ (π½ β (TopOnβπ) β (βπ₯ β π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β π) β βπ₯ β π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β βͺ π½))) |
78 | 73, 77 | bitr4d 282 |
1
β’ (π½ β (TopOnβπ) β (π½ β Conn β βπ₯ β π½ βπ¦ β π½ ((π₯ β β
β§ π¦ β β
β§ (π₯ β© π¦) = β
) β (π₯ βͺ π¦) β π))) |