Step | Hyp | Ref
| Expression |
1 | | neq0 4279 |
. . . 4
⊢ (¬
([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ↔ ∃𝑥 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) |
2 | | simpl 483 |
. . . . . . 7
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑅 Er 𝑋) |
3 | | elinel1 4129 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → 𝑥 ∈ [𝐴]𝑅) |
4 | 3 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑥 ∈ [𝐴]𝑅) |
5 | | vex 3436 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
6 | | ecexr 8503 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ [𝐴]𝑅 → 𝐴 ∈ V) |
7 | 4, 6 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴 ∈ V) |
8 | | elecg 8541 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) |
9 | 5, 7, 8 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) |
10 | 4, 9 | mpbid 231 |
. . . . . . . 8
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴𝑅𝑥) |
11 | | elinel2 4130 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → 𝑥 ∈ [𝐵]𝑅) |
12 | 11 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑥 ∈ [𝐵]𝑅) |
13 | | ecexr 8503 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ [𝐵]𝑅 → 𝐵 ∈ V) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐵 ∈ V) |
15 | | elecg 8541 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) |
16 | 5, 14, 15 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) |
17 | 12, 16 | mpbid 231 |
. . . . . . . 8
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐵𝑅𝑥) |
18 | 2, 10, 17 | ertr4d 8517 |
. . . . . . 7
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴𝑅𝐵) |
19 | 2, 18 | erthi 8549 |
. . . . . 6
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → [𝐴]𝑅 = [𝐵]𝑅) |
20 | 19 | ex 413 |
. . . . 5
⊢ (𝑅 Er 𝑋 → (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)) |
21 | 20 | exlimdv 1936 |
. . . 4
⊢ (𝑅 Er 𝑋 → (∃𝑥 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)) |
22 | 1, 21 | syl5bi 241 |
. . 3
⊢ (𝑅 Er 𝑋 → (¬ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ → [𝐴]𝑅 = [𝐵]𝑅)) |
23 | 22 | orrd 860 |
. 2
⊢ (𝑅 Er 𝑋 → (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ [𝐴]𝑅 = [𝐵]𝑅)) |
24 | 23 | orcomd 868 |
1
⊢ (𝑅 Er 𝑋 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)) |