Step | Hyp | Ref
| Expression |
1 | | difundi 4243 |
. . . . . 6
β’ (π β (π΄ βͺ π΅)) = ((π β π΄) β© (π β π΅)) |
2 | 1 | fveq2i 6849 |
. . . . 5
β’
((intβπ½)β(π β (π΄ βͺ π΅))) = ((intβπ½)β((π β π΄) β© (π β π΅))) |
3 | | difss 4095 |
. . . . . . 7
β’ (π β π΄) β π |
4 | | difss 4095 |
. . . . . . 7
β’ (π β π΅) β π |
5 | | clsun.1 |
. . . . . . . 8
β’ π = βͺ
π½ |
6 | 5 | ntrin 22435 |
. . . . . . 7
β’ ((π½ β Top β§ (π β π΄) β π β§ (π β π΅) β π) β ((intβπ½)β((π β π΄) β© (π β π΅))) = (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅)))) |
7 | 3, 4, 6 | mp3an23 1454 |
. . . . . 6
β’ (π½ β Top β
((intβπ½)β((π β π΄) β© (π β π΅))) = (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅)))) |
8 | 7 | 3ad2ant1 1134 |
. . . . 5
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β((π β π΄) β© (π β π΅))) = (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅)))) |
9 | 2, 8 | eqtrid 2785 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β(π β (π΄ βͺ π΅))) = (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅)))) |
10 | | simp1 1137 |
. . . . 5
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β π½ β Top) |
11 | | unss 4148 |
. . . . . . 7
β’ ((π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) |
12 | 11 | biimpi 215 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) |
13 | 12 | 3adant1 1131 |
. . . . 5
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β π) |
14 | 5 | ntrdif 22426 |
. . . . 5
β’ ((π½ β Top β§ (π΄ βͺ π΅) β π) β ((intβπ½)β(π β (π΄ βͺ π΅))) = (π β ((clsβπ½)β(π΄ βͺ π΅)))) |
15 | 10, 13, 14 | syl2anc 585 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β(π β (π΄ βͺ π΅))) = (π β ((clsβπ½)β(π΄ βͺ π΅)))) |
16 | 5 | ntrdif 22426 |
. . . . . . 7
β’ ((π½ β Top β§ π΄ β π) β ((intβπ½)β(π β π΄)) = (π β ((clsβπ½)βπ΄))) |
17 | 16 | 3adant3 1133 |
. . . . . 6
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β(π β π΄)) = (π β ((clsβπ½)βπ΄))) |
18 | 5 | ntrdif 22426 |
. . . . . . 7
β’ ((π½ β Top β§ π΅ β π) β ((intβπ½)β(π β π΅)) = (π β ((clsβπ½)βπ΅))) |
19 | 18 | 3adant2 1132 |
. . . . . 6
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((intβπ½)β(π β π΅)) = (π β ((clsβπ½)βπ΅))) |
20 | 17, 19 | ineq12d 4177 |
. . . . 5
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅))) = ((π β ((clsβπ½)βπ΄)) β© (π β ((clsβπ½)βπ΅)))) |
21 | | difundi 4243 |
. . . . 5
β’ (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) = ((π β ((clsβπ½)βπ΄)) β© (π β ((clsβπ½)βπ΅))) |
22 | 20, 21 | eqtr4di 2791 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (((intβπ½)β(π β π΄)) β© ((intβπ½)β(π β π΅))) = (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)))) |
23 | 9, 15, 22 | 3eqtr3d 2781 |
. . 3
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (π β ((clsβπ½)β(π΄ βͺ π΅))) = (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)))) |
24 | 23 | difeq2d 4086 |
. 2
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (π β (π β ((clsβπ½)β(π΄ βͺ π΅)))) = (π β (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))))) |
25 | 5 | clscld 22421 |
. . . . 5
β’ ((π½ β Top β§ (π΄ βͺ π΅) β π) β ((clsβπ½)β(π΄ βͺ π΅)) β (Clsdβπ½)) |
26 | 10, 13, 25 | syl2anc 585 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) β (Clsdβπ½)) |
27 | 5 | cldss 22403 |
. . . 4
β’
(((clsβπ½)β(π΄ βͺ π΅)) β (Clsdβπ½) β ((clsβπ½)β(π΄ βͺ π΅)) β π) |
28 | 26, 27 | syl 17 |
. . 3
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) β π) |
29 | | dfss4 4222 |
. . 3
β’
(((clsβπ½)β(π΄ βͺ π΅)) β π β (π β (π β ((clsβπ½)β(π΄ βͺ π΅)))) = ((clsβπ½)β(π΄ βͺ π΅))) |
30 | 28, 29 | sylib 217 |
. 2
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (π β (π β ((clsβπ½)β(π΄ βͺ π΅)))) = ((clsβπ½)β(π΄ βͺ π΅))) |
31 | 5 | clsss3 22433 |
. . . . 5
β’ ((π½ β Top β§ π΄ β π) β ((clsβπ½)βπ΄) β π) |
32 | 31 | 3adant3 1133 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)βπ΄) β π) |
33 | 5 | clsss3 22433 |
. . . . 5
β’ ((π½ β Top β§ π΅ β π) β ((clsβπ½)βπ΅) β π) |
34 | 33 | 3adant2 1132 |
. . . 4
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)βπ΅) β π) |
35 | 32, 34 | jca 513 |
. . 3
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (((clsβπ½)βπ΄) β π β§ ((clsβπ½)βπ΅) β π)) |
36 | | unss 4148 |
. . . 4
β’
((((clsβπ½)βπ΄) β π β§ ((clsβπ½)βπ΅) β π) β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)) β π) |
37 | | dfss4 4222 |
. . . 4
β’
((((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)) β π β (π β (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)))) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) |
38 | 36, 37 | bitri 275 |
. . 3
β’
((((clsβπ½)βπ΄) β π β§ ((clsβπ½)βπ΅) β π) β (π β (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)))) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) |
39 | 35, 38 | sylib 217 |
. 2
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β (π β (π β (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅)))) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) |
40 | 24, 30, 39 | 3eqtr3d 2781 |
1
β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) |