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

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

Proof of Theorem toslublem
StepHypRef Expression
1 toslub.1 . . . . . 6 (𝜑𝐾 ∈ Toset)
21ad2antrr 761 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → 𝐾 ∈ Toset)
3 simplr 791 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → 𝑎𝐵)
4 toslub.2 . . . . . . 7 (𝜑𝐴𝐵)
54adantr 481 . . . . . 6 ((𝜑𝑎𝐵) → 𝐴𝐵)
65sselda 3587 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → 𝑏𝐵)
7 toslub.b . . . . . 6 𝐵 = (Base‘𝐾)
8 toslub.e . . . . . 6 = (le‘𝐾)
9 toslub.l . . . . . 6 < = (lt‘𝐾)
107, 8, 9tltnle 29471 . . . . 5 ((𝐾 ∈ Toset ∧ 𝑎𝐵𝑏𝐵) → (𝑎 < 𝑏 ↔ ¬ 𝑏 𝑎))
112, 3, 6, 10syl3anc 1323 . . . 4 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → (𝑎 < 𝑏 ↔ ¬ 𝑏 𝑎))
1211con2bid 344 . . 3 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → (𝑏 𝑎 ↔ ¬ 𝑎 < 𝑏))
1312ralbidva 2980 . 2 ((𝜑𝑎𝐵) → (∀𝑏𝐴 𝑏 𝑎 ↔ ∀𝑏𝐴 ¬ 𝑎 < 𝑏))
144ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → 𝐴𝐵)
15 simpr 477 . . . . . . . . . . 11 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → 𝑏𝐴)
1614, 15sseldd 3588 . . . . . . . . . 10 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → 𝑏𝐵)
177, 8, 9tltnle 29471 . . . . . . . . . . . . 13 ((𝐾 ∈ Toset ∧ 𝑐𝐵𝑏𝐵) → (𝑐 < 𝑏 ↔ ¬ 𝑏 𝑐))
181, 17syl3an1 1356 . . . . . . . . . . . 12 ((𝜑𝑐𝐵𝑏𝐵) → (𝑐 < 𝑏 ↔ ¬ 𝑏 𝑐))
19183expa 1262 . . . . . . . . . . 11 (((𝜑𝑐𝐵) ∧ 𝑏𝐵) → (𝑐 < 𝑏 ↔ ¬ 𝑏 𝑐))
2019con2bid 344 . . . . . . . . . 10 (((𝜑𝑐𝐵) ∧ 𝑏𝐵) → (𝑏 𝑐 ↔ ¬ 𝑐 < 𝑏))
2116, 20syldan 487 . . . . . . . . 9 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → (𝑏 𝑐 ↔ ¬ 𝑐 < 𝑏))
2221ralbidva 2980 . . . . . . . 8 ((𝜑𝑐𝐵) → (∀𝑏𝐴 𝑏 𝑐 ↔ ∀𝑏𝐴 ¬ 𝑐 < 𝑏))
23 breq2 4622 . . . . . . . . . . 11 (𝑏 = 𝑑 → (𝑐 < 𝑏𝑐 < 𝑑))
2423notbid 308 . . . . . . . . . 10 (𝑏 = 𝑑 → (¬ 𝑐 < 𝑏 ↔ ¬ 𝑐 < 𝑑))
2524cbvralv 3162 . . . . . . . . 9 (∀𝑏𝐴 ¬ 𝑐 < 𝑏 ↔ ∀𝑑𝐴 ¬ 𝑐 < 𝑑)
26 ralnex 2987 . . . . . . . . 9 (∀𝑑𝐴 ¬ 𝑐 < 𝑑 ↔ ¬ ∃𝑑𝐴 𝑐 < 𝑑)
2725, 26bitri 264 . . . . . . . 8 (∀𝑏𝐴 ¬ 𝑐 < 𝑏 ↔ ¬ ∃𝑑𝐴 𝑐 < 𝑑)
2822, 27syl6bb 276 . . . . . . 7 ((𝜑𝑐𝐵) → (∀𝑏𝐴 𝑏 𝑐 ↔ ¬ ∃𝑑𝐴 𝑐 < 𝑑))
2928adantlr 750 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → (∀𝑏𝐴 𝑏 𝑐 ↔ ¬ ∃𝑑𝐴 𝑐 < 𝑑))
301ad2antrr 761 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → 𝐾 ∈ Toset)
31 simpr 477 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → 𝑐𝐵)
32 simplr 791 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → 𝑎𝐵)
337, 8, 9tltnle 29471 . . . . . . . 8 ((𝐾 ∈ Toset ∧ 𝑐𝐵𝑎𝐵) → (𝑐 < 𝑎 ↔ ¬ 𝑎 𝑐))
3430, 31, 32, 33syl3anc 1323 . . . . . . 7 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → (𝑐 < 𝑎 ↔ ¬ 𝑎 𝑐))
3534con2bid 344 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → (𝑎 𝑐 ↔ ¬ 𝑐 < 𝑎))
3629, 35imbi12d 334 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → ((∀𝑏𝐴 𝑏 𝑐𝑎 𝑐) ↔ (¬ ∃𝑑𝐴 𝑐 < 𝑑 → ¬ 𝑐 < 𝑎)))
37 con34b 306 . . . . 5 ((𝑐 < 𝑎 → ∃𝑑𝐴 𝑐 < 𝑑) ↔ (¬ ∃𝑑𝐴 𝑐 < 𝑑 → ¬ 𝑐 < 𝑎))
3836, 37syl6bbr 278 . . . 4 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → ((∀𝑏𝐴 𝑏 𝑐𝑎 𝑐) ↔ (𝑐 < 𝑎 → ∃𝑑𝐴 𝑐 < 𝑑)))
3938ralbidva 2980 . . 3 ((𝜑𝑎𝐵) → (∀𝑐𝐵 (∀𝑏𝐴 𝑏 𝑐𝑎 𝑐) ↔ ∀𝑐𝐵 (𝑐 < 𝑎 → ∃𝑑𝐴 𝑐 < 𝑑)))
40 breq1 4621 . . . . 5 (𝑏 = 𝑐 → (𝑏 < 𝑎𝑐 < 𝑎))
41 breq1 4621 . . . . . 6 (𝑏 = 𝑐 → (𝑏 < 𝑑𝑐 < 𝑑))
4241rexbidv 3046 . . . . 5 (𝑏 = 𝑐 → (∃𝑑𝐴 𝑏 < 𝑑 ↔ ∃𝑑𝐴 𝑐 < 𝑑))
4340, 42imbi12d 334 . . . 4 (𝑏 = 𝑐 → ((𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑) ↔ (𝑐 < 𝑎 → ∃𝑑𝐴 𝑐 < 𝑑)))
4443cbvralv 3162 . . 3 (∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑) ↔ ∀𝑐𝐵 (𝑐 < 𝑎 → ∃𝑑𝐴 𝑐 < 𝑑))
4539, 44syl6bbr 278 . 2 ((𝜑𝑎𝐵) → (∀𝑐𝐵 (∀𝑏𝐴 𝑏 𝑐𝑎 𝑐) ↔ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑)))
4613, 45anbi12d 746 1 ((𝜑𝑎𝐵) → ((∀𝑏𝐴 𝑏 𝑎 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑏 𝑐𝑎 𝑐)) ↔ (∀𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  wrex 2908  wss 3559   class class class wbr 4618  cfv 5852  Basecbs 15792  lecple 15880  ltcplt 16873  Tosetctos 16965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-iota 5815  df-fun 5854  df-fv 5860  df-preset 16860  df-poset 16878  df-plt 16890  df-toset 16966
This theorem is referenced by:  toslub  29477  xrsclat  29489
  Copyright terms: Public domain W3C validator