Proof of Theorem diftpsn3OLD
Step | Hyp | Ref
| Expression |
1 | | df-tp 4130 |
. . . 4
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})) |
3 | 2 | difeq1d 3689 |
. 2
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = (({𝐴, 𝐵} ∪ {𝐶}) ∖ {𝐶})) |
4 | | difundir 3839 |
. . 3
⊢ (({𝐴, 𝐵} ∪ {𝐶}) ∖ {𝐶}) = (({𝐴, 𝐵} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶})) |
5 | 4 | a1i 11 |
. 2
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴, 𝐵} ∪ {𝐶}) ∖ {𝐶}) = (({𝐴, 𝐵} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶}))) |
6 | | df-pr 4128 |
. . . . . . . . 9
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
7 | 6 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})) |
8 | 7 | ineq1d 3775 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∩ {𝐶}) = (({𝐴} ∪ {𝐵}) ∩ {𝐶})) |
9 | | incom 3767 |
. . . . . . . . 9
⊢ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = ({𝐶} ∩ ({𝐴} ∪ {𝐵})) |
10 | | indi 3832 |
. . . . . . . . 9
⊢ ({𝐶} ∩ ({𝐴} ∪ {𝐵})) = (({𝐶} ∩ {𝐴}) ∪ ({𝐶} ∩ {𝐵})) |
11 | 9, 10 | eqtri 2632 |
. . . . . . . 8
⊢ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = (({𝐶} ∩ {𝐴}) ∪ ({𝐶} ∩ {𝐵})) |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = (({𝐶} ∩ {𝐴}) ∪ ({𝐶} ∩ {𝐵}))) |
13 | | necom 2835 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴) |
14 | | disjsn2 4193 |
. . . . . . . . . . 11
⊢ (𝐶 ≠ 𝐴 → ({𝐶} ∩ {𝐴}) = ∅) |
15 | 13, 14 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝐴 ≠ 𝐶 → ({𝐶} ∩ {𝐴}) = ∅) |
16 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶} ∩ {𝐴}) = ∅) |
17 | | necom 2835 |
. . . . . . . . . . 11
⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵) |
18 | | disjsn2 4193 |
. . . . . . . . . . 11
⊢ (𝐶 ≠ 𝐵 → ({𝐶} ∩ {𝐵}) = ∅) |
19 | 17, 18 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝐵 ≠ 𝐶 → ({𝐶} ∩ {𝐵}) = ∅) |
20 | 19 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶} ∩ {𝐵}) = ∅) |
21 | 16, 20 | uneq12d 3730 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐶} ∩ {𝐴}) ∪ ({𝐶} ∩ {𝐵})) = (∅ ∪
∅)) |
22 | | unidm 3718 |
. . . . . . . 8
⊢ (∅
∪ ∅) = ∅ |
23 | 21, 22 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐶} ∩ {𝐴}) ∪ ({𝐶} ∩ {𝐵})) = ∅) |
24 | 8, 12, 23 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∩ {𝐶}) = ∅) |
25 | | disj3 3973 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∩ {𝐶}) = ∅ ↔ {𝐴, 𝐵} = ({𝐴, 𝐵} ∖ {𝐶})) |
26 | 24, 25 | sylib 207 |
. . . . 5
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵} = ({𝐴, 𝐵} ∖ {𝐶})) |
27 | 26 | eqcomd 2616 |
. . . 4
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∖ {𝐶}) = {𝐴, 𝐵}) |
28 | | difid 3902 |
. . . . 5
⊢ ({𝐶} ∖ {𝐶}) = ∅ |
29 | 28 | a1i 11 |
. . . 4
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶} ∖ {𝐶}) = ∅) |
30 | 27, 29 | uneq12d 3730 |
. . 3
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴, 𝐵} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶})) = ({𝐴, 𝐵} ∪ ∅)) |
31 | | un0 3919 |
. . 3
⊢ ({𝐴, 𝐵} ∪ ∅) = {𝐴, 𝐵} |
32 | 30, 31 | syl6eq 2660 |
. 2
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴, 𝐵} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶})) = {𝐴, 𝐵}) |
33 | 3, 5, 32 | 3eqtrd 2648 |
1
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵}) |