Step | Hyp | Ref
| Expression |
1 | | neq0 3930 |
. . . 4
⊢ (¬
([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ↔ ∃𝑥 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) |
2 | | simpl 473 |
. . . . . . 7
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑅 Er 𝑋) |
3 | | elin 3796 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) ↔ (𝑥 ∈ [𝐴]𝑅 ∧ 𝑥 ∈ [𝐵]𝑅)) |
4 | 3 | simplbi 476 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → 𝑥 ∈ [𝐴]𝑅) |
5 | 4 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑥 ∈ [𝐴]𝑅) |
6 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
7 | | ecexr 7747 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ [𝐴]𝑅 → 𝐴 ∈ V) |
8 | 5, 7 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴 ∈ V) |
9 | | elecg 7785 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) |
10 | 6, 8, 9 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) |
11 | 5, 10 | mpbid 222 |
. . . . . . . 8
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴𝑅𝑥) |
12 | 3 | simprbi 480 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → 𝑥 ∈ [𝐵]𝑅) |
13 | 12 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑥 ∈ [𝐵]𝑅) |
14 | | ecexr 7747 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ [𝐵]𝑅 → 𝐵 ∈ V) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐵 ∈ V) |
16 | | elecg 7785 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) |
17 | 6, 15, 16 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) |
18 | 13, 17 | mpbid 222 |
. . . . . . . 8
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐵𝑅𝑥) |
19 | 2, 11, 18 | ertr4d 7761 |
. . . . . . 7
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴𝑅𝐵) |
20 | 2, 19 | erthi 7793 |
. . . . . 6
⊢ ((𝑅 Er 𝑋 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → [𝐴]𝑅 = [𝐵]𝑅) |
21 | 20 | ex 450 |
. . . . 5
⊢ (𝑅 Er 𝑋 → (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)) |
22 | 21 | exlimdv 1861 |
. . . 4
⊢ (𝑅 Er 𝑋 → (∃𝑥 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)) |
23 | 1, 22 | syl5bi 232 |
. . 3
⊢ (𝑅 Er 𝑋 → (¬ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ → [𝐴]𝑅 = [𝐵]𝑅)) |
24 | 23 | orrd 393 |
. 2
⊢ (𝑅 Er 𝑋 → (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ [𝐴]𝑅 = [𝐵]𝑅)) |
25 | 24 | orcomd 403 |
1
⊢ (𝑅 Er 𝑋 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)) |