Proof of Theorem disjpr2
| Step | Hyp | Ref
| Expression |
| 1 | | df-pr 4629 |
. . . 4
⊢ {𝐶, 𝐷} = ({𝐶} ∪ {𝐷}) |
| 2 | 1 | ineq2i 4217 |
. . 3
⊢ ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ({𝐴, 𝐵} ∩ ({𝐶} ∪ {𝐷})) |
| 3 | | indi 4284 |
. . 3
⊢ ({𝐴, 𝐵} ∩ ({𝐶} ∪ {𝐷})) = (({𝐴, 𝐵} ∩ {𝐶}) ∪ ({𝐴, 𝐵} ∩ {𝐷})) |
| 4 | 2, 3 | eqtri 2765 |
. 2
⊢ ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = (({𝐴, 𝐵} ∩ {𝐶}) ∪ ({𝐴, 𝐵} ∩ {𝐷})) |
| 5 | | df-pr 4629 |
. . . . . . . 8
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
| 6 | 5 | ineq1i 4216 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ∩ {𝐶}) = (({𝐴} ∪ {𝐵}) ∩ {𝐶}) |
| 7 | | indir 4286 |
. . . . . . 7
⊢ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = (({𝐴} ∩ {𝐶}) ∪ ({𝐵} ∩ {𝐶})) |
| 8 | 6, 7 | eqtri 2765 |
. . . . . 6
⊢ ({𝐴, 𝐵} ∩ {𝐶}) = (({𝐴} ∩ {𝐶}) ∪ ({𝐵} ∩ {𝐶})) |
| 9 | | disjsn2 4712 |
. . . . . . . 8
⊢ (𝐴 ≠ 𝐶 → ({𝐴} ∩ {𝐶}) = ∅) |
| 10 | | disjsn2 4712 |
. . . . . . . 8
⊢ (𝐵 ≠ 𝐶 → ({𝐵} ∩ {𝐶}) = ∅) |
| 11 | 9, 10 | anim12i 613 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅)) |
| 12 | | un00 4445 |
. . . . . . 7
⊢ ((({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅) ↔ (({𝐴} ∩ {𝐶}) ∪ ({𝐵} ∩ {𝐶})) = ∅) |
| 13 | 11, 12 | sylib 218 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝐴} ∩ {𝐶}) ∪ ({𝐵} ∩ {𝐶})) = ∅) |
| 14 | 8, 13 | eqtrid 2789 |
. . . . 5
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} ∩ {𝐶}) = ∅) |
| 15 | 14 | adantr 480 |
. . . 4
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐶}) = ∅) |
| 16 | 5 | ineq1i 4216 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ∩ {𝐷}) = (({𝐴} ∪ {𝐵}) ∩ {𝐷}) |
| 17 | | indir 4286 |
. . . . . . 7
⊢ (({𝐴} ∪ {𝐵}) ∩ {𝐷}) = (({𝐴} ∩ {𝐷}) ∪ ({𝐵} ∩ {𝐷})) |
| 18 | 16, 17 | eqtri 2765 |
. . . . . 6
⊢ ({𝐴, 𝐵} ∩ {𝐷}) = (({𝐴} ∩ {𝐷}) ∪ ({𝐵} ∩ {𝐷})) |
| 19 | | disjsn2 4712 |
. . . . . . . 8
⊢ (𝐴 ≠ 𝐷 → ({𝐴} ∩ {𝐷}) = ∅) |
| 20 | | disjsn2 4712 |
. . . . . . . 8
⊢ (𝐵 ≠ 𝐷 → ({𝐵} ∩ {𝐷}) = ∅) |
| 21 | 19, 20 | anim12i 613 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷) → (({𝐴} ∩ {𝐷}) = ∅ ∧ ({𝐵} ∩ {𝐷}) = ∅)) |
| 22 | | un00 4445 |
. . . . . . 7
⊢ ((({𝐴} ∩ {𝐷}) = ∅ ∧ ({𝐵} ∩ {𝐷}) = ∅) ↔ (({𝐴} ∩ {𝐷}) ∪ ({𝐵} ∩ {𝐷})) = ∅) |
| 23 | 21, 22 | sylib 218 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷) → (({𝐴} ∩ {𝐷}) ∪ ({𝐵} ∩ {𝐷})) = ∅) |
| 24 | 18, 23 | eqtrid 2789 |
. . . . 5
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷) → ({𝐴, 𝐵} ∩ {𝐷}) = ∅) |
| 25 | 24 | adantl 481 |
. . . 4
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐷}) = ∅) |
| 26 | 15, 25 | uneq12d 4169 |
. . 3
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → (({𝐴, 𝐵} ∩ {𝐶}) ∪ ({𝐴, 𝐵} ∩ {𝐷})) = (∅ ∪
∅)) |
| 27 | | un0 4394 |
. . 3
⊢ (∅
∪ ∅) = ∅ |
| 28 | 26, 27 | eqtrdi 2793 |
. 2
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → (({𝐴, 𝐵} ∩ {𝐶}) ∪ ({𝐴, 𝐵} ∩ {𝐷})) = ∅) |
| 29 | 4, 28 | eqtrid 2789 |
1
⊢ (((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) → ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅) |