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 6309

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 6308	. . 3 ⊢ (𝑅 Po 𝐴 ↔ ^◡𝑅 Po 𝐴)
2		ralcom 3294	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
3		vex 3458	. . . . . . 7 ⊢ 𝑦 ∈ V
4		vex 3458	. . . . . . 7 ⊢ 𝑥 ∈ V
5	3, 4	brcnv 5867	. . . . . 6 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
6		equcom 2053	. . . . . 6 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
7	4, 3	brcnv 5867	. . . . . 6 ⊢ (𝑥^◡𝑅𝑦 ↔ 𝑦𝑅𝑥)
8	5, 6, 7	3orbi123i 1174	. . . . 5 ⊢ ((𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦) ↔ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
9	8	2ralbii 3141	. . . 4 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
10	2, 9	bitr4i 281	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦))
11	1, 10	anbi12i 640	. 2 ⊢ ((𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (^◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦)))
12		df-so 5564	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
13		df-so 5564	. 2 ⊢ (^◡𝑅 Or 𝐴 ↔ (^◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦^◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥^◡𝑅𝑦)))
14	11, 12, 13	3bitr4i 306	1 ⊢ (𝑅 Or 𝐴 ↔ ^◡𝑅 Or 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 ∨ w3o 1102 ∀wral 3080 class class class wbr 5106 Po wpo 5561 Or wor 5562 ^◡ccnv 5654

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5252 ax-pr 5395

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-clab 2742 df-cleq 2755 df-clel 2839 df-ne 2960 df-ral 3081 df-rab 3417 df-v 3456 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-sn 4589 df-pr 4591 df-op 4839 df-br 5107 df-opab 5171 df-po 5563 df-so 5564 df-cnv 5663

This theorem is used by: infexd 9503 eqinf 9504 infval 9506 infcl 9508 inflb 9509 infglb 9510 infglbb 9511 fiinfcl 9522 infltoreq 9523 infempty 9528 infiso 9529 wofib 9566 oemapso 9710 cflim2 10368 fin23lem40 10456 gtso 11418 nomaxmo 28085 tosglb 33606 xrsclat 33642 xrge0iifiso 34637 socnv 36707 welb 38862 xrgtso 46562

W3C validator