Proof of Theorem disjtp2
Step | Hyp | Ref
| Expression |
1 | | df-tp 4566 |
. . 3
⊢ {𝐷, 𝐸, 𝐹} = ({𝐷, 𝐸} ∪ {𝐹}) |
2 | 1 | ineq2i 4143 |
. 2
⊢ ({𝐴, 𝐵, 𝐶} ∩ {𝐷, 𝐸, 𝐹}) = ({𝐴, 𝐵, 𝐶} ∩ ({𝐷, 𝐸} ∪ {𝐹})) |
3 | | df-tp 4566 |
. . . . . 6
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) |
4 | 3 | ineq1i 4142 |
. . . . 5
⊢ ({𝐴, 𝐵, 𝐶} ∩ {𝐷, 𝐸}) = (({𝐴, 𝐵} ∪ {𝐶}) ∩ {𝐷, 𝐸}) |
5 | | 3simpa 1147 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) → (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷)) |
6 | | 3simpa 1147 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) → (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸)) |
7 | | disjpr2 4649 |
. . . . . . . . 9
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸)) → ({𝐴, 𝐵} ∩ {𝐷, 𝐸}) = ∅) |
8 | 5, 6, 7 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸)) → ({𝐴, 𝐵} ∩ {𝐷, 𝐸}) = ∅) |
9 | 8 | 3adant3 1131 |
. . . . . . 7
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → ({𝐴, 𝐵} ∩ {𝐷, 𝐸}) = ∅) |
10 | | incom 4135 |
. . . . . . . 8
⊢ ({𝐶} ∩ {𝐷, 𝐸}) = ({𝐷, 𝐸} ∩ {𝐶}) |
11 | | necom 2997 |
. . . . . . . . . . . 12
⊢ (𝐶 ≠ 𝐷 ↔ 𝐷 ≠ 𝐶) |
12 | 11 | biimpi 215 |
. . . . . . . . . . 11
⊢ (𝐶 ≠ 𝐷 → 𝐷 ≠ 𝐶) |
13 | 12 | 3ad2ant3 1134 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) → 𝐷 ≠ 𝐶) |
14 | | necom 2997 |
. . . . . . . . . . . 12
⊢ (𝐶 ≠ 𝐸 ↔ 𝐸 ≠ 𝐶) |
15 | 14 | biimpi 215 |
. . . . . . . . . . 11
⊢ (𝐶 ≠ 𝐸 → 𝐸 ≠ 𝐶) |
16 | 15 | 3ad2ant3 1134 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) → 𝐸 ≠ 𝐶) |
17 | | disjprsn 4650 |
. . . . . . . . . 10
⊢ ((𝐷 ≠ 𝐶 ∧ 𝐸 ≠ 𝐶) → ({𝐷, 𝐸} ∩ {𝐶}) = ∅) |
18 | 13, 16, 17 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸)) → ({𝐷, 𝐸} ∩ {𝐶}) = ∅) |
19 | 18 | 3adant3 1131 |
. . . . . . . 8
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → ({𝐷, 𝐸} ∩ {𝐶}) = ∅) |
20 | 10, 19 | eqtrid 2790 |
. . . . . . 7
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → ({𝐶} ∩ {𝐷, 𝐸}) = ∅) |
21 | 9, 20 | jca 512 |
. . . . . 6
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → (({𝐴, 𝐵} ∩ {𝐷, 𝐸}) = ∅ ∧ ({𝐶} ∩ {𝐷, 𝐸}) = ∅)) |
22 | | undisj1 4395 |
. . . . . 6
⊢ ((({𝐴, 𝐵} ∩ {𝐷, 𝐸}) = ∅ ∧ ({𝐶} ∩ {𝐷, 𝐸}) = ∅) ↔ (({𝐴, 𝐵} ∪ {𝐶}) ∩ {𝐷, 𝐸}) = ∅) |
23 | 21, 22 | sylib 217 |
. . . . 5
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → (({𝐴, 𝐵} ∪ {𝐶}) ∩ {𝐷, 𝐸}) = ∅) |
24 | 4, 23 | eqtrid 2790 |
. . . 4
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → ({𝐴, 𝐵, 𝐶} ∩ {𝐷, 𝐸}) = ∅) |
25 | | disjtpsn 4651 |
. . . . 5
⊢ ((𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹) → ({𝐴, 𝐵, 𝐶} ∩ {𝐹}) = ∅) |
26 | 25 | 3ad2ant3 1134 |
. . . 4
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → ({𝐴, 𝐵, 𝐶} ∩ {𝐹}) = ∅) |
27 | 24, 26 | jca 512 |
. . 3
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → (({𝐴, 𝐵, 𝐶} ∩ {𝐷, 𝐸}) = ∅ ∧ ({𝐴, 𝐵, 𝐶} ∩ {𝐹}) = ∅)) |
28 | | undisj2 4396 |
. . 3
⊢ ((({𝐴, 𝐵, 𝐶} ∩ {𝐷, 𝐸}) = ∅ ∧ ({𝐴, 𝐵, 𝐶} ∩ {𝐹}) = ∅) ↔ ({𝐴, 𝐵, 𝐶} ∩ ({𝐷, 𝐸} ∪ {𝐹})) = ∅) |
29 | 27, 28 | sylib 217 |
. 2
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → ({𝐴, 𝐵, 𝐶} ∩ ({𝐷, 𝐸} ∪ {𝐹})) = ∅) |
30 | 2, 29 | eqtrid 2790 |
1
⊢ (((𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐵 ≠ 𝐸 ∧ 𝐶 ≠ 𝐸) ∧ (𝐴 ≠ 𝐹 ∧ 𝐵 ≠ 𝐹 ∧ 𝐶 ≠ 𝐹)) → ({𝐴, 𝐵, 𝐶} ∩ {𝐷, 𝐸, 𝐹}) = ∅) |