![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnvso | Structured version Visualization version GIF version |
Description: The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005.) |
Ref | Expression |
---|---|
cnvso | ⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvpo 6238 | . . 3 ⊢ (𝑅 Po 𝐴 ↔ ◡𝑅 Po 𝐴) | |
2 | ralcom 3271 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) | |
3 | vex 3448 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
4 | vex 3448 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
5 | 3, 4 | brcnv 5837 | . . . . . 6 ⊢ (𝑦◡𝑅𝑥 ↔ 𝑥𝑅𝑦) |
6 | equcom 2022 | . . . . . 6 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦) | |
7 | 4, 3 | brcnv 5837 | . . . . . 6 ⊢ (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥) |
8 | 5, 6, 7 | 3orbi123i 1157 | . . . . 5 ⊢ ((𝑦◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥◡𝑅𝑦) ↔ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
9 | 8 | 2ralbii 3126 | . . . 4 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥◡𝑅𝑦) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
10 | 2, 9 | bitr4i 278 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥◡𝑅𝑦)) |
11 | 1, 10 | anbi12i 628 | . 2 ⊢ ((𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥◡𝑅𝑦))) |
12 | df-so 5545 | . 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
13 | df-so 5545 | . 2 ⊢ (◡𝑅 Or 𝐴 ↔ (◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥◡𝑅𝑦))) | |
14 | 11, 12, 13 | 3bitr4i 303 | 1 ⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∨ w3o 1087 ∀wral 3063 class class class wbr 5104 Po wpo 5542 Or wor 5543 ◡ccnv 5631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-sep 5255 ax-nul 5262 ax-pr 5383 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2943 df-ral 3064 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-br 5105 df-opab 5167 df-po 5544 df-so 5545 df-cnv 5640 |
This theorem is referenced by: infexd 9378 eqinf 9379 infval 9381 infcl 9383 inflb 9384 infglb 9385 infglbb 9386 fiinfcl 9396 infltoreq 9397 infempty 9402 infiso 9403 wofib 9440 oemapso 9577 cflim2 10158 fin23lem40 10246 gtso 11195 nomaxmo 26998 tosglb 31660 xrsclat 31696 xrge0iifiso 32320 socnv 34147 welb 36127 xrgtso 43478 |
Copyright terms: Public domain | W3C validator |