![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > disji2 | GIF version |
Description: Property of a disjoint collection: if 𝐵(𝑋) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑋 ≠ 𝑌, then 𝐶 and 𝐷 are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) |
Ref | Expression |
---|---|
disji.1 | ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) |
disji.2 | ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
disji2 | ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disjnims 3929 | . . 3 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 ≠ 𝑧 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) | |
2 | neeq1 2322 | . . . . 5 ⊢ (𝑦 = 𝑋 → (𝑦 ≠ 𝑧 ↔ 𝑋 ≠ 𝑧)) | |
3 | nfcv 2282 | . . . . . . . 8 ⊢ Ⅎ𝑥𝑋 | |
4 | nfcv 2282 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐶 | |
5 | disji.1 | . . . . . . . 8 ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) | |
6 | 3, 4, 5 | csbhypf 3043 | . . . . . . 7 ⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶) |
7 | 6 | ineq1d 3281 | . . . . . 6 ⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵)) |
8 | 7 | eqeq1d 2149 | . . . . 5 ⊢ (𝑦 = 𝑋 → ((⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
9 | 2, 8 | imbi12d 233 | . . . 4 ⊢ (𝑦 = 𝑋 → ((𝑦 ≠ 𝑧 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) ↔ (𝑋 ≠ 𝑧 → (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅))) |
10 | neeq2 2323 | . . . . 5 ⊢ (𝑧 = 𝑌 → (𝑋 ≠ 𝑧 ↔ 𝑋 ≠ 𝑌)) | |
11 | nfcv 2282 | . . . . . . . 8 ⊢ Ⅎ𝑥𝑌 | |
12 | nfcv 2282 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐷 | |
13 | disji.2 | . . . . . . . 8 ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) | |
14 | 11, 12, 13 | csbhypf 3043 | . . . . . . 7 ⊢ (𝑧 = 𝑌 → ⦋𝑧 / 𝑥⦌𝐵 = 𝐷) |
15 | 14 | ineq2d 3282 | . . . . . 6 ⊢ (𝑧 = 𝑌 → (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐶 ∩ 𝐷)) |
16 | 15 | eqeq1d 2149 | . . . . 5 ⊢ (𝑧 = 𝑌 → ((𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ 𝐷) = ∅)) |
17 | 10, 16 | imbi12d 233 | . . . 4 ⊢ (𝑧 = 𝑌 → ((𝑋 ≠ 𝑧 → (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) ↔ (𝑋 ≠ 𝑌 → (𝐶 ∩ 𝐷) = ∅))) |
18 | 9, 17 | rspc2v 2806 | . . 3 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 ≠ 𝑧 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → (𝑋 ≠ 𝑌 → (𝐶 ∩ 𝐷) = ∅))) |
19 | 1, 18 | mpan9 279 | . 2 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋 ≠ 𝑌 → (𝐶 ∩ 𝐷) = ∅)) |
20 | 19 | 3impia 1179 | 1 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 963 = wceq 1332 ∈ wcel 1481 ≠ wne 2309 ∀wral 2417 ⦋csb 3007 ∩ cin 3075 ∅c0 3368 Disj wdisj 3914 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ne 2310 df-ral 2422 df-rex 2423 df-reu 2424 df-rmo 2425 df-v 2691 df-sbc 2914 df-csb 3008 df-dif 3078 df-in 3082 df-nul 3369 df-disj 3915 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |