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 6271

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 6270	. . 3 ⊢ (𝑅 Po 𝐴 ↔ ^◡𝑅 Po 𝐴)
2		ralcom 3289	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
3		vex 3457	. . . . . . 7 ⊢ 𝑦 ∈ V
4		vex 3457	. . . . . . 7 ⊢ 𝑥 ∈ V
5	3, 4	brcnv 5852	. . . . . 6 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
6		equcom 2037	. . . . . 6 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
7	4, 3	brcnv 5852	. . . . . 6 ⊢ (𝑥^◡𝑅𝑦 ↔ 𝑦𝑅𝑥)
8	5, 6, 7	3orbi123i 1168	. . . . 5 ⊢ ((𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦) ↔ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
9	8	2ralbii 3136	. . . 4 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
10	2, 9	bitr4i 280	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦))
11	1, 10	anbi12i 637	. 2 ⊢ ((𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (^◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦)))
12		df-so 5554	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
13		df-so 5554	. 2 ⊢ (^◡𝑅 Or 𝐴 ↔ (^◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦)))
14	11, 12, 13	3bitr4i 305	1 ⊢ (𝑅 Or 𝐴 ↔ ^◡𝑅 Or 𝐴)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 ∧ wa 399 ∨ w3o 1096 ∀wral 3075 class class class wbr 5099 Po wpo 5551 Or wor 5552 ^◡ccnv 5644

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5245 ax-pr 5389

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-clab 2740 df-cleq 2753 df-clel 2836 df-ne 2957 df-ral 3076 df-rab 3414 df-v 3455 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4480 df-sn 4582 df-pr 4584 df-op 4588 df-br 5100 df-opab 5162 df-po 5553 df-so 5554 df-cnv 5653

This theorem is referenced by: infexd 9427 eqinf 9428 infval 9430 infcl 9432 inflb 9433 infglb 9434 infglbb 9435 fiinfcl 9446 infltoreq 9447 infempty 9452 infiso 9453 wofib 9490 oemapso 9634 cflim2 10217 fin23lem40 10305 gtso 11261 nomaxmo 27739 tosglb 33114 xrsclat 33150 xrge0iifiso 34193 socnv 36078 welb 38199 xrgtso 45885

W3C validator