![]() |
Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > qsdisjALTV | Structured version Visualization version GIF version |
Description: Elements of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.) (Revised by Peter Mazsa, 3-Jun-2019.) |
Ref | Expression |
---|---|
qsdisjALTV.1 | ⊢ (𝜑 → EqvRel 𝑅) |
qsdisjALTV.2 | ⊢ (𝜑 → 𝐵 ∈ (𝐴 / 𝑅)) |
qsdisjALTV.3 | ⊢ (𝜑 → 𝐶 ∈ (𝐴 / 𝑅)) |
Ref | Expression |
---|---|
qsdisjALTV | ⊢ (𝜑 → (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | qsdisjALTV.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ (𝐴 / 𝑅)) | |
2 | eqid 2725 | . . 3 ⊢ (𝐴 / 𝑅) = (𝐴 / 𝑅) | |
3 | eqeq1 2729 | . . . 4 ⊢ ([𝑥]𝑅 = 𝐵 → ([𝑥]𝑅 = 𝐶 ↔ 𝐵 = 𝐶)) | |
4 | ineq1 4199 | . . . . 5 ⊢ ([𝑥]𝑅 = 𝐵 → ([𝑥]𝑅 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
5 | 4 | eqeq1d 2727 | . . . 4 ⊢ ([𝑥]𝑅 = 𝐵 → (([𝑥]𝑅 ∩ 𝐶) = ∅ ↔ (𝐵 ∩ 𝐶) = ∅)) |
6 | 3, 5 | orbi12d 916 | . . 3 ⊢ ([𝑥]𝑅 = 𝐵 → (([𝑥]𝑅 = 𝐶 ∨ ([𝑥]𝑅 ∩ 𝐶) = ∅) ↔ (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅))) |
7 | qsdisjALTV.3 | . . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐴 / 𝑅)) | |
8 | eqeq2 2737 | . . . . . 6 ⊢ ([𝑦]𝑅 = 𝐶 → ([𝑥]𝑅 = [𝑦]𝑅 ↔ [𝑥]𝑅 = 𝐶)) | |
9 | ineq2 4200 | . . . . . . 7 ⊢ ([𝑦]𝑅 = 𝐶 → ([𝑥]𝑅 ∩ [𝑦]𝑅) = ([𝑥]𝑅 ∩ 𝐶)) | |
10 | 9 | eqeq1d 2727 | . . . . . 6 ⊢ ([𝑦]𝑅 = 𝐶 → (([𝑥]𝑅 ∩ [𝑦]𝑅) = ∅ ↔ ([𝑥]𝑅 ∩ 𝐶) = ∅)) |
11 | 8, 10 | orbi12d 916 | . . . . 5 ⊢ ([𝑦]𝑅 = 𝐶 → (([𝑥]𝑅 = [𝑦]𝑅 ∨ ([𝑥]𝑅 ∩ [𝑦]𝑅) = ∅) ↔ ([𝑥]𝑅 = 𝐶 ∨ ([𝑥]𝑅 ∩ 𝐶) = ∅))) |
12 | qsdisjALTV.1 | . . . . . . 7 ⊢ (𝜑 → EqvRel 𝑅) | |
13 | 12 | ad2antrr 724 | . . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → EqvRel 𝑅) |
14 | eqvreldisj 38141 | . . . . . 6 ⊢ ( EqvRel 𝑅 → ([𝑥]𝑅 = [𝑦]𝑅 ∨ ([𝑥]𝑅 ∩ [𝑦]𝑅) = ∅)) | |
15 | 13, 14 | syl 17 | . . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ([𝑥]𝑅 = [𝑦]𝑅 ∨ ([𝑥]𝑅 ∩ [𝑦]𝑅) = ∅)) |
16 | 2, 11, 15 | ectocld 8799 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ∈ (𝐴 / 𝑅)) → ([𝑥]𝑅 = 𝐶 ∨ ([𝑥]𝑅 ∩ 𝐶) = ∅)) |
17 | 7, 16 | mpidan 687 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ([𝑥]𝑅 = 𝐶 ∨ ([𝑥]𝑅 ∩ 𝐶) = ∅)) |
18 | 2, 6, 17 | ectocld 8799 | . 2 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅)) |
19 | 1, 18 | mpdan 685 | 1 ⊢ (𝜑 → (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∨ wo 845 = wceq 1533 ∈ wcel 2098 ∩ cin 3939 ∅c0 4318 [cec 8719 / cqs 8720 EqvRel weqvrel 37721 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5294 ax-nul 5301 ax-pr 5423 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2931 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3465 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-br 5144 df-opab 5206 df-id 5570 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-ec 8723 df-qs 8727 df-refrel 38039 df-symrel 38071 df-trrel 38101 df-eqvrel 38112 |
This theorem is referenced by: eqvreldisj1 38351 |
Copyright terms: Public domain | W3C validator |