Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . 7
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄)) β π β ((neiβπ½)βπ΄)) |
2 | | simpl 484 |
. . . . . . . 8
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄)) β π½ β Top) |
3 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
4 | 3 | neiss2 22605 |
. . . . . . . 8
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄)) β π΄ β βͺ π½) |
5 | 3 | neii1 22610 |
. . . . . . . 8
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄)) β π β βͺ π½) |
6 | 3 | neiint 22608 |
. . . . . . . 8
β’ ((π½ β Top β§ π΄ β βͺ π½
β§ π β βͺ π½)
β (π β
((neiβπ½)βπ΄) β π΄ β ((intβπ½)βπ))) |
7 | 2, 4, 5, 6 | syl3anc 1372 |
. . . . . . 7
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄)) β (π β ((neiβπ½)βπ΄) β π΄ β ((intβπ½)βπ))) |
8 | 1, 7 | mpbid 231 |
. . . . . 6
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄)) β π΄ β ((intβπ½)βπ)) |
9 | | ssinss1 4238 |
. . . . . 6
β’ (π΄ β ((intβπ½)βπ) β (π΄ β© π΅) β ((intβπ½)βπ)) |
10 | 8, 9 | syl 17 |
. . . . 5
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄)) β (π΄ β© π΅) β ((intβπ½)βπ)) |
11 | 10 | 3adant3 1133 |
. . . 4
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β (π΄ β© π΅) β ((intβπ½)βπ)) |
12 | | inss2 4230 |
. . . . 5
β’ (π΄ β© π΅) β π΅ |
13 | | simpr 486 |
. . . . . . 7
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΅)) β π β ((neiβπ½)βπ΅)) |
14 | | simpl 484 |
. . . . . . . 8
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΅)) β π½ β Top) |
15 | 3 | neiss2 22605 |
. . . . . . . 8
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΅)) β π΅ β βͺ π½) |
16 | 3 | neii1 22610 |
. . . . . . . 8
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΅)) β π β βͺ π½) |
17 | 3 | neiint 22608 |
. . . . . . . 8
β’ ((π½ β Top β§ π΅ β βͺ π½
β§ π β βͺ π½)
β (π β
((neiβπ½)βπ΅) β π΅ β ((intβπ½)βπ))) |
18 | 14, 15, 16, 17 | syl3anc 1372 |
. . . . . . 7
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΅)) β (π β ((neiβπ½)βπ΅) β π΅ β ((intβπ½)βπ))) |
19 | 13, 18 | mpbid 231 |
. . . . . 6
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΅)) β π΅ β ((intβπ½)βπ)) |
20 | 19 | 3adant2 1132 |
. . . . 5
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β π΅ β ((intβπ½)βπ)) |
21 | 12, 20 | sstrid 3994 |
. . . 4
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β (π΄ β© π΅) β ((intβπ½)βπ)) |
22 | 11, 21 | ssind 4233 |
. . 3
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β (π΄ β© π΅) β (((intβπ½)βπ) β© ((intβπ½)βπ))) |
23 | | simp1 1137 |
. . . 4
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β π½ β Top) |
24 | 5 | 3adant3 1133 |
. . . 4
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β π β βͺ π½) |
25 | 16 | 3adant2 1132 |
. . . 4
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β π β βͺ π½) |
26 | 3 | ntrin 22565 |
. . . 4
β’ ((π½ β Top β§ π β βͺ π½
β§ π β βͺ π½)
β ((intβπ½)β(π β© π)) = (((intβπ½)βπ) β© ((intβπ½)βπ))) |
27 | 23, 24, 25, 26 | syl3anc 1372 |
. . 3
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β ((intβπ½)β(π β© π)) = (((intβπ½)βπ) β© ((intβπ½)βπ))) |
28 | 22, 27 | sseqtrrd 4024 |
. 2
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β (π΄ β© π΅) β ((intβπ½)β(π β© π))) |
29 | | ssinss1 4238 |
. . . . 5
β’ (π΄ β βͺ π½
β (π΄ β© π΅) β βͺ π½) |
30 | 4, 29 | syl 17 |
. . . 4
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄)) β (π΄ β© π΅) β βͺ π½) |
31 | | ssinss1 4238 |
. . . . 5
β’ (π β βͺ π½
β (π β© π) β βͺ π½) |
32 | 5, 31 | syl 17 |
. . . 4
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄)) β (π β© π) β βͺ π½) |
33 | 3 | neiint 22608 |
. . . 4
β’ ((π½ β Top β§ (π΄ β© π΅) β βͺ π½ β§ (π β© π) β βͺ π½) β ((π β© π) β ((neiβπ½)β(π΄ β© π΅)) β (π΄ β© π΅) β ((intβπ½)β(π β© π)))) |
34 | 2, 30, 32, 33 | syl3anc 1372 |
. . 3
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄)) β ((π β© π) β ((neiβπ½)β(π΄ β© π΅)) β (π΄ β© π΅) β ((intβπ½)β(π β© π)))) |
35 | 34 | 3adant3 1133 |
. 2
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β ((π β© π) β ((neiβπ½)β(π΄ β© π΅)) β (π΄ β© π΅) β ((intβπ½)β(π β© π)))) |
36 | 28, 35 | mpbird 257 |
1
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β (π β© π) β ((neiβπ½)β(π΄ β© π΅))) |