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 6261

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 6260	. . 3 ⊢ (𝑅 Po 𝐴 ↔ ^◡𝑅 Po 𝐴)
2		ralcom 3265	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
3		vex 3451	. . . . . . 7 ⊢ 𝑦 ∈ V
4		vex 3451	. . . . . . 7 ⊢ 𝑥 ∈ V
5	3, 4	brcnv 5846	. . . . . 6 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
6		equcom 2018	. . . . . 6 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
7	4, 3	brcnv 5846	. . . . . 6 ⊢ (𝑥^◡𝑅𝑦 ↔ 𝑦𝑅𝑥)
8	5, 6, 7	3orbi123i 1156	. . . . 5 ⊢ ((𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦) ↔ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
9	8	2ralbii 3108	. . . 4 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
10	2, 9	bitr4i 278	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦))
11	1, 10	anbi12i 628	. 2 ⊢ ((𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (^◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦)))
12		df-so 5547	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
13		df-so 5547	. 2 ⊢ (^◡𝑅 Or 𝐴 ↔ (^◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦)))
14	11, 12, 13	3bitr4i 303	1 ⊢ (𝑅 Or 𝐴 ↔ ^◡𝑅 Or 𝐴)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 ∨ w3o 1085 ∀wral 3044 class class class wbr 5107 Po wpo 5544 Or wor 5545 ^◡ccnv 5637

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5251 ax-nul 5261 ax-pr 5387

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-ne 2926 df-ral 3045 df-rab 3406 df-v 3449 df-dif 3917 df-un 3919 df-ss 3931 df-nul 4297 df-if 4489 df-sn 4590 df-pr 4592 df-op 4596 df-br 5108 df-opab 5170 df-po 5546 df-so 5547 df-cnv 5646

This theorem is referenced by: infexd 9435 eqinf 9436 infval 9438 infcl 9440 inflb 9441 infglb 9442 infglbb 9443 fiinfcl 9454 infltoreq 9455 infempty 9460 infiso 9461 wofib 9498 oemapso 9635 cflim2 10216 fin23lem40 10304 gtso 11255 nomaxmo 27610 tosglb 32901 xrsclat 32949 xrge0iifiso 33925 socnv 35751 welb 37730 xrgtso 45341

W3C validator