Step | Hyp | Ref
| Expression |
1 | | neq0 4232 |
. . . 4
⊢ (¬
([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ↔ ∃𝑥 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) |
2 | | simpl 486 |
. . . . . . 7
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → EqvRel 𝑅) |
3 | | elinel1 4083 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → 𝑥 ∈ [𝐴]𝑅) |
4 | 3 | adantl 485 |
. . . . . . . . 9
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑥 ∈ [𝐴]𝑅) |
5 | | ecexr 8318 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ [𝐴]𝑅 → 𝐴 ∈ V) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴 ∈ V) |
7 | | vex 3401 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
8 | | elecALTV 36017 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝑥 ∈ V) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) |
9 | 6, 7, 8 | sylancl 589 |
. . . . . . . . 9
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) |
10 | 4, 9 | mpbid 235 |
. . . . . . . 8
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴𝑅𝑥) |
11 | | elinel2 4084 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → 𝑥 ∈ [𝐵]𝑅) |
12 | 11 | adantl 485 |
. . . . . . . . 9
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝑥 ∈ [𝐵]𝑅) |
13 | | ecexr 8318 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ [𝐵]𝑅 → 𝐵 ∈ V) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐵 ∈ V) |
15 | | elecALTV 36017 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ V ∧ 𝑥 ∈ V) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) |
16 | 14, 7, 15 | sylancl 589 |
. . . . . . . . 9
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) |
17 | 12, 16 | mpbid 235 |
. . . . . . . 8
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐵𝑅𝑥) |
18 | 2, 10, 17 | eqvreltr4d 36334 |
. . . . . . 7
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → 𝐴𝑅𝐵) |
19 | 2, 18 | eqvrelthi 36338 |
. . . . . 6
⊢ (( EqvRel
𝑅 ∧ 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅)) → [𝐴]𝑅 = [𝐵]𝑅) |
20 | 19 | ex 416 |
. . . . 5
⊢ ( EqvRel
𝑅 → (𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)) |
21 | 20 | exlimdv 1939 |
. . . 4
⊢ ( EqvRel
𝑅 → (∃𝑥 𝑥 ∈ ([𝐴]𝑅 ∩ [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)) |
22 | 1, 21 | syl5bi 245 |
. . 3
⊢ ( EqvRel
𝑅 → (¬ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ → [𝐴]𝑅 = [𝐵]𝑅)) |
23 | 22 | orrd 862 |
. 2
⊢ ( EqvRel
𝑅 → (([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅ ∨ [𝐴]𝑅 = [𝐵]𝑅)) |
24 | 23 | orcomd 870 |
1
⊢ ( EqvRel
𝑅 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)) |