Proof of Theorem disjpr2
Step | Hyp | Ref
| Expression |
1 | | df-pr 4564 |
. . . 4
⊢ {𝐶, 𝐷} = ({𝐶} ∪ {𝐷}) |
2 | 1 | ineq2i 4143 |
. . 3
⊢ ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ({𝐴, 𝐵} ∩ ({𝐶} ∪ {𝐷})) |
3 | | indi 4207 |
. . 3
⊢ ({𝐴, 𝐵} ∩ ({𝐶} ∪ {𝐷})) = (({𝐴, 𝐵} ∩ {𝐶}) ∪ ({𝐴, 𝐵} ∩ {𝐷})) |
4 | 2, 3 | eqtri 2766 |
. 2
⊢ ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = (({𝐴, 𝐵} ∩ {𝐶}) ∪ ({𝐴, 𝐵} ∩ {𝐷})) |
5 | | df-pr 4564 |
. . . . . . . 8
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
6 | 5 | ineq1i 4142 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ∩ {𝐶}) = (({𝐴} ∪ {𝐵}) ∩ {𝐶}) |
7 | | indir 4209 |
. . . . . . 7
⊢ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = (({𝐴} ∩ {𝐶}) ∪ ({𝐵} ∩ {𝐶})) |
8 | 6, 7 | eqtri 2766 |
. . . . . 6
⊢ ({𝐴, 𝐵} ∩ {𝐶}) = (({𝐴} ∩ {𝐶}) ∪ ({𝐵} ∩ {𝐶})) |
9 | | disjsn2 4648 |
. . . . . . . 8
⊢ (𝐴 ≠ 𝐶 → ({𝐴} ∩ {𝐶}) = ∅) |
10 | | disjsn2 4648 |
. . . . . . . 8
⊢ (𝐵 ≠ 𝐶 → ({𝐵} ∩ {𝐶}) = ∅) |
11 | 9, 10 | anim12i 613 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅)) |
12 | | un00 4376 |
. . . . . . 7
⊢ ((({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅) ↔ (({𝐴} ∩ {𝐶}) ∪ ({𝐵} ∩ {𝐶})) = ∅) |
13 | 11, 12 | sylib 217 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∩ {𝐶}) ∪ ({𝐵} ∩ {𝐶})) = ∅) |
14 | 8, 13 | eqtrid 2790 |
. . . . 5
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∩ {𝐶}) = ∅) |
15 | 14 | adantr 481 |
. . . 4
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐶}) = ∅) |
16 | 5 | ineq1i 4142 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ∩ {𝐷}) = (({𝐴} ∪ {𝐵}) ∩ {𝐷}) |
17 | | indir 4209 |
. . . . . . 7
⊢ (({𝐴} ∪ {𝐵}) ∩ {𝐷}) = (({𝐴} ∩ {𝐷}) ∪ ({𝐵} ∩ {𝐷})) |
18 | 16, 17 | eqtri 2766 |
. . . . . 6
⊢ ({𝐴, 𝐵} ∩ {𝐷}) = (({𝐴} ∩ {𝐷}) ∪ ({𝐵} ∩ {𝐷})) |
19 | | disjsn2 4648 |
. . . . . . . 8
⊢ (𝐴 ≠ 𝐷 → ({𝐴} ∩ {𝐷}) = ∅) |
20 | | disjsn2 4648 |
. . . . . . . 8
⊢ (𝐵 ≠ 𝐷 → ({𝐵} ∩ {𝐷}) = ∅) |
21 | 19, 20 | anim12i 613 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷) → (({𝐴} ∩ {𝐷}) = ∅ ∧ ({𝐵} ∩ {𝐷}) = ∅)) |
22 | | un00 4376 |
. . . . . . 7
⊢ ((({𝐴} ∩ {𝐷}) = ∅ ∧ ({𝐵} ∩ {𝐷}) = ∅) ↔ (({𝐴} ∩ {𝐷}) ∪ ({𝐵} ∩ {𝐷})) = ∅) |
23 | 21, 22 | sylib 217 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷) → (({𝐴} ∩ {𝐷}) ∪ ({𝐵} ∩ {𝐷})) = ∅) |
24 | 18, 23 | eqtrid 2790 |
. . . . 5
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷) → ({𝐴, 𝐵} ∩ {𝐷}) = ∅) |
25 | 24 | adantl 482 |
. . . 4
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐷}) = ∅) |
26 | 15, 25 | uneq12d 4098 |
. . 3
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → (({𝐴, 𝐵} ∩ {𝐶}) ∪ ({𝐴, 𝐵} ∩ {𝐷})) = (∅ ∪
∅)) |
27 | | un0 4324 |
. . 3
⊢ (∅
∪ ∅) = ∅ |
28 | 26, 27 | eqtrdi 2794 |
. 2
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → (({𝐴, 𝐵} ∩ {𝐶}) ∪ ({𝐴, 𝐵} ∩ {𝐷})) = ∅) |
29 | 4, 28 | eqtrid 2790 |
1
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅) |