Step | Hyp | Ref
| Expression |
1 | | inindi 4190 |
. 2
β’ ((π΄ βͺ π΅) β© ((π΄ βͺ (V β πΆ)) β© (π΅ βͺ πΆ))) = (((π΄ βͺ π΅) β© (π΄ βͺ (V β πΆ))) β© ((π΄ βͺ π΅) β© (π΅ βͺ πΆ))) |
2 | | dfif3.1 |
. . 3
β’ πΆ = {π₯ β£ π} |
3 | 2 | dfif4 4505 |
. 2
β’ if(π, π΄, π΅) = ((π΄ βͺ π΅) β© ((π΄ βͺ (V β πΆ)) β© (π΅ βͺ πΆ))) |
4 | | undir 4240 |
. . 3
β’ ((π΄ β© π΅) βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ)))) = ((π΄ βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ)))) β© (π΅ βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ))))) |
5 | | unidm 4116 |
. . . . . . . 8
β’ (π΄ βͺ π΄) = π΄ |
6 | 5 | uneq1i 4123 |
. . . . . . 7
β’ ((π΄ βͺ π΄) βͺ (π΅ β© (V β πΆ))) = (π΄ βͺ (π΅ β© (V β πΆ))) |
7 | | unass 4130 |
. . . . . . 7
β’ ((π΄ βͺ π΄) βͺ (π΅ β© (V β πΆ))) = (π΄ βͺ (π΄ βͺ (π΅ β© (V β πΆ)))) |
8 | | undi 4238 |
. . . . . . 7
β’ (π΄ βͺ (π΅ β© (V β πΆ))) = ((π΄ βͺ π΅) β© (π΄ βͺ (V β πΆ))) |
9 | 6, 7, 8 | 3eqtr3ri 2770 |
. . . . . 6
β’ ((π΄ βͺ π΅) β© (π΄ βͺ (V β πΆ))) = (π΄ βͺ (π΄ βͺ (π΅ β© (V β πΆ)))) |
10 | | undi 4238 |
. . . . . . . 8
β’ (π΄ βͺ ((π΄ β π΅) β© πΆ)) = ((π΄ βͺ (π΄ β π΅)) β© (π΄ βͺ πΆ)) |
11 | | undifabs 4441 |
. . . . . . . . 9
β’ (π΄ βͺ (π΄ β π΅)) = π΄ |
12 | 11 | ineq1i 4172 |
. . . . . . . 8
β’ ((π΄ βͺ (π΄ β π΅)) β© (π΄ βͺ πΆ)) = (π΄ β© (π΄ βͺ πΆ)) |
13 | | inabs 4219 |
. . . . . . . 8
β’ (π΄ β© (π΄ βͺ πΆ)) = π΄ |
14 | 10, 12, 13 | 3eqtri 2765 |
. . . . . . 7
β’ (π΄ βͺ ((π΄ β π΅) β© πΆ)) = π΄ |
15 | | undif2 4440 |
. . . . . . . . 9
β’ (π΄ βͺ (π΅ β π΄)) = (π΄ βͺ π΅) |
16 | 15 | ineq1i 4172 |
. . . . . . . 8
β’ ((π΄ βͺ (π΅ β π΄)) β© (π΄ βͺ (V β πΆ))) = ((π΄ βͺ π΅) β© (π΄ βͺ (V β πΆ))) |
17 | | undi 4238 |
. . . . . . . 8
β’ (π΄ βͺ ((π΅ β π΄) β© (V β πΆ))) = ((π΄ βͺ (π΅ β π΄)) β© (π΄ βͺ (V β πΆ))) |
18 | 16, 17, 8 | 3eqtr4i 2771 |
. . . . . . 7
β’ (π΄ βͺ ((π΅ β π΄) β© (V β πΆ))) = (π΄ βͺ (π΅ β© (V β πΆ))) |
19 | 14, 18 | uneq12i 4125 |
. . . . . 6
β’ ((π΄ βͺ ((π΄ β π΅) β© πΆ)) βͺ (π΄ βͺ ((π΅ β π΄) β© (V β πΆ)))) = (π΄ βͺ (π΄ βͺ (π΅ β© (V β πΆ)))) |
20 | 9, 19 | eqtr4i 2764 |
. . . . 5
β’ ((π΄ βͺ π΅) β© (π΄ βͺ (V β πΆ))) = ((π΄ βͺ ((π΄ β π΅) β© πΆ)) βͺ (π΄ βͺ ((π΅ β π΄) β© (V β πΆ)))) |
21 | | unundi 4134 |
. . . . 5
β’ (π΄ βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ)))) = ((π΄ βͺ ((π΄ β π΅) β© πΆ)) βͺ (π΄ βͺ ((π΅ β π΄) β© (V β πΆ)))) |
22 | 20, 21 | eqtr4i 2764 |
. . . 4
β’ ((π΄ βͺ π΅) β© (π΄ βͺ (V β πΆ))) = (π΄ βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ)))) |
23 | | unass 4130 |
. . . . . 6
β’ (((π΄ β© πΆ) βͺ π΅) βͺ π΅) = ((π΄ β© πΆ) βͺ (π΅ βͺ π΅)) |
24 | | undi 4238 |
. . . . . . . . 9
β’ (π΅ βͺ (π΄ β© πΆ)) = ((π΅ βͺ π΄) β© (π΅ βͺ πΆ)) |
25 | | uncom 4117 |
. . . . . . . . 9
β’ ((π΄ β© πΆ) βͺ π΅) = (π΅ βͺ (π΄ β© πΆ)) |
26 | | undif2 4440 |
. . . . . . . . . 10
β’ (π΅ βͺ (π΄ β π΅)) = (π΅ βͺ π΄) |
27 | 26 | ineq1i 4172 |
. . . . . . . . 9
β’ ((π΅ βͺ (π΄ β π΅)) β© (π΅ βͺ πΆ)) = ((π΅ βͺ π΄) β© (π΅ βͺ πΆ)) |
28 | 24, 25, 27 | 3eqtr4i 2771 |
. . . . . . . 8
β’ ((π΄ β© πΆ) βͺ π΅) = ((π΅ βͺ (π΄ β π΅)) β© (π΅ βͺ πΆ)) |
29 | | undi 4238 |
. . . . . . . 8
β’ (π΅ βͺ ((π΄ β π΅) β© πΆ)) = ((π΅ βͺ (π΄ β π΅)) β© (π΅ βͺ πΆ)) |
30 | 28, 29 | eqtr4i 2764 |
. . . . . . 7
β’ ((π΄ β© πΆ) βͺ π΅) = (π΅ βͺ ((π΄ β π΅) β© πΆ)) |
31 | | undi 4238 |
. . . . . . . 8
β’ (π΅ βͺ ((π΅ β π΄) β© (V β πΆ))) = ((π΅ βͺ (π΅ β π΄)) β© (π΅ βͺ (V β πΆ))) |
32 | | undifabs 4441 |
. . . . . . . . 9
β’ (π΅ βͺ (π΅ β π΄)) = π΅ |
33 | 32 | ineq1i 4172 |
. . . . . . . 8
β’ ((π΅ βͺ (π΅ β π΄)) β© (π΅ βͺ (V β πΆ))) = (π΅ β© (π΅ βͺ (V β πΆ))) |
34 | | inabs 4219 |
. . . . . . . 8
β’ (π΅ β© (π΅ βͺ (V β πΆ))) = π΅ |
35 | 31, 33, 34 | 3eqtrri 2766 |
. . . . . . 7
β’ π΅ = (π΅ βͺ ((π΅ β π΄) β© (V β πΆ))) |
36 | 30, 35 | uneq12i 4125 |
. . . . . 6
β’ (((π΄ β© πΆ) βͺ π΅) βͺ π΅) = ((π΅ βͺ ((π΄ β π΅) β© πΆ)) βͺ (π΅ βͺ ((π΅ β π΄) β© (V β πΆ)))) |
37 | | unidm 4116 |
. . . . . . 7
β’ (π΅ βͺ π΅) = π΅ |
38 | 37 | uneq2i 4124 |
. . . . . 6
β’ ((π΄ β© πΆ) βͺ (π΅ βͺ π΅)) = ((π΄ β© πΆ) βͺ π΅) |
39 | 23, 36, 38 | 3eqtr3ri 2770 |
. . . . 5
β’ ((π΄ β© πΆ) βͺ π΅) = ((π΅ βͺ ((π΄ β π΅) β© πΆ)) βͺ (π΅ βͺ ((π΅ β π΄) β© (V β πΆ)))) |
40 | | uncom 4117 |
. . . . . . 7
β’ (π΅ βͺ πΆ) = (πΆ βͺ π΅) |
41 | 40 | ineq2i 4173 |
. . . . . 6
β’ ((π΄ βͺ π΅) β© (π΅ βͺ πΆ)) = ((π΄ βͺ π΅) β© (πΆ βͺ π΅)) |
42 | | undir 4240 |
. . . . . 6
β’ ((π΄ β© πΆ) βͺ π΅) = ((π΄ βͺ π΅) β© (πΆ βͺ π΅)) |
43 | 41, 42 | eqtr4i 2764 |
. . . . 5
β’ ((π΄ βͺ π΅) β© (π΅ βͺ πΆ)) = ((π΄ β© πΆ) βͺ π΅) |
44 | | unundi 4134 |
. . . . 5
β’ (π΅ βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ)))) = ((π΅ βͺ ((π΄ β π΅) β© πΆ)) βͺ (π΅ βͺ ((π΅ β π΄) β© (V β πΆ)))) |
45 | 39, 43, 44 | 3eqtr4i 2771 |
. . . 4
β’ ((π΄ βͺ π΅) β© (π΅ βͺ πΆ)) = (π΅ βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ)))) |
46 | 22, 45 | ineq12i 4174 |
. . 3
β’ (((π΄ βͺ π΅) β© (π΄ βͺ (V β πΆ))) β© ((π΄ βͺ π΅) β© (π΅ βͺ πΆ))) = ((π΄ βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ)))) β© (π΅ βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ))))) |
47 | 4, 46 | eqtr4i 2764 |
. 2
β’ ((π΄ β© π΅) βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ)))) = (((π΄ βͺ π΅) β© (π΄ βͺ (V β πΆ))) β© ((π΄ βͺ π΅) β© (π΅ βͺ πΆ))) |
48 | 1, 3, 47 | 3eqtr4i 2771 |
1
β’ if(π, π΄, π΅) = ((π΄ β© π΅) βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ)))) |