Step | Hyp | Ref
| Expression |
1 | | n0 4310 |
. . 3
β’ ((π΄ β© π΅) β β
β βπ₯ π₯ β (π΄ β© π΅)) |
2 | | uniiun 5022 |
. . . . . . . . 9
β’ βͺ {π΄,
π΅} = βͺ π β {π΄, π΅}π |
3 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β π½ β (TopOnβπ)) |
4 | | toponmax 22298 |
. . . . . . . . . . . 12
β’ (π½ β (TopOnβπ) β π β π½) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β π β π½) |
6 | | simpl2l 1227 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β π΄ β π) |
7 | 5, 6 | ssexd 5285 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β π΄ β V) |
8 | | simpl2r 1228 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β π΅ β π) |
9 | 5, 8 | ssexd 5285 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β π΅ β V) |
10 | | uniprg 4886 |
. . . . . . . . . 10
β’ ((π΄ β V β§ π΅ β V) β βͺ {π΄,
π΅} = (π΄ βͺ π΅)) |
11 | 7, 9, 10 | syl2anc 585 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β βͺ {π΄,
π΅} = (π΄ βͺ π΅)) |
12 | 2, 11 | eqtr3id 2787 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β βͺ π β {π΄, π΅}π = (π΄ βͺ π΅)) |
13 | 12 | oveq2d 7377 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β (π½ βΎt βͺ π β {π΄, π΅}π) = (π½ βΎt (π΄ βͺ π΅))) |
14 | | vex 3451 |
. . . . . . . . . 10
β’ π β V |
15 | 14 | elpr 4613 |
. . . . . . . . 9
β’ (π β {π΄, π΅} β (π = π΄ β¨ π = π΅)) |
16 | | simpl2 1193 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β (π΄ β π β§ π΅ β π)) |
17 | | sseq1 3973 |
. . . . . . . . . . . 12
β’ (π = π΄ β (π β π β π΄ β π)) |
18 | 17 | biimprd 248 |
. . . . . . . . . . 11
β’ (π = π΄ β (π΄ β π β π β π)) |
19 | | sseq1 3973 |
. . . . . . . . . . . 12
β’ (π = π΅ β (π β π β π΅ β π)) |
20 | 19 | biimprd 248 |
. . . . . . . . . . 11
β’ (π = π΅ β (π΅ β π β π β π)) |
21 | 18, 20 | jaoa 955 |
. . . . . . . . . 10
β’ ((π = π΄ β¨ π = π΅) β ((π΄ β π β§ π΅ β π) β π β π)) |
22 | 16, 21 | mpan9 508 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β§ (π = π΄ β¨ π = π΅)) β π β π) |
23 | 15, 22 | sylan2b 595 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β§ π β {π΄, π΅}) β π β π) |
24 | | simpl3 1194 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β π₯ β (π΄ β© π΅)) |
25 | | elin 3930 |
. . . . . . . . . . 11
β’ (π₯ β (π΄ β© π΅) β (π₯ β π΄ β§ π₯ β π΅)) |
26 | 24, 25 | sylib 217 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β (π₯ β π΄ β§ π₯ β π΅)) |
27 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π = π΄ β (π₯ β π β π₯ β π΄)) |
28 | 27 | biimprd 248 |
. . . . . . . . . . 11
β’ (π = π΄ β (π₯ β π΄ β π₯ β π)) |
29 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π = π΅ β (π₯ β π β π₯ β π΅)) |
30 | 29 | biimprd 248 |
. . . . . . . . . . 11
β’ (π = π΅ β (π₯ β π΅ β π₯ β π)) |
31 | 28, 30 | jaoa 955 |
. . . . . . . . . 10
β’ ((π = π΄ β¨ π = π΅) β ((π₯ β π΄ β§ π₯ β π΅) β π₯ β π)) |
32 | 26, 31 | mpan9 508 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β§ (π = π΄ β¨ π = π΅)) β π₯ β π) |
33 | 15, 32 | sylan2b 595 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β§ π β {π΄, π΅}) β π₯ β π) |
34 | | simpr 486 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) |
35 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π = π΄ β (π½ βΎt π) = (π½ βΎt π΄)) |
36 | 35 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = π΄ β ((π½ βΎt π) β Conn β (π½ βΎt π΄) β Conn)) |
37 | 36 | biimprd 248 |
. . . . . . . . . . 11
β’ (π = π΄ β ((π½ βΎt π΄) β Conn β (π½ βΎt π) β Conn)) |
38 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π = π΅ β (π½ βΎt π) = (π½ βΎt π΅)) |
39 | 38 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = π΅ β ((π½ βΎt π) β Conn β (π½ βΎt π΅) β Conn)) |
40 | 39 | biimprd 248 |
. . . . . . . . . . 11
β’ (π = π΅ β ((π½ βΎt π΅) β Conn β (π½ βΎt π) β Conn)) |
41 | 37, 40 | jaoa 955 |
. . . . . . . . . 10
β’ ((π = π΄ β¨ π = π΅) β (((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn) β (π½ βΎt π) β Conn)) |
42 | 34, 41 | mpan9 508 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β§ (π = π΄ β¨ π = π΅)) β (π½ βΎt π) β Conn) |
43 | 15, 42 | sylan2b 595 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β§ π β {π΄, π΅}) β (π½ βΎt π) β Conn) |
44 | 3, 23, 33, 43 | iunconn 22802 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β (π½ βΎt βͺ π β {π΄, π΅}π) β Conn) |
45 | 13, 44 | eqeltrrd 2835 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β§ ((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn)) β (π½ βΎt (π΄ βͺ π΅)) β Conn) |
46 | 45 | ex 414 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ π₯ β (π΄ β© π΅)) β (((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn) β (π½ βΎt (π΄ βͺ π΅)) β Conn)) |
47 | 46 | 3expia 1122 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π)) β (π₯ β (π΄ β© π΅) β (((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn) β (π½ βΎt (π΄ βͺ π΅)) β Conn))) |
48 | 47 | exlimdv 1937 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π)) β (βπ₯ π₯ β (π΄ β© π΅) β (((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn) β (π½ βΎt (π΄ βͺ π΅)) β Conn))) |
49 | 1, 48 | biimtrid 241 |
. 2
β’ ((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π)) β ((π΄ β© π΅) β β
β (((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn) β (π½ βΎt (π΄ βͺ π΅)) β Conn))) |
50 | 49 | 3impia 1118 |
1
β’ ((π½ β (TopOnβπ) β§ (π΄ β π β§ π΅ β π) β§ (π΄ β© π΅) β β
) β (((π½ βΎt π΄) β Conn β§ (π½ βΎt π΅) β Conn) β (π½ βΎt (π΄ βͺ π΅)) β Conn)) |