ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnvsom GIF version

Theorem cnvsom 5193
Description: The converse of a strict order relation is a strict order relation. (Contributed by Jim Kingdon, 19-Dec-2018.)
Assertion
Ref Expression
cnvsom (∃𝑥 𝑥𝐴 → (𝑅 Or 𝐴𝑅 Or 𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑅

Proof of Theorem cnvsom
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnvpom 5192 . . 3 (∃𝑥 𝑥𝐴 → (𝑅 Po 𝐴𝑅 Po 𝐴))
2 vex 2755 . . . . . . . . 9 𝑦 ∈ V
3 vex 2755 . . . . . . . . 9 𝑥 ∈ V
42, 3brcnv 4831 . . . . . . . 8 (𝑦𝑅𝑥𝑥𝑅𝑦)
5 vex 2755 . . . . . . . . . . 11 𝑧 ∈ V
62, 5brcnv 4831 . . . . . . . . . 10 (𝑦𝑅𝑧𝑧𝑅𝑦)
75, 3brcnv 4831 . . . . . . . . . 10 (𝑧𝑅𝑥𝑥𝑅𝑧)
86, 7orbi12i 765 . . . . . . . . 9 ((𝑦𝑅𝑧𝑧𝑅𝑥) ↔ (𝑧𝑅𝑦𝑥𝑅𝑧))
9 orcom 729 . . . . . . . . 9 ((𝑧𝑅𝑦𝑥𝑅𝑧) ↔ (𝑥𝑅𝑧𝑧𝑅𝑦))
108, 9bitri 184 . . . . . . . 8 ((𝑦𝑅𝑧𝑧𝑅𝑥) ↔ (𝑥𝑅𝑧𝑧𝑅𝑦))
114, 10imbi12i 239 . . . . . . 7 ((𝑦𝑅𝑥 → (𝑦𝑅𝑧𝑧𝑅𝑥)) ↔ (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))
1211ralbii 2496 . . . . . 6 (∀𝑧𝐴 (𝑦𝑅𝑥 → (𝑦𝑅𝑧𝑧𝑅𝑥)) ↔ ∀𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))
13122ralbii 2498 . . . . 5 (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑦𝑅𝑥 → (𝑦𝑅𝑧𝑧𝑅𝑥)) ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))
14 ralcom 2653 . . . . 5 (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑦𝑅𝑥 → (𝑦𝑅𝑧𝑧𝑅𝑥)) ↔ ∀𝑦𝐴𝑥𝐴𝑧𝐴 (𝑦𝑅𝑥 → (𝑦𝑅𝑧𝑧𝑅𝑥)))
1513, 14bitr3i 186 . . . 4 (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)) ↔ ∀𝑦𝐴𝑥𝐴𝑧𝐴 (𝑦𝑅𝑥 → (𝑦𝑅𝑧𝑧𝑅𝑥)))
1615a1i 9 . . 3 (∃𝑥 𝑥𝐴 → (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)) ↔ ∀𝑦𝐴𝑥𝐴𝑧𝐴 (𝑦𝑅𝑥 → (𝑦𝑅𝑧𝑧𝑅𝑥))))
171, 16anbi12d 473 . 2 (∃𝑥 𝑥𝐴 → ((𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))) ↔ (𝑅 Po 𝐴 ∧ ∀𝑦𝐴𝑥𝐴𝑧𝐴 (𝑦𝑅𝑥 → (𝑦𝑅𝑧𝑧𝑅𝑥)))))
18 df-iso 4318 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))))
19 df-iso 4318 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑦𝐴𝑥𝐴𝑧𝐴 (𝑦𝑅𝑥 → (𝑦𝑅𝑧𝑧𝑅𝑥))))
2017, 18, 193bitr4g 223 1 (∃𝑥 𝑥𝐴 → (𝑅 Or 𝐴𝑅 Or 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wo 709  wex 1503  wcel 2160  wral 2468   class class class wbr 4021   Po wpo 4315   Or wor 4316  ccnv 4646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4139  ax-pow 4195  ax-pr 4230
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-pw 3595  df-sn 3616  df-pr 3617  df-op 3619  df-br 4022  df-opab 4083  df-po 4317  df-iso 4318  df-cnv 4655
This theorem is referenced by:  gtso  8071
  Copyright terms: Public domain W3C validator