Step | Hyp | Ref
| Expression |
1 | | neq0 4234 |
. . . 4
⊢ (¬
([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ↔ ∃𝑥 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) |
2 | | simpl 486 |
. . . . . . 7
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑅 Er 𝑋) |
3 | | elinel1 4085 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → 𝑥 ∈ [𝐴]𝑅) |
4 | 3 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑥 ∈ [𝐴]𝑅) |
5 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
6 | | ecexr 8325 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ [𝐴]𝑅 → 𝐴 ∈ V) |
7 | 4, 6 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴 ∈ V) |
8 | | elecg 8363 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) |
9 | 5, 7, 8 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) |
10 | 4, 9 | mpbid 235 |
. . . . . . . 8
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴𝑅𝑥) |
11 | | elinel2 4086 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → 𝑥 ∈ [𝐵]𝑅) |
12 | 11 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑥 ∈ [𝐵]𝑅) |
13 | | ecexr 8325 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ [𝐵]𝑅 → 𝐵 ∈ V) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐵 ∈ V) |
15 | | elecg 8363 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) |
16 | 5, 14, 15 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) |
17 | 12, 16 | mpbid 235 |
. . . . . . . 8
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐵𝑅𝑥) |
18 | 2, 10, 17 | ertr4d 8339 |
. . . . . . 7
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴𝑅𝐵) |
19 | 2, 18 | erthi 8371 |
. . . . . 6
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → [𝐴]𝑅 = [𝐵]𝑅) |
20 | 19 | ex 416 |
. . . . 5
⊢ (𝑅 Er 𝑋 → (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)) |
21 | 20 | exlimdv 1940 |
. . . 4
⊢ (𝑅 Er 𝑋 → (∃𝑥 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)) |
22 | 1, 21 | syl5bi 245 |
. . 3
⊢ (𝑅 Er 𝑋 → (¬ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ → [𝐴]𝑅 = [𝐵]𝑅)) |
23 | 22 | orrd 862 |
. 2
⊢ (𝑅 Er 𝑋 → (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ [𝐴]𝑅 = [𝐵]𝑅)) |
24 | 23 | orcomd 870 |
1
⊢ (𝑅 Er 𝑋 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)) |