cnvso - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cnvso		Structured version Visualization version GIF version

Theorem cnvso 5977

Description: The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005.)

**Assertion**
Ref	Expression
cnvso	⊢ (𝑅 Or 𝐴 ↔ ^◡𝑅 Or 𝐴)

Proof of Theorem cnvso Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnvpo 5976	. . 3 ⊢ (𝑅 Po 𝐴 ↔ ^◡𝑅 Po 𝐴)
2		ralcom 3295	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
3		vex 3418	. . . . . . 7 ⊢ 𝑦 ∈ V
4		vex 3418	. . . . . . 7 ⊢ 𝑥 ∈ V
5	3, 4	brcnv 5603	. . . . . 6 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
6		equcom 1975	. . . . . 6 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
7	4, 3	brcnv 5603	. . . . . 6 ⊢ (𝑥^◡𝑅𝑦 ↔ 𝑦𝑅𝑥)
8	5, 6, 7	3orbi123i 1136	. . . . 5 ⊢ ((𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦) ↔ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
9	8	2ralbii 3116	. . . 4 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
10	2, 9	bitr4i 270	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦))
11	1, 10	anbi12i 617	. 2 ⊢ ((𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (^◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦)))
12		df-so 5327	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
13		df-so 5327	. 2 ⊢ (^◡𝑅 Or 𝐴 ↔ (^◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦)))
14	11, 12, 13	3bitr4i 295	1 ⊢ (𝑅 Or 𝐴 ↔ ^◡𝑅 Or 𝐴)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 198 ∧ wa 387 ∨ w3o 1067 ∀wral 3088 class class class wbr 4929 Po wpo 5324 Or wor 5325 ^◡ccnv 5406

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pr 5186

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-ral 3093 df-rab 3097 df-v 3417 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-br 4930 df-opab 4992 df-po 5326 df-so 5327 df-cnv 5415

This theorem is referenced by: infexd 8742 eqinf 8743 infval 8745 infcl 8747 inflb 8748 infglb 8749 infglbb 8750 fiinfcl 8760 infltoreq 8761 infempty 8766 infiso 8767 wofib 8804 oemapso 8939 cflim2 9483 fin23lem40 9571 gtso 10522 tosglb 30395 xrsclat 30405 xrge0iifiso 30828 socnv 32526 nomaxmo 32728 welb 34459 xrgtso 41048

W3C validator