Step | Hyp | Ref
| Expression |
1 | | difundi 4279 |
. . . . . 6
β’ (π β (π΄ βͺ π΅)) = ((π β π΄) β© (π β π΅)) |
2 | 1 | fveq2i 6894 |
. . . . 5
β’
((intβπ½)β(π β (π΄ βͺ π΅))) = ((intβπ½)β((π β π΄) β© (π β π΅))) |
3 | | difss 4131 |
. . . . . . 7
β’ (π β π΄) β π |
4 | | difss 4131 |
. . . . . . 7
β’ (π β π΅) β π |
5 | | clsun.1 |
. . . . . . . 8
β’ π = βͺ
π½ |
6 | 5 | ntrin 22564 |
. . . . . . 7
β’ ((π½ β Top β§ (π β π΄) β π β§ (π β π΅) β π) β ((intβπ½)β((π β π΄) β© (π β π΅))) = (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅)))) |
7 | 3, 4, 6 | mp3an23 1453 |
. . . . . 6
β’ (π½ β Top β
((intβπ½)β((π β π΄) β© (π β π΅))) = (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅)))) |
8 | 7 | 3ad2ant1 1133 |
. . . . 5
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β((π β π΄) β© (π β π΅))) = (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅)))) |
9 | 2, 8 | eqtrid 2784 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β(π β (π΄ βͺ π΅))) = (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅)))) |
10 | | simp1 1136 |
. . . . 5
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β π½ β Top) |
11 | | unss 4184 |
. . . . . . 7
β’ ((π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) |
12 | 11 | biimpi 215 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) |
13 | 12 | 3adant1 1130 |
. . . . 5
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) |
14 | 5 | ntrdif 22555 |
. . . . 5
β’ ((π½ β Top β§ (π΄ βͺ π΅) β π) β ((intβπ½)β(π β (π΄ βͺ π΅))) = (π β ((clsβπ½)β(π΄ βͺ π΅)))) |
15 | 10, 13, 14 | syl2anc 584 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β(π β (π΄ βͺ π΅))) = (π β ((clsβπ½)β(π΄ βͺ π΅)))) |
16 | 5 | ntrdif 22555 |
. . . . . . 7
β’ ((π½ β Top β§ π΄ β π) β ((intβπ½)β(π β π΄)) = (π β ((clsβπ½)βπ΄))) |
17 | 16 | 3adant3 1132 |
. . . . . 6
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β(π β π΄)) = (π β ((clsβπ½)βπ΄))) |
18 | 5 | ntrdif 22555 |
. . . . . . 7
β’ ((π½ β Top β§ π΅ β π) β ((intβπ½)β(π β π΅)) = (π β ((clsβπ½)βπ΅))) |
19 | 18 | 3adant2 1131 |
. . . . . 6
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β(π β π΅)) = (π β ((clsβπ½)βπ΅))) |
20 | 17, 19 | ineq12d 4213 |
. . . . 5
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅))) = ((π β ((clsβπ½)βπ΄)) β© (π β ((clsβπ½)βπ΅)))) |
21 | | difundi 4279 |
. . . . 5
β’ (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) = ((π β ((clsβπ½)βπ΄)) β© (π β ((clsβπ½)βπ΅))) |
22 | 20, 21 | eqtr4di 2790 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅))) = (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)))) |
23 | 9, 15, 22 | 3eqtr3d 2780 |
. . 3
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (π β ((clsβπ½)β(π΄ βͺ π΅))) = (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)))) |
24 | 23 | difeq2d 4122 |
. 2
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (π β (π β ((clsβπ½)β(π΄ βͺ π΅)))) = (π β (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))))) |
25 | 5 | clscld 22550 |
. . . . 5
β’ ((π½ β Top β§ (π΄ βͺ π΅) β π) β ((clsβπ½)β(π΄ βͺ π΅)) β (Clsdβπ½)) |
26 | 10, 13, 25 | syl2anc 584 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) β (Clsdβπ½)) |
27 | 5 | cldss 22532 |
. . . 4
β’
(((clsβπ½)β(π΄ βͺ π΅)) β (Clsdβπ½) β ((clsβπ½)β(π΄ βͺ π΅)) β π) |
28 | 26, 27 | syl 17 |
. . 3
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) β π) |
29 | | dfss4 4258 |
. . 3
β’
(((clsβπ½)β(π΄ βͺ π΅)) β π β (π β (π β ((clsβπ½)β(π΄ βͺ π΅)))) = ((clsβπ½)β(π΄ βͺ π΅))) |
30 | 28, 29 | sylib 217 |
. 2
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (π β (π β ((clsβπ½)β(π΄ βͺ π΅)))) = ((clsβπ½)β(π΄ βͺ π΅))) |
31 | 5 | clsss3 22562 |
. . . . 5
β’ ((π½ β Top β§ π΄ β π) β ((clsβπ½)βπ΄) β π) |
32 | 31 | 3adant3 1132 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)βπ΄) β π) |
33 | 5 | clsss3 22562 |
. . . . 5
β’ ((π½ β Top β§ π΅ β π) β ((clsβπ½)βπ΅) β π) |
34 | 33 | 3adant2 1131 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)βπ΅) β π) |
35 | 32, 34 | jca 512 |
. . 3
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (((clsβπ½)βπ΄) β π β§ ((clsβπ½)βπ΅) β π)) |
36 | | unss 4184 |
. . . 4
β’
((((clsβπ½)βπ΄) β π β§ ((clsβπ½)βπ΅) β π) β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)) β π) |
37 | | dfss4 4258 |
. . . 4
β’
((((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)) β π β (π β (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)))) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) |
38 | 36, 37 | bitri 274 |
. . 3
β’
((((clsβπ½)βπ΄) β π β§ ((clsβπ½)βπ΅) β π) β (π β (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)))) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) |
39 | 35, 38 | sylib 217 |
. 2
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (π β (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)))) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) |
40 | 24, 30, 39 | 3eqtr3d 2780 |
1
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) |