Step | Hyp | Ref
| Expression |
1 | | 0opn 22626 |
. . . . 5
β’ (π½ β Top β β
β π½) |
2 | 1 | adantr 481 |
. . . 4
β’ ((π½ β Top β§ π = β
) β β
β π½) |
3 | | eleq1 2821 |
. . . . 5
β’ (π = β
β (π β π½ β β
β π½)) |
4 | 3 | adantl 482 |
. . . 4
β’ ((π½ β Top β§ π = β
) β (π β π½ β β
β π½)) |
5 | 2, 4 | mpbird 256 |
. . 3
β’ ((π½ β Top β§ π = β
) β π β π½) |
6 | | rzal 4508 |
. . . 4
β’ (π = β
β βπ₯ β π π β ((neiβπ½)β{π₯})) |
7 | 6 | adantl 482 |
. . 3
β’ ((π½ β Top β§ π = β
) β βπ₯ β π π β ((neiβπ½)β{π₯})) |
8 | 5, 7 | 2thd 264 |
. 2
β’ ((π½ β Top β§ π = β
) β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
9 | | opnneip 22843 |
. . . . . . 7
β’ ((π½ β Top β§ π β π½ β§ π₯ β π) β π β ((neiβπ½)β{π₯})) |
10 | 9 | 3expia 1121 |
. . . . . 6
β’ ((π½ β Top β§ π β π½) β (π₯ β π β π β ((neiβπ½)β{π₯}))) |
11 | 10 | ralrimiv 3145 |
. . . . 5
β’ ((π½ β Top β§ π β π½) β βπ₯ β π π β ((neiβπ½)β{π₯})) |
12 | 11 | ex 413 |
. . . 4
β’ (π½ β Top β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
13 | 12 | adantr 481 |
. . 3
β’ ((π½ β Top β§ Β¬ π = β
) β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
14 | | df-ne 2941 |
. . . . . 6
β’ (π β β
β Β¬ π = β
) |
15 | | r19.2z 4494 |
. . . . . . 7
β’ ((π β β
β§
βπ₯ β π π β ((neiβπ½)β{π₯})) β βπ₯ β π π β ((neiβπ½)β{π₯})) |
16 | 15 | ex 413 |
. . . . . 6
β’ (π β β
β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
17 | 14, 16 | sylbir 234 |
. . . . 5
β’ (Β¬
π = β
β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
18 | | eqid 2732 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
19 | 18 | neii1 22830 |
. . . . . . 7
β’ ((π½ β Top β§ π β ((neiβπ½)β{π₯})) β π β βͺ π½) |
20 | 19 | ex 413 |
. . . . . 6
β’ (π½ β Top β (π β ((neiβπ½)β{π₯}) β π β βͺ π½)) |
21 | 20 | rexlimdvw 3160 |
. . . . 5
β’ (π½ β Top β (βπ₯ β π π β ((neiβπ½)β{π₯}) β π β βͺ π½)) |
22 | 17, 21 | sylan9r 509 |
. . . 4
β’ ((π½ β Top β§ Β¬ π = β
) β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β π β βͺ π½)) |
23 | 18 | ntrss2 22781 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β βͺ π½)
β ((intβπ½)βπ) β π) |
24 | 23 | adantr 481 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β βͺ π½)
β§ βπ₯ β
π {π₯} β ((intβπ½)βπ)) β ((intβπ½)βπ) β π) |
25 | | vex 3478 |
. . . . . . . . . . . . 13
β’ π₯ β V |
26 | 25 | snss 4789 |
. . . . . . . . . . . 12
β’ (π₯ β ((intβπ½)βπ) β {π₯} β ((intβπ½)βπ)) |
27 | 26 | ralbii 3093 |
. . . . . . . . . . 11
β’
(βπ₯ β
π π₯ β ((intβπ½)βπ) β βπ₯ β π {π₯} β ((intβπ½)βπ)) |
28 | | dfss3 3970 |
. . . . . . . . . . . . 13
β’ (π β ((intβπ½)βπ) β βπ₯ β π π₯ β ((intβπ½)βπ)) |
29 | 28 | biimpri 227 |
. . . . . . . . . . . 12
β’
(βπ₯ β
π π₯ β ((intβπ½)βπ) β π β ((intβπ½)βπ)) |
30 | 29 | adantl 482 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ π β βͺ π½)
β§ βπ₯ β
π π₯ β ((intβπ½)βπ)) β π β ((intβπ½)βπ)) |
31 | 27, 30 | sylan2br 595 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β βͺ π½)
β§ βπ₯ β
π {π₯} β ((intβπ½)βπ)) β π β ((intβπ½)βπ)) |
32 | 24, 31 | eqssd 3999 |
. . . . . . . . 9
β’ (((π½ β Top β§ π β βͺ π½)
β§ βπ₯ β
π {π₯} β ((intβπ½)βπ)) β ((intβπ½)βπ) = π) |
33 | 32 | ex 413 |
. . . . . . . 8
β’ ((π½ β Top β§ π β βͺ π½)
β (βπ₯ β
π {π₯} β ((intβπ½)βπ) β ((intβπ½)βπ) = π)) |
34 | 25 | snss 4789 |
. . . . . . . . . . . 12
β’ (π₯ β π β {π₯} β π) |
35 | | sstr2 3989 |
. . . . . . . . . . . . . 14
β’ ({π₯} β π β (π β βͺ π½ β {π₯} β βͺ π½)) |
36 | 35 | com12 32 |
. . . . . . . . . . . . 13
β’ (π β βͺ π½
β ({π₯} β π β {π₯} β βͺ π½)) |
37 | 36 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π β βͺ π½)
β ({π₯} β π β {π₯} β βͺ π½)) |
38 | 34, 37 | biimtrid 241 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β βͺ π½)
β (π₯ β π β {π₯} β βͺ π½)) |
39 | 38 | imp 407 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β βͺ π½)
β§ π₯ β π) β {π₯} β βͺ π½) |
40 | 18 | neiint 22828 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ {π₯} β βͺ π½
β§ π β βͺ π½)
β (π β
((neiβπ½)β{π₯}) β {π₯} β ((intβπ½)βπ))) |
41 | 40 | 3com23 1126 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β βͺ π½
β§ {π₯} β βͺ π½)
β (π β
((neiβπ½)β{π₯}) β {π₯} β ((intβπ½)βπ))) |
42 | 41 | 3expa 1118 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β βͺ π½)
β§ {π₯} β βͺ π½)
β (π β
((neiβπ½)β{π₯}) β {π₯} β ((intβπ½)βπ))) |
43 | 39, 42 | syldan 591 |
. . . . . . . . 9
β’ (((π½ β Top β§ π β βͺ π½)
β§ π₯ β π) β (π β ((neiβπ½)β{π₯}) β {π₯} β ((intβπ½)βπ))) |
44 | 43 | ralbidva 3175 |
. . . . . . . 8
β’ ((π½ β Top β§ π β βͺ π½)
β (βπ₯ β
π π β ((neiβπ½)β{π₯}) β βπ₯ β π {π₯} β ((intβπ½)βπ))) |
45 | 18 | isopn3 22790 |
. . . . . . . 8
β’ ((π½ β Top β§ π β βͺ π½)
β (π β π½ β ((intβπ½)βπ) = π)) |
46 | 33, 44, 45 | 3imtr4d 293 |
. . . . . . 7
β’ ((π½ β Top β§ π β βͺ π½)
β (βπ₯ β
π π β ((neiβπ½)β{π₯}) β π β π½)) |
47 | 46 | ex 413 |
. . . . . 6
β’ (π½ β Top β (π β βͺ π½
β (βπ₯ β
π π β ((neiβπ½)β{π₯}) β π β π½))) |
48 | 47 | com23 86 |
. . . . 5
β’ (π½ β Top β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β (π β βͺ π½ β π β π½))) |
49 | 48 | adantr 481 |
. . . 4
β’ ((π½ β Top β§ Β¬ π = β
) β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β (π β βͺ π½ β π β π½))) |
50 | 22, 49 | mpdd 43 |
. . 3
β’ ((π½ β Top β§ Β¬ π = β
) β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β π β π½)) |
51 | 13, 50 | impbid 211 |
. 2
β’ ((π½ β Top β§ Β¬ π = β
) β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
52 | 8, 51 | pm2.61dan 811 |
1
β’ (π½ β Top β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) |