Proof of Theorem diftpsn3
Step | Hyp | Ref
| Expression |
1 | | df-tp 3375 |
. . . 4
⊢ {A, B, 𝐶} = ({A, B} ∪
{𝐶}) |
2 | 1 | a1i 9 |
. . 3
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → {A, B, 𝐶} = ({A, B} ∪
{𝐶})) |
3 | 2 | difeq1d 3055 |
. 2
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → ({A, B, 𝐶} ∖ {𝐶}) = (({A, B} ∪
{𝐶}) ∖ {𝐶})) |
4 | | difundir 3184 |
. . 3
⊢
(({A, B} ∪ {𝐶}) ∖ {𝐶}) = (({A, B} ∖
{𝐶}) ∪ ({𝐶} ∖ {𝐶})) |
5 | 4 | a1i 9 |
. 2
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → (({A, B} ∪
{𝐶}) ∖ {𝐶}) = (({A, B} ∖
{𝐶}) ∪ ({𝐶} ∖ {𝐶}))) |
6 | | df-pr 3374 |
. . . . . . . . 9
⊢ {A, B} =
({A} ∪ {B}) |
7 | 6 | a1i 9 |
. . . . . . . 8
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → {A, B} =
({A} ∪ {B})) |
8 | 7 | ineq1d 3131 |
. . . . . . 7
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → ({A, B} ∩
{𝐶}) = (({A} ∪ {B})
∩ {𝐶})) |
9 | | incom 3123 |
. . . . . . . . 9
⊢
(({A} ∪ {B}) ∩ {𝐶}) = ({𝐶} ∩ ({A} ∪ {B})) |
10 | | indi 3178 |
. . . . . . . . 9
⊢ ({𝐶} ∩ ({A} ∪ {B})) =
(({𝐶} ∩ {A}) ∪ ({𝐶} ∩ {B})) |
11 | 9, 10 | eqtri 2057 |
. . . . . . . 8
⊢
(({A} ∪ {B}) ∩ {𝐶}) = (({𝐶} ∩ {A}) ∪ ({𝐶} ∩ {B})) |
12 | 11 | a1i 9 |
. . . . . . 7
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → (({A} ∪ {B})
∩ {𝐶}) = (({𝐶} ∩ {A}) ∪ ({𝐶} ∩ {B}))) |
13 | | necom 2283 |
. . . . . . . . . . 11
⊢ (A ≠ 𝐶 ↔ 𝐶 ≠ A) |
14 | | disjsn2 3424 |
. . . . . . . . . . 11
⊢ (𝐶 ≠ A → ({𝐶} ∩ {A}) = ∅) |
15 | 13, 14 | sylbi 114 |
. . . . . . . . . 10
⊢ (A ≠ 𝐶 → ({𝐶} ∩ {A}) = ∅) |
16 | 15 | adantr 261 |
. . . . . . . . 9
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → ({𝐶} ∩ {A}) = ∅) |
17 | | necom 2283 |
. . . . . . . . . . 11
⊢ (B ≠ 𝐶 ↔ 𝐶 ≠ B) |
18 | | disjsn2 3424 |
. . . . . . . . . . 11
⊢ (𝐶 ≠ B → ({𝐶} ∩ {B}) = ∅) |
19 | 17, 18 | sylbi 114 |
. . . . . . . . . 10
⊢ (B ≠ 𝐶 → ({𝐶} ∩ {B}) = ∅) |
20 | 19 | adantl 262 |
. . . . . . . . 9
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → ({𝐶} ∩ {B}) = ∅) |
21 | 16, 20 | uneq12d 3092 |
. . . . . . . 8
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → (({𝐶} ∩ {A}) ∪ ({𝐶} ∩ {B})) = (∅ ∪ ∅)) |
22 | | unidm 3080 |
. . . . . . . 8
⊢ (∅
∪ ∅) = ∅ |
23 | 21, 22 | syl6eq 2085 |
. . . . . . 7
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → (({𝐶} ∩ {A}) ∪ ({𝐶} ∩ {B})) = ∅) |
24 | 8, 12, 23 | 3eqtrd 2073 |
. . . . . 6
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → ({A, B} ∩
{𝐶}) =
∅) |
25 | | disj3 3266 |
. . . . . 6
⊢
(({A, B} ∩ {𝐶}) = ∅ ↔ {A, B} =
({A, B}
∖ {𝐶})) |
26 | 24, 25 | sylib 127 |
. . . . 5
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → {A, B} =
({A, B}
∖ {𝐶})) |
27 | 26 | eqcomd 2042 |
. . . 4
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → ({A, B} ∖
{𝐶}) = {A, B}) |
28 | | difid 3286 |
. . . . 5
⊢ ({𝐶} ∖ {𝐶}) = ∅ |
29 | 28 | a1i 9 |
. . . 4
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → ({𝐶} ∖ {𝐶}) = ∅) |
30 | 27, 29 | uneq12d 3092 |
. . 3
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → (({A, B} ∖
{𝐶}) ∪ ({𝐶} ∖ {𝐶})) = ({A, B} ∪
∅)) |
31 | | un0 3245 |
. . 3
⊢
({A, B} ∪ ∅) = {A, B} |
32 | 30, 31 | syl6eq 2085 |
. 2
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → (({A, B} ∖
{𝐶}) ∪ ({𝐶} ∖ {𝐶})) = {A, B}) |
33 | 3, 5, 32 | 3eqtrd 2073 |
1
⊢
((A ≠ 𝐶 ∧ B ≠ 𝐶) → ({A, B, 𝐶} ∖ {𝐶}) = {A,
B}) |