Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
2 | 1 | hausnei 22702 |
. . . . . . . 8
β’ ((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β βπ§ β π½ βπ€ β π½ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
)) |
3 | | simprr1 1222 |
. . . . . . . . . . 11
β’ ((((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β§ π§ β π½) β§ (π€ β π½ β§ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
))) β π₯ β π§) |
4 | | noel 4294 |
. . . . . . . . . . . . 13
β’ Β¬
π¦ β
β
|
5 | | simprr3 1224 |
. . . . . . . . . . . . . 14
β’ ((((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β§ π§ β π½) β§ (π€ β π½ β§ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
))) β (π§ β© π€) = β
) |
6 | 5 | eleq2d 2820 |
. . . . . . . . . . . . 13
β’ ((((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β§ π§ β π½) β§ (π€ β π½ β§ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
))) β (π¦ β (π§ β© π€) β π¦ β β
)) |
7 | 4, 6 | mtbiri 327 |
. . . . . . . . . . . 12
β’ ((((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β§ π§ β π½) β§ (π€ β π½ β§ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
))) β Β¬ π¦ β (π§ β© π€)) |
8 | | simprr2 1223 |
. . . . . . . . . . . . 13
β’ ((((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β§ π§ β π½) β§ (π€ β π½ β§ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
))) β π¦ β π€) |
9 | | elin 3930 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π§ β© π€) β (π¦ β π§ β§ π¦ β π€)) |
10 | 9 | simplbi2com 504 |
. . . . . . . . . . . . 13
β’ (π¦ β π€ β (π¦ β π§ β π¦ β (π§ β© π€))) |
11 | 8, 10 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β§ π§ β π½) β§ (π€ β π½ β§ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
))) β (π¦ β π§ β π¦ β (π§ β© π€))) |
12 | 7, 11 | mtod 197 |
. . . . . . . . . . 11
β’ ((((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β§ π§ β π½) β§ (π€ β π½ β§ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
))) β Β¬ π¦ β π§) |
13 | 3, 12 | jca 513 |
. . . . . . . . . 10
β’ ((((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β§ π§ β π½) β§ (π€ β π½ β§ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
))) β (π₯ β π§ β§ Β¬ π¦ β π§)) |
14 | 13 | rexlimdvaa 3150 |
. . . . . . . . 9
β’ (((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β§ π§ β π½) β (βπ€ β π½ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
) β (π₯ β π§ β§ Β¬ π¦ β π§))) |
15 | 14 | reximdva 3162 |
. . . . . . . 8
β’ ((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β (βπ§ β π½ βπ€ β π½ (π₯ β π§ β§ π¦ β π€ β§ (π§ β© π€) = β
) β βπ§ β π½ (π₯ β π§ β§ Β¬ π¦ β π§))) |
16 | 2, 15 | mpd 15 |
. . . . . . 7
β’ ((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β βπ§ β π½ (π₯ β π§ β§ Β¬ π¦ β π§)) |
17 | | rexanali 3102 |
. . . . . . 7
β’
(βπ§ β
π½ (π₯ β π§ β§ Β¬ π¦ β π§) β Β¬ βπ§ β π½ (π₯ β π§ β π¦ β π§)) |
18 | 16, 17 | sylib 217 |
. . . . . 6
β’ ((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½
β§ π₯ β π¦)) β Β¬ βπ§ β π½ (π₯ β π§ β π¦ β π§)) |
19 | 18 | 3exp2 1355 |
. . . . 5
β’ (π½ β Haus β (π₯ β βͺ π½
β (π¦ β βͺ π½
β (π₯ β π¦ β Β¬ βπ§ β π½ (π₯ β π§ β π¦ β π§))))) |
20 | 19 | imp32 420 |
. . . 4
β’ ((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½))
β (π₯ β π¦ β Β¬ βπ§ β π½ (π₯ β π§ β π¦ β π§))) |
21 | 20 | necon4ad 2959 |
. . 3
β’ ((π½ β Haus β§ (π₯ β βͺ π½
β§ π¦ β βͺ π½))
β (βπ§ β
π½ (π₯ β π§ β π¦ β π§) β π₯ = π¦)) |
22 | 21 | ralrimivva 3194 |
. 2
β’ (π½ β Haus β
βπ₯ β βͺ π½βπ¦ β βͺ π½(βπ§ β π½ (π₯ β π§ β π¦ β π§) β π₯ = π¦)) |
23 | | haustop 22705 |
. . . 4
β’ (π½ β Haus β π½ β Top) |
24 | | toptopon2 22290 |
. . . 4
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
25 | 23, 24 | sylib 217 |
. . 3
β’ (π½ β Haus β π½ β (TopOnββͺ π½)) |
26 | | ist1-2 22721 |
. . 3
β’ (π½ β (TopOnββͺ π½)
β (π½ β Fre β
βπ₯ β βͺ π½βπ¦ β βͺ π½(βπ§ β π½ (π₯ β π§ β π¦ β π§) β π₯ = π¦))) |
27 | 25, 26 | syl 17 |
. 2
β’ (π½ β Haus β (π½ β Fre β βπ₯ β βͺ π½βπ¦ β βͺ π½(βπ§ β π½ (π₯ β π§ β π¦ β π§) β π₯ = π¦))) |
28 | 22, 27 | mpbird 257 |
1
β’ (π½ β Haus β π½ β Fre) |