| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > iserd | Structured version Visualization version GIF version | ||
| Description: A reflexive, symmetric, transitive relation is an equivalence relation on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| Ref | Expression |
|---|---|
| iserd.1 | ⊢ (𝜑 → Rel 𝑅) |
| iserd.2 | ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦𝑅𝑥) |
| iserd.3 | ⊢ ((𝜑 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) |
| iserd.4 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)) |
| Ref | Expression |
|---|---|
| iserd | ⊢ (𝜑 → 𝑅 Er 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iserd.1 | . . 3 ⊢ (𝜑 → Rel 𝑅) | |
| 2 | eqidd 2738 | . . 3 ⊢ (𝜑 → dom 𝑅 = dom 𝑅) | |
| 3 | iserd.2 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦𝑅𝑥) | |
| 4 | 3 | ex 412 | . . . . . . 7 ⊢ (𝜑 → (𝑥𝑅𝑦 → 𝑦𝑅𝑥)) |
| 5 | iserd.3 | . . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) | |
| 6 | 5 | ex 412 | . . . . . . 7 ⊢ (𝜑 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
| 7 | 4, 6 | jca 511 | . . . . . 6 ⊢ (𝜑 → ((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
| 8 | 7 | alrimiv 1929 | . . . . 5 ⊢ (𝜑 → ∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
| 9 | 8 | alrimiv 1929 | . . . 4 ⊢ (𝜑 → ∀𝑦∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
| 10 | 9 | alrimiv 1929 | . . 3 ⊢ (𝜑 → ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
| 11 | dfer2 8635 | . . 3 ⊢ (𝑅 Er dom 𝑅 ↔ (Rel 𝑅 ∧ dom 𝑅 = dom 𝑅 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))) | |
| 12 | 1, 2, 10, 11 | syl3anbrc 1345 | . 2 ⊢ (𝜑 → 𝑅 Er dom 𝑅) |
| 13 | 12 | adantr 480 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝑅) → 𝑅 Er dom 𝑅) |
| 14 | simpr 484 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝑅) → 𝑥 ∈ dom 𝑅) | |
| 15 | 13, 14 | erref 8655 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝑅) → 𝑥𝑅𝑥) |
| 16 | 15 | ex 412 | . . . . . 6 ⊢ (𝜑 → (𝑥 ∈ dom 𝑅 → 𝑥𝑅𝑥)) |
| 17 | vex 3434 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
| 18 | 17, 17 | breldm 5855 | . . . . . 6 ⊢ (𝑥𝑅𝑥 → 𝑥 ∈ dom 𝑅) |
| 19 | 16, 18 | impbid1 225 | . . . . 5 ⊢ (𝜑 → (𝑥 ∈ dom 𝑅 ↔ 𝑥𝑅𝑥)) |
| 20 | iserd.4 | . . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)) | |
| 21 | 19, 20 | bitr4d 282 | . . . 4 ⊢ (𝜑 → (𝑥 ∈ dom 𝑅 ↔ 𝑥 ∈ 𝐴)) |
| 22 | 21 | eqrdv 2735 | . . 3 ⊢ (𝜑 → dom 𝑅 = 𝐴) |
| 23 | ereq2 8643 | . . 3 ⊢ (dom 𝑅 = 𝐴 → (𝑅 Er dom 𝑅 ↔ 𝑅 Er 𝐴)) | |
| 24 | 22, 23 | syl 17 | . 2 ⊢ (𝜑 → (𝑅 Er dom 𝑅 ↔ 𝑅 Er 𝐴)) |
| 25 | 12, 24 | mpbid 232 | 1 ⊢ (𝜑 → 𝑅 Er 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1540 = wceq 1542 ∈ wcel 2114 class class class wbr 5086 dom cdm 5622 Rel wrel 5627 Er wer 8631 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-sep 5231 ax-pr 5368 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-br 5087 df-opab 5149 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-er 8634 |
| This theorem is referenced by: iseri 8662 iseriALT 8663 swoer 8666 iiner 8727 erinxp 8729 cicer 17762 eqger 19142 gaorber 19272 efgrelexlemb 19714 efgcpbllemb 19719 xmeter 24407 ercgrg 28604 erler 33346 metider 34059 prjsper 43052 cicerALT 49518 |
| Copyright terms: Public domain | W3C validator |