Step | Hyp | Ref
| Expression |
1 | | 0opn 22626 |
. . . . 5
β’ (π½ β Top β β
β π½) |
2 | 1 | adantr 479 |
. . . 4
β’ ((π½ β Top β§ π = β
) β β
β π½) |
3 | | eleq1 2819 |
. . . . 5
β’ (π = β
β (π β π½ β β
β π½)) |
4 | 3 | adantl 480 |
. . . 4
β’ ((π½ β Top β§ π = β
) β (π β π½ β β
β π½)) |
5 | 2, 4 | mpbird 256 |
. . 3
β’ ((π½ β Top β§ π = β
) β π β π½) |
6 | | rzal 4507 |
. . . 4
β’ (π = β
β βπ₯ β π π β ((neiβπ½)β{π₯})) |
7 | 6 | adantl 480 |
. . 3
β’ ((π½ β Top β§ π = β
) β βπ₯ β π π β ((neiβπ½)β{π₯})) |
8 | 5, 7 | 2thd 264 |
. 2
β’ ((π½ β Top β§ π = β
) β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
9 | | opnneip 22843 |
. . . . . . 7
β’ ((π½ β Top β§ π β π½ β§ π₯ β π) β π β ((neiβπ½)β{π₯})) |
10 | 9 | 3expia 1119 |
. . . . . 6
β’ ((π½ β Top β§ π β π½) β (π₯ β π β π β ((neiβπ½)β{π₯}))) |
11 | 10 | ralrimiv 3143 |
. . . . 5
β’ ((π½ β Top β§ π β π½) β βπ₯ β π π β ((neiβπ½)β{π₯})) |
12 | 11 | ex 411 |
. . . 4
β’ (π½ β Top β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
13 | 12 | adantr 479 |
. . 3
β’ ((π½ β Top β§ Β¬ π = β
) β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
14 | | df-ne 2939 |
. . . . . 6
β’ (π β β
β Β¬ π = β
) |
15 | | r19.2z 4493 |
. . . . . . 7
β’ ((π β β
β§
βπ₯ β π π β ((neiβπ½)β{π₯})) β βπ₯ β π π β ((neiβπ½)β{π₯})) |
16 | 15 | ex 411 |
. . . . . 6
β’ (π β β
β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
17 | 14, 16 | sylbir 234 |
. . . . 5
β’ (Β¬
π = β
β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
18 | | eqid 2730 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
19 | 18 | neii1 22830 |
. . . . . . 7
β’ ((π½ β Top β§ π β ((neiβπ½)β{π₯})) β π β βͺ π½) |
20 | 19 | ex 411 |
. . . . . 6
β’ (π½ β Top β (π β ((neiβπ½)β{π₯}) β π β βͺ π½)) |
21 | 20 | rexlimdvw 3158 |
. . . . 5
β’ (π½ β Top β (βπ₯ β π π β ((neiβπ½)β{π₯}) β π β βͺ π½)) |
22 | 17, 21 | sylan9r 507 |
. . . 4
β’ ((π½ β Top β§ Β¬ π = β
) β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β π β βͺ π½)) |
23 | 18 | ntrss2 22781 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β βͺ π½)
β ((intβπ½)βπ) β π) |
24 | 23 | adantr 479 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β βͺ π½)
β§ βπ₯ β
π {π₯} β ((intβπ½)βπ)) β ((intβπ½)βπ) β π) |
25 | | vex 3476 |
. . . . . . . . . . . . 13
β’ π₯ β V |
26 | 25 | snss 4788 |
. . . . . . . . . . . 12
β’ (π₯ β ((intβπ½)βπ) β {π₯} β ((intβπ½)βπ)) |
27 | 26 | ralbii 3091 |
. . . . . . . . . . 11
β’
(βπ₯ β
π π₯ β ((intβπ½)βπ) β βπ₯ β π {π₯} β ((intβπ½)βπ)) |
28 | | dfss3 3969 |
. . . . . . . . . . . . 13
β’ (π β ((intβπ½)βπ) β βπ₯ β π π₯ β ((intβπ½)βπ)) |
29 | 28 | biimpri 227 |
. . . . . . . . . . . 12
β’
(βπ₯ β
π π₯ β ((intβπ½)βπ) β π β ((intβπ½)βπ)) |
30 | 29 | adantl 480 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ π β βͺ π½)
β§ βπ₯ β
π π₯ β ((intβπ½)βπ)) β π β ((intβπ½)βπ)) |
31 | 27, 30 | sylan2br 593 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β βͺ π½)
β§ βπ₯ β
π {π₯} β ((intβπ½)βπ)) β π β ((intβπ½)βπ)) |
32 | 24, 31 | eqssd 3998 |
. . . . . . . . 9
β’ (((π½ β Top β§ π β βͺ π½)
β§ βπ₯ β
π {π₯} β ((intβπ½)βπ)) β ((intβπ½)βπ) = π) |
33 | 32 | ex 411 |
. . . . . . . 8
β’ ((π½ β Top β§ π β βͺ π½)
β (βπ₯ β
π {π₯} β ((intβπ½)βπ) β ((intβπ½)βπ) = π)) |
34 | 25 | snss 4788 |
. . . . . . . . . . . 12
β’ (π₯ β π β {π₯} β π) |
35 | | sstr2 3988 |
. . . . . . . . . . . . . 14
β’ ({π₯} β π β (π β βͺ π½ β {π₯} β βͺ π½)) |
36 | 35 | com12 32 |
. . . . . . . . . . . . 13
β’ (π β βͺ π½
β ({π₯} β π β {π₯} β βͺ π½)) |
37 | 36 | adantl 480 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π β βͺ π½)
β ({π₯} β π β {π₯} β βͺ π½)) |
38 | 34, 37 | biimtrid 241 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β βͺ π½)
β (π₯ β π β {π₯} β βͺ π½)) |
39 | 38 | imp 405 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β βͺ π½)
β§ π₯ β π) β {π₯} β βͺ π½) |
40 | 18 | neiint 22828 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ {π₯} β βͺ π½
β§ π β βͺ π½)
β (π β
((neiβπ½)β{π₯}) β {π₯} β ((intβπ½)βπ))) |
41 | 40 | 3com23 1124 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β βͺ π½
β§ {π₯} β βͺ π½)
β (π β
((neiβπ½)β{π₯}) β {π₯} β ((intβπ½)βπ))) |
42 | 41 | 3expa 1116 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π β βͺ π½)
β§ {π₯} β βͺ π½)
β (π β
((neiβπ½)β{π₯}) β {π₯} β ((intβπ½)βπ))) |
43 | 39, 42 | syldan 589 |
. . . . . . . . 9
β’ (((π½ β Top β§ π β βͺ π½)
β§ π₯ β π) β (π β ((neiβπ½)β{π₯}) β {π₯} β ((intβπ½)βπ))) |
44 | 43 | ralbidva 3173 |
. . . . . . . 8
β’ ((π½ β Top β§ π β βͺ π½)
β (βπ₯ β
π π β ((neiβπ½)β{π₯}) β βπ₯ β π {π₯} β ((intβπ½)βπ))) |
45 | 18 | isopn3 22790 |
. . . . . . . 8
β’ ((π½ β Top β§ π β βͺ π½)
β (π β π½ β ((intβπ½)βπ) = π)) |
46 | 33, 44, 45 | 3imtr4d 293 |
. . . . . . 7
β’ ((π½ β Top β§ π β βͺ π½)
β (βπ₯ β
π π β ((neiβπ½)β{π₯}) β π β π½)) |
47 | 46 | ex 411 |
. . . . . 6
β’ (π½ β Top β (π β βͺ π½
β (βπ₯ β
π π β ((neiβπ½)β{π₯}) β π β π½))) |
48 | 47 | com23 86 |
. . . . 5
β’ (π½ β Top β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β (π β βͺ π½ β π β π½))) |
49 | 48 | adantr 479 |
. . . 4
β’ ((π½ β Top β§ Β¬ π = β
) β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β (π β βͺ π½ β π β π½))) |
50 | 22, 49 | mpdd 43 |
. . 3
β’ ((π½ β Top β§ Β¬ π = β
) β
(βπ₯ β π π β ((neiβπ½)β{π₯}) β π β π½)) |
51 | 13, 50 | impbid 211 |
. 2
β’ ((π½ β Top β§ Β¬ π = β
) β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) |
52 | 8, 51 | pm2.61dan 809 |
1
β’ (π½ β Top β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) |