Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tosglblem Structured version   Visualization version   GIF version

Theorem tosglblem 30583
Description: Lemma for tosglb 30584 and xrsclat 30594. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.)
Hypotheses
Ref Expression
tosglb.b 𝐵 = (Base‘𝐾)
tosglb.l < = (lt‘𝐾)
tosglb.1 (𝜑𝐾 ∈ Toset)
tosglb.2 (𝜑𝐴𝐵)
tosglb.e = (le‘𝐾)
Assertion
Ref Expression
tosglblem ((𝜑𝑎𝐵) → ((∀𝑏𝐴 𝑎 𝑏 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑐 𝑏𝑐 𝑎)) ↔ (∀𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑))))
Distinct variable groups:   𝑎,𝑏,𝑐,𝑑, <   𝐴,𝑎,𝑏,𝑐,𝑑   𝐵,𝑎,𝑏,𝑐,𝑑   𝐾,𝑎,𝑏,𝑐   𝜑,𝑎,𝑏,𝑐
Allowed substitution hints:   𝜑(𝑑)   𝐾(𝑑)   (𝑎,𝑏,𝑐,𝑑)

Proof of Theorem tosglblem
StepHypRef Expression
1 tosglb.1 . . . . . . 7 (𝜑𝐾 ∈ Toset)
21ad2antrr 722 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → 𝐾 ∈ Toset)
3 tosglb.2 . . . . . . . 8 (𝜑𝐴𝐵)
43adantr 481 . . . . . . 7 ((𝜑𝑎𝐵) → 𝐴𝐵)
54sselda 3964 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → 𝑏𝐵)
6 simplr 765 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → 𝑎𝐵)
7 tosglb.b . . . . . . 7 𝐵 = (Base‘𝐾)
8 tosglb.e . . . . . . 7 = (le‘𝐾)
9 tosglb.l . . . . . . 7 < = (lt‘𝐾)
107, 8, 9tltnle 30576 . . . . . 6 ((𝐾 ∈ Toset ∧ 𝑏𝐵𝑎𝐵) → (𝑏 < 𝑎 ↔ ¬ 𝑎 𝑏))
112, 5, 6, 10syl3anc 1363 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → (𝑏 < 𝑎 ↔ ¬ 𝑎 𝑏))
1211con2bid 356 . . . 4 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → (𝑎 𝑏 ↔ ¬ 𝑏 < 𝑎))
1312ralbidva 3193 . . 3 ((𝜑𝑎𝐵) → (∀𝑏𝐴 𝑎 𝑏 ↔ ∀𝑏𝐴 ¬ 𝑏 < 𝑎))
143ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → 𝐴𝐵)
15 simpr 485 . . . . . . . . . . . 12 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → 𝑏𝐴)
1614, 15sseldd 3965 . . . . . . . . . . 11 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → 𝑏𝐵)
177, 8, 9tltnle 30576 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Toset ∧ 𝑏𝐵𝑐𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏))
181, 17syl3an1 1155 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵𝑐𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏))
19183com23 1118 . . . . . . . . . . . . 13 ((𝜑𝑐𝐵𝑏𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏))
20193expa 1110 . . . . . . . . . . . 12 (((𝜑𝑐𝐵) ∧ 𝑏𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏))
2120con2bid 356 . . . . . . . . . . 11 (((𝜑𝑐𝐵) ∧ 𝑏𝐵) → (𝑐 𝑏 ↔ ¬ 𝑏 < 𝑐))
2216, 21syldan 591 . . . . . . . . . 10 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → (𝑐 𝑏 ↔ ¬ 𝑏 < 𝑐))
2322ralbidva 3193 . . . . . . . . 9 ((𝜑𝑐𝐵) → (∀𝑏𝐴 𝑐 𝑏 ↔ ∀𝑏𝐴 ¬ 𝑏 < 𝑐))
24 breq1 5060 . . . . . . . . . . . 12 (𝑏 = 𝑑 → (𝑏 < 𝑐𝑑 < 𝑐))
2524notbid 319 . . . . . . . . . . 11 (𝑏 = 𝑑 → (¬ 𝑏 < 𝑐 ↔ ¬ 𝑑 < 𝑐))
2625cbvralvw 3447 . . . . . . . . . 10 (∀𝑏𝐴 ¬ 𝑏 < 𝑐 ↔ ∀𝑑𝐴 ¬ 𝑑 < 𝑐)
27 ralnex 3233 . . . . . . . . . 10 (∀𝑑𝐴 ¬ 𝑑 < 𝑐 ↔ ¬ ∃𝑑𝐴 𝑑 < 𝑐)
2826, 27bitri 276 . . . . . . . . 9 (∀𝑏𝐴 ¬ 𝑏 < 𝑐 ↔ ¬ ∃𝑑𝐴 𝑑 < 𝑐)
2923, 28syl6bb 288 . . . . . . . 8 ((𝜑𝑐𝐵) → (∀𝑏𝐴 𝑐 𝑏 ↔ ¬ ∃𝑑𝐴 𝑑 < 𝑐))
3029adantlr 711 . . . . . . 7 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → (∀𝑏𝐴 𝑐 𝑏 ↔ ¬ ∃𝑑𝐴 𝑑 < 𝑐))
311ad2antrr 722 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → 𝐾 ∈ Toset)
32 simplr 765 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → 𝑎𝐵)
33 simpr 485 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → 𝑐𝐵)
347, 8, 9tltnle 30576 . . . . . . . . 9 ((𝐾 ∈ Toset ∧ 𝑎𝐵𝑐𝐵) → (𝑎 < 𝑐 ↔ ¬ 𝑐 𝑎))
3531, 32, 33, 34syl3anc 1363 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → (𝑎 < 𝑐 ↔ ¬ 𝑐 𝑎))
3635con2bid 356 . . . . . . 7 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → (𝑐 𝑎 ↔ ¬ 𝑎 < 𝑐))
3730, 36imbi12d 346 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → ((∀𝑏𝐴 𝑐 𝑏𝑐 𝑎) ↔ (¬ ∃𝑑𝐴 𝑑 < 𝑐 → ¬ 𝑎 < 𝑐)))
38 con34b 317 . . . . . 6 ((𝑎 < 𝑐 → ∃𝑑𝐴 𝑑 < 𝑐) ↔ (¬ ∃𝑑𝐴 𝑑 < 𝑐 → ¬ 𝑎 < 𝑐))
3937, 38syl6bbr 290 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → ((∀𝑏𝐴 𝑐 𝑏𝑐 𝑎) ↔ (𝑎 < 𝑐 → ∃𝑑𝐴 𝑑 < 𝑐)))
4039ralbidva 3193 . . . 4 ((𝜑𝑎𝐵) → (∀𝑐𝐵 (∀𝑏𝐴 𝑐 𝑏𝑐 𝑎) ↔ ∀𝑐𝐵 (𝑎 < 𝑐 → ∃𝑑𝐴 𝑑 < 𝑐)))
41 breq2 5061 . . . . . 6 (𝑏 = 𝑐 → (𝑎 < 𝑏𝑎 < 𝑐))
42 breq2 5061 . . . . . . 7 (𝑏 = 𝑐 → (𝑑 < 𝑏𝑑 < 𝑐))
4342rexbidv 3294 . . . . . 6 (𝑏 = 𝑐 → (∃𝑑𝐴 𝑑 < 𝑏 ↔ ∃𝑑𝐴 𝑑 < 𝑐))
4441, 43imbi12d 346 . . . . 5 (𝑏 = 𝑐 → ((𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏) ↔ (𝑎 < 𝑐 → ∃𝑑𝐴 𝑑 < 𝑐)))
4544cbvralvw 3447 . . . 4 (∀𝑏𝐵 (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏) ↔ ∀𝑐𝐵 (𝑎 < 𝑐 → ∃𝑑𝐴 𝑑 < 𝑐))
4640, 45syl6bbr 290 . . 3 ((𝜑𝑎𝐵) → (∀𝑐𝐵 (∀𝑏𝐴 𝑐 𝑏𝑐 𝑎) ↔ ∀𝑏𝐵 (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏)))
4713, 46anbi12d 630 . 2 ((𝜑𝑎𝐵) → ((∀𝑏𝐴 𝑎 𝑏 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑐 𝑏𝑐 𝑎)) ↔ (∀𝑏𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏𝐵 (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏))))
48 vex 3495 . . . . . 6 𝑎 ∈ V
49 vex 3495 . . . . . 6 𝑏 ∈ V
5048, 49brcnv 5746 . . . . 5 (𝑎 < 𝑏𝑏 < 𝑎)
5150notbii 321 . . . 4 𝑎 < 𝑏 ↔ ¬ 𝑏 < 𝑎)
5251ralbii 3162 . . 3 (∀𝑏𝐴 ¬ 𝑎 < 𝑏 ↔ ∀𝑏𝐴 ¬ 𝑏 < 𝑎)
5349, 48brcnv 5746 . . . . 5 (𝑏 < 𝑎𝑎 < 𝑏)
54 vex 3495 . . . . . . 7 𝑑 ∈ V
5549, 54brcnv 5746 . . . . . 6 (𝑏 < 𝑑𝑑 < 𝑏)
5655rexbii 3244 . . . . 5 (∃𝑑𝐴 𝑏 < 𝑑 ↔ ∃𝑑𝐴 𝑑 < 𝑏)
5753, 56imbi12i 352 . . . 4 ((𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑) ↔ (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏))
5857ralbii 3162 . . 3 (∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑) ↔ ∀𝑏𝐵 (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏))
5952, 58anbi12i 626 . 2 ((∀𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑)) ↔ (∀𝑏𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏𝐵 (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏)))
6047, 59syl6bbr 290 1 ((𝜑𝑎𝐵) → ((∀𝑏𝐴 𝑎 𝑏 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑐 𝑏𝑐 𝑎)) ↔ (∀𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wral 3135  wrex 3136  wss 3933   class class class wbr 5057  ccnv 5547  cfv 6348  Basecbs 16471  lecple 16560  ltcplt 17539  Tosetctos 17631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-proset 17526  df-poset 17544  df-plt 17556  df-toset 17632
This theorem is referenced by:  tosglb  30584  xrsclat  30594
  Copyright terms: Public domain W3C validator