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