Theorem cnvso 6291

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 6290	. . 3 ⊢ (𝑅 Po 𝐴 ↔ ◡𝑅 Po 𝐴)
2		ralcom 3291	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
3		vex 3455	. . . . . . 7 ⊢ 𝑦 ∈ V
4		vex 3455	. . . . . . 7 ⊢ 𝑥 ∈ V
5	3, 4	brcnv 5860	. . . . . 6 ⊢ (𝑦◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
6		equcom 2051	. . . . . 6 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
7	4, 3	brcnv 5860	. . . . . 6 ⊢ (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥)
8	5, 6, 7	3orbi123i 1174	. . . . 5 ⊢ ((𝑦◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥◡𝑅𝑦) ↔ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
9	8	2ralbii 3138	. . . 4 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥◡𝑅𝑦) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
10	2, 9	bitr4i 281	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥◡𝑅𝑦))
11	1, 10	anbi12i 640	. 2 ⊢ ((𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥◡𝑅𝑦)))
12		df-so 5560	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
13		df-so 5560	. 2 ⊢ (◡𝑅 Or 𝐴 ↔ (◡𝑅 Po 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑦◡𝑅𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥◡𝑅𝑦)))
14	11, 12, 13	3bitr4i 306	1 ⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ w3o 1102  ∀wral 3077   class class class wbr 5103   Po wpo 5557   Or wor 5558  ^◡ccnv 5650

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-po 5559  df-so 5560  df-cnv 5659

This theorem is used by:  infexd  9476  eqinf  9477  infval  9479  infcl  9481  inflb  9482  infglb  9483  infglbb  9484  fiinfcl  9495  infltoreq  9496  infempty  9501  infiso  9502  wofib  9539  oemapso  9683  cflim2  10341  fin23lem40  10429  gtso  11391  nomaxmo  28055  tosglb  33536  xrsclat  33572  xrge0iifiso  34567  socnv  36529  welb  38671  xrgtso  46357