Proof of Theorem dfif5
Step | Hyp | Ref
| Expression |
1 | | inindi 4160 |
. 2
⊢ ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶))) = (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶))) |
2 | | dfif3.1 |
. . 3
⊢ 𝐶 = {𝑥 ∣ 𝜑} |
3 | 2 | dfif4 4474 |
. 2
⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((𝐴 ∪ (V ∖ 𝐶)) ∩ (𝐵 ∪ 𝐶))) |
4 | | undir 4210 |
. . 3
⊢ ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))) |
5 | | unidm 4086 |
. . . . . . . 8
⊢ (𝐴 ∪ 𝐴) = 𝐴 |
6 | 5 | uneq1i 4093 |
. . . . . . 7
⊢ ((𝐴 ∪ 𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))) |
7 | | unass 4100 |
. . . . . . 7
⊢ ((𝐴 ∪ 𝐴) ∪ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))) |
8 | | undi 4208 |
. . . . . . 7
⊢ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) |
9 | 6, 7, 8 | 3eqtr3ri 2775 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))) |
10 | | undi 4208 |
. . . . . . . 8
⊢ (𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = ((𝐴 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐴 ∪ 𝐶)) |
11 | | undifabs 4411 |
. . . . . . . . 9
⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
12 | 11 | ineq1i 4142 |
. . . . . . . 8
⊢ ((𝐴 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐴 ∪ 𝐶)) = (𝐴 ∩ (𝐴 ∪ 𝐶)) |
13 | | inabs 4189 |
. . . . . . . 8
⊢ (𝐴 ∩ (𝐴 ∪ 𝐶)) = 𝐴 |
14 | 10, 12, 13 | 3eqtri 2770 |
. . . . . . 7
⊢ (𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = 𝐴 |
15 | | undif2 4410 |
. . . . . . . . 9
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
16 | 15 | ineq1i 4142 |
. . . . . . . 8
⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) |
17 | | undi 4208 |
. . . . . . . 8
⊢ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = ((𝐴 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐴 ∪ (V ∖ 𝐶))) |
18 | 16, 17, 8 | 3eqtr4i 2776 |
. . . . . . 7
⊢ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶))) |
19 | 14, 18 | uneq12i 4095 |
. . . . . 6
⊢ ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = (𝐴 ∪ (𝐴 ∪ (𝐵 ∩ (V ∖ 𝐶)))) |
20 | 9, 19 | eqtr4i 2769 |
. . . . 5
⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) |
21 | | unundi 4104 |
. . . . 5
⊢ (𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐴 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐴 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) |
22 | 20, 21 | eqtr4i 2769 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) = (𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) |
23 | | unass 4100 |
. . . . . 6
⊢ (((𝐴 ∩ 𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∪ 𝐵)) |
24 | | undi 4208 |
. . . . . . . . 9
⊢ (𝐵 ∪ (𝐴 ∩ 𝐶)) = ((𝐵 ∪ 𝐴) ∩ (𝐵 ∪ 𝐶)) |
25 | | uncom 4087 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = (𝐵 ∪ (𝐴 ∩ 𝐶)) |
26 | | undif2 4410 |
. . . . . . . . . 10
⊢ (𝐵 ∪ (𝐴 ∖ 𝐵)) = (𝐵 ∪ 𝐴) |
27 | 26 | ineq1i 4142 |
. . . . . . . . 9
⊢ ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶)) = ((𝐵 ∪ 𝐴) ∩ (𝐵 ∪ 𝐶)) |
28 | 24, 25, 27 | 3eqtr4i 2776 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶)) |
29 | | undi 4208 |
. . . . . . . 8
⊢ (𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) = ((𝐵 ∪ (𝐴 ∖ 𝐵)) ∩ (𝐵 ∪ 𝐶)) |
30 | 28, 29 | eqtr4i 2769 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = (𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) |
31 | | undi 4208 |
. . . . . . . 8
⊢ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) = ((𝐵 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶))) |
32 | | undifabs 4411 |
. . . . . . . . 9
⊢ (𝐵 ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
33 | 32 | ineq1i 4142 |
. . . . . . . 8
⊢ ((𝐵 ∪ (𝐵 ∖ 𝐴)) ∩ (𝐵 ∪ (V ∖ 𝐶))) = (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶))) |
34 | | inabs 4189 |
. . . . . . . 8
⊢ (𝐵 ∩ (𝐵 ∪ (V ∖ 𝐶))) = 𝐵 |
35 | 31, 33, 34 | 3eqtrri 2771 |
. . . . . . 7
⊢ 𝐵 = (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))) |
36 | 30, 35 | uneq12i 4095 |
. . . . . 6
⊢ (((𝐴 ∩ 𝐶) ∪ 𝐵) ∪ 𝐵) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) |
37 | | unidm 4086 |
. . . . . . 7
⊢ (𝐵 ∪ 𝐵) = 𝐵 |
38 | 37 | uneq2i 4094 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∪ 𝐵)) = ((𝐴 ∩ 𝐶) ∪ 𝐵) |
39 | 23, 36, 38 | 3eqtr3ri 2775 |
. . . . 5
⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) |
40 | | uncom 4087 |
. . . . . . 7
⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵) |
41 | 40 | ineq2i 4143 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐶 ∪ 𝐵)) |
42 | | undir 4210 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐶) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ (𝐶 ∪ 𝐵)) |
43 | 41, 42 | eqtr4i 2769 |
. . . . 5
⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐶) ∪ 𝐵) |
44 | | unundi 4104 |
. . . . 5
⊢ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = ((𝐵 ∪ ((𝐴 ∖ 𝐵) ∩ 𝐶)) ∪ (𝐵 ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) |
45 | 39, 43, 44 | 3eqtr4i 2776 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶)) = (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) |
46 | 22, 45 | ineq12i 4144 |
. . 3
⊢ (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶))) = ((𝐴 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) ∩ (𝐵 ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶))))) |
47 | 4, 46 | eqtr4i 2769 |
. 2
⊢ ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) = (((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ (V ∖ 𝐶))) ∩ ((𝐴 ∪ 𝐵) ∩ (𝐵 ∪ 𝐶))) |
48 | 1, 3, 47 | 3eqtr4i 2776 |
1
⊢ if(𝜑, 𝐴, 𝐵) = ((𝐴 ∩ 𝐵) ∪ (((𝐴 ∖ 𝐵) ∩ 𝐶) ∪ ((𝐵 ∖ 𝐴) ∩ (V ∖ 𝐶)))) |