Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
2 | 1 | neii1 22601 |
. . . 4
β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β π β βͺ π½) |
3 | | ssinss1 4236 |
. . . 4
β’ (π β βͺ π½
β (π β© π) β βͺ π½) |
4 | 2, 3 | syl 17 |
. . 3
β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β (π β© π) β βͺ π½) |
5 | 4 | 3adant3 1132 |
. 2
β’ ((π½ β Top β§ π β ((neiβπ½)βπ) β§ π β ((neiβπ½)βπ)) β (π β© π) β βͺ π½) |
6 | | neii2 22603 |
. . . . 5
β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β ββ β π½ (π β β β§ β β π)) |
7 | | neii2 22603 |
. . . . 5
β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β βπ£ β π½ (π β π£ β§ π£ β π)) |
8 | 6, 7 | anim12dan 619 |
. . . 4
β’ ((π½ β Top β§ (π β ((neiβπ½)βπ) β§ π β ((neiβπ½)βπ))) β (ββ β π½ (π β β β§ β β π) β§ βπ£ β π½ (π β π£ β§ π£ β π))) |
9 | | inopn 22392 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ β β π½ β§ π£ β π½) β (β β© π£) β π½) |
10 | 9 | 3expa 1118 |
. . . . . . . . . 10
β’ (((π½ β Top β§ β β π½) β§ π£ β π½) β (β β© π£) β π½) |
11 | | ssin 4229 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β π£) β π β (β β© π£)) |
12 | 11 | biimpi 215 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β π£) β π β (β β© π£)) |
13 | | ss2in 4235 |
. . . . . . . . . . . 12
β’ ((β β π β§ π£ β π) β (β β© π£) β (π β© π)) |
14 | 12, 13 | anim12i 613 |
. . . . . . . . . . 11
β’ (((π β β β§ π β π£) β§ (β β π β§ π£ β π)) β (π β (β β© π£) β§ (β β© π£) β (π β© π))) |
15 | 14 | an4s 658 |
. . . . . . . . . 10
β’ (((π β β β§ β β π) β§ (π β π£ β§ π£ β π)) β (π β (β β© π£) β§ (β β© π£) β (π β© π))) |
16 | | sseq2 4007 |
. . . . . . . . . . . 12
β’ (π = (β β© π£) β (π β π β π β (β β© π£))) |
17 | | sseq1 4006 |
. . . . . . . . . . . 12
β’ (π = (β β© π£) β (π β (π β© π) β (β β© π£) β (π β© π))) |
18 | 16, 17 | anbi12d 631 |
. . . . . . . . . . 11
β’ (π = (β β© π£) β ((π β π β§ π β (π β© π)) β (π β (β β© π£) β§ (β β© π£) β (π β© π)))) |
19 | 18 | rspcev 3612 |
. . . . . . . . . 10
β’ (((β β© π£) β π½ β§ (π β (β β© π£) β§ (β β© π£) β (π β© π))) β βπ β π½ (π β π β§ π β (π β© π))) |
20 | 10, 15, 19 | syl2an 596 |
. . . . . . . . 9
β’ ((((π½ β Top β§ β β π½) β§ π£ β π½) β§ ((π β β β§ β β π) β§ (π β π£ β§ π£ β π))) β βπ β π½ (π β π β§ π β (π β© π))) |
21 | 20 | expr 457 |
. . . . . . . 8
β’ ((((π½ β Top β§ β β π½) β§ π£ β π½) β§ (π β β β§ β β π)) β ((π β π£ β§ π£ β π) β βπ β π½ (π β π β§ π β (π β© π)))) |
22 | 21 | an32s 650 |
. . . . . . 7
β’ ((((π½ β Top β§ β β π½) β§ (π β β β§ β β π)) β§ π£ β π½) β ((π β π£ β§ π£ β π) β βπ β π½ (π β π β§ π β (π β© π)))) |
23 | 22 | rexlimdva 3155 |
. . . . . 6
β’ (((π½ β Top β§ β β π½) β§ (π β β β§ β β π)) β (βπ£ β π½ (π β π£ β§ π£ β π) β βπ β π½ (π β π β§ π β (π β© π)))) |
24 | 23 | rexlimdva2 3157 |
. . . . 5
β’ (π½ β Top β (ββ β π½ (π β β β§ β β π) β (βπ£ β π½ (π β π£ β§ π£ β π) β βπ β π½ (π β π β§ π β (π β© π))))) |
25 | 24 | imp32 419 |
. . . 4
β’ ((π½ β Top β§ (ββ β π½ (π β β β§ β β π) β§ βπ£ β π½ (π β π£ β§ π£ β π))) β βπ β π½ (π β π β§ π β (π β© π))) |
26 | 8, 25 | syldan 591 |
. . 3
β’ ((π½ β Top β§ (π β ((neiβπ½)βπ) β§ π β ((neiβπ½)βπ))) β βπ β π½ (π β π β§ π β (π β© π))) |
27 | 26 | 3impb 1115 |
. 2
β’ ((π½ β Top β§ π β ((neiβπ½)βπ) β§ π β ((neiβπ½)βπ)) β βπ β π½ (π β π β§ π β (π β© π))) |
28 | 1 | neiss2 22596 |
. . . 4
β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β π β βͺ π½) |
29 | 1 | isnei 22598 |
. . . 4
β’ ((π½ β Top β§ π β βͺ π½)
β ((π β© π) β ((neiβπ½)βπ) β ((π β© π) β βͺ π½ β§ βπ β π½ (π β π β§ π β (π β© π))))) |
30 | 28, 29 | syldan 591 |
. . 3
β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β ((π β© π) β ((neiβπ½)βπ) β ((π β© π) β βͺ π½ β§ βπ β π½ (π β π β§ π β (π β© π))))) |
31 | 30 | 3adant3 1132 |
. 2
β’ ((π½ β Top β§ π β ((neiβπ½)βπ) β§ π β ((neiβπ½)βπ)) β ((π β© π) β ((neiβπ½)βπ) β ((π β© π) β βͺ π½ β§ βπ β π½ (π β π β§ π β (π β© π))))) |
32 | 5, 27, 31 | mpbir2and 711 |
1
β’ ((π½ β Top β§ π β ((neiβπ½)βπ) β§ π β ((neiβπ½)βπ)) β (π β© π) β ((neiβπ½)βπ)) |