Proof of Theorem diftpsn3
Step | Hyp | Ref
| Expression |
1 | | df-tp 3406 |
. . . 4
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
2 | 1 | a1i 9 |
. . 3
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})) |
3 | 2 | difeq1d 3089 |
. 2
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = (({𝐴, 𝐵} ∪ {𝐶}) ∖ {𝐶})) |
4 | | difundir 3217 |
. . 3
⊢ (({𝐴, 𝐵} ∪ {𝐶}) ∖ {𝐶}) = (({𝐴, 𝐵} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶})) |
5 | 4 | a1i 9 |
. 2
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴, 𝐵} ∪ {𝐶}) ∖ {𝐶}) = (({𝐴, 𝐵} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶}))) |
6 | | df-pr 3405 |
. . . . . . . . 9
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
7 | 6 | a1i 9 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})) |
8 | 7 | ineq1d 3166 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∩ {𝐶}) = (({𝐴} ∪ {𝐵}) ∩ {𝐶})) |
9 | | incom 3158 |
. . . . . . . . 9
⊢ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = ({𝐶} ∩ ({𝐴} ∪ {𝐵})) |
10 | | indi 3211 |
. . . . . . . . 9
⊢ ({𝐶} ∩ ({𝐴} ∪ {𝐵})) = (({𝐶} ∩ {𝐴}) ∪ ({𝐶} ∩ {𝐵})) |
11 | 9, 10 | eqtri 2101 |
. . . . . . . 8
⊢ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = (({𝐶} ∩ {𝐴}) ∪ ({𝐶} ∩ {𝐵})) |
12 | 11 | a1i 9 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = (({𝐶} ∩ {𝐴}) ∪ ({𝐶} ∩ {𝐵}))) |
13 | | necom 2329 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴) |
14 | | disjsn2 3455 |
. . . . . . . . . . 11
⊢ (𝐶 ≠ 𝐴 → ({𝐶} ∩ {𝐴}) = ∅) |
15 | 13, 14 | sylbi 119 |
. . . . . . . . . 10
⊢ (𝐴 ≠ 𝐶 → ({𝐶} ∩ {𝐴}) = ∅) |
16 | 15 | adantr 270 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶} ∩ {𝐴}) = ∅) |
17 | | necom 2329 |
. . . . . . . . . . 11
⊢ (𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵) |
18 | | disjsn2 3455 |
. . . . . . . . . . 11
⊢ (𝐶 ≠ 𝐵 → ({𝐶} ∩ {𝐵}) = ∅) |
19 | 17, 18 | sylbi 119 |
. . . . . . . . . 10
⊢ (𝐵 ≠ 𝐶 → ({𝐶} ∩ {𝐵}) = ∅) |
20 | 19 | adantl 271 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶} ∩ {𝐵}) = ∅) |
21 | 16, 20 | uneq12d 3127 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐶} ∩ {𝐴}) ∪ ({𝐶} ∩ {𝐵})) = (∅ ∪
∅)) |
22 | | unidm 3115 |
. . . . . . . 8
⊢ (∅
∪ ∅) = ∅ |
23 | 21, 22 | syl6eq 2129 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐶} ∩ {𝐴}) ∪ ({𝐶} ∩ {𝐵})) = ∅) |
24 | 8, 12, 23 | 3eqtrd 2117 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∩ {𝐶}) = ∅) |
25 | | disj3 3296 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∩ {𝐶}) = ∅ ↔ {𝐴, 𝐵} = ({𝐴, 𝐵} ∖ {𝐶})) |
26 | 24, 25 | sylib 120 |
. . . . 5
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {𝐴, 𝐵} = ({𝐴, 𝐵} ∖ {𝐶})) |
27 | 26 | eqcomd 2086 |
. . . 4
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∖ {𝐶}) = {𝐴, 𝐵}) |
28 | | difid 3312 |
. . . . 5
⊢ ({𝐶} ∖ {𝐶}) = ∅ |
29 | 28 | a1i 9 |
. . . 4
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐶} ∖ {𝐶}) = ∅) |
30 | 27, 29 | uneq12d 3127 |
. . 3
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴, 𝐵} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶})) = ({𝐴, 𝐵} ∪ ∅)) |
31 | | un0 3278 |
. . 3
⊢ ({𝐴, 𝐵} ∪ ∅) = {𝐴, 𝐵} |
32 | 30, 31 | syl6eq 2129 |
. 2
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴, 𝐵} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶})) = {𝐴, 𝐵}) |
33 | 3, 5, 32 | 3eqtrd 2117 |
1
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵}) |