![]() |
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 3845 | . . 3 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 ≠ 𝑧 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) | |
2 | neeq1 2269 | . . . . 5 ⊢ (𝑦 = 𝑋 → (𝑦 ≠ 𝑧 ↔ 𝑋 ≠ 𝑧)) | |
3 | nfcv 2229 | . . . . . . . 8 ⊢ Ⅎ𝑥𝑋 | |
4 | nfcv 2229 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐶 | |
5 | disji.1 | . . . . . . . 8 ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) | |
6 | 3, 4, 5 | csbhypf 2969 | . . . . . . 7 ⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶) |
7 | 6 | ineq1d 3203 | . . . . . 6 ⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵)) |
8 | 7 | eqeq1d 2097 | . . . . 5 ⊢ (𝑦 = 𝑋 → ((⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
9 | 2, 8 | imbi12d 233 | . . . 4 ⊢ (𝑦 = 𝑋 → ((𝑦 ≠ 𝑧 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) ↔ (𝑋 ≠ 𝑧 → (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅))) |
10 | neeq2 2270 | . . . . 5 ⊢ (𝑧 = 𝑌 → (𝑋 ≠ 𝑧 ↔ 𝑋 ≠ 𝑌)) | |
11 | nfcv 2229 | . . . . . . . 8 ⊢ Ⅎ𝑥𝑌 | |
12 | nfcv 2229 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐷 | |
13 | disji.2 | . . . . . . . 8 ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) | |
14 | 11, 12, 13 | csbhypf 2969 | . . . . . . 7 ⊢ (𝑧 = 𝑌 → ⦋𝑧 / 𝑥⦌𝐵 = 𝐷) |
15 | 14 | ineq2d 3204 | . . . . . 6 ⊢ (𝑧 = 𝑌 → (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐶 ∩ 𝐷)) |
16 | 15 | eqeq1d 2097 | . . . . 5 ⊢ (𝑧 = 𝑌 → ((𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ 𝐷) = ∅)) |
17 | 10, 16 | imbi12d 233 | . . . 4 ⊢ (𝑧 = 𝑌 → ((𝑋 ≠ 𝑧 → (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) ↔ (𝑋 ≠ 𝑌 → (𝐶 ∩ 𝐷) = ∅))) |
18 | 9, 17 | rspc2v 2737 | . . 3 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 ≠ 𝑧 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → (𝑋 ≠ 𝑌 → (𝐶 ∩ 𝐷) = ∅))) |
19 | 1, 18 | mpan9 276 | . 2 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋 ≠ 𝑌 → (𝐶 ∩ 𝐷) = ∅)) |
20 | 19 | 3impia 1141 | 1 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 925 = wceq 1290 ∈ wcel 1439 ≠ wne 2256 ∀wral 2360 ⦋csb 2936 ∩ cin 3001 ∅c0 3289 Disj wdisj 3830 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 580 ax-in2 581 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-3an 927 df-tru 1293 df-fal 1296 df-nf 1396 df-sb 1694 df-eu 1952 df-mo 1953 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ne 2257 df-ral 2365 df-rex 2366 df-reu 2367 df-rmo 2368 df-v 2624 df-sbc 2844 df-csb 2937 df-dif 3004 df-in 3008 df-nul 3290 df-disj 3831 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |