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 31239
Description: Lemma for tosglb 31240 and xrsclat 31276. (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 723 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → 𝐾 ∈ Toset)
3 tosglb.2 . . . . . . . 8 (𝜑𝐴𝐵)
43adantr 481 . . . . . . 7 ((𝜑𝑎𝐵) → 𝐴𝐵)
54sselda 3922 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → 𝑏𝐵)
6 simplr 766 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → 𝑎𝐵)
7 tosglb.b . . . . . . 7 𝐵 = (Base‘𝐾)
8 tosglb.e . . . . . . 7 = (le‘𝐾)
9 tosglb.l . . . . . . 7 < = (lt‘𝐾)
107, 8, 9tltnle 18129 . . . . . 6 ((𝐾 ∈ Toset ∧ 𝑏𝐵𝑎𝐵) → (𝑏 < 𝑎 ↔ ¬ 𝑎 𝑏))
112, 5, 6, 10syl3anc 1370 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → (𝑏 < 𝑎 ↔ ¬ 𝑎 𝑏))
1211con2bid 355 . . . 4 (((𝜑𝑎𝐵) ∧ 𝑏𝐴) → (𝑎 𝑏 ↔ ¬ 𝑏 < 𝑎))
1312ralbidva 3117 . . 3 ((𝜑𝑎𝐵) → (∀𝑏𝐴 𝑎 𝑏 ↔ ∀𝑏𝐴 ¬ 𝑏 < 𝑎))
143ad2antrr 723 . . . . . . . . . . . 12 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → 𝐴𝐵)
15 simpr 485 . . . . . . . . . . . 12 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → 𝑏𝐴)
1614, 15sseldd 3923 . . . . . . . . . . 11 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → 𝑏𝐵)
177, 8, 9tltnle 18129 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Toset ∧ 𝑏𝐵𝑐𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏))
181, 17syl3an1 1162 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵𝑐𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏))
19183com23 1125 . . . . . . . . . . . . 13 ((𝜑𝑐𝐵𝑏𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏))
20193expa 1117 . . . . . . . . . . . 12 (((𝜑𝑐𝐵) ∧ 𝑏𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 𝑏))
2120con2bid 355 . . . . . . . . . . 11 (((𝜑𝑐𝐵) ∧ 𝑏𝐵) → (𝑐 𝑏 ↔ ¬ 𝑏 < 𝑐))
2216, 21syldan 591 . . . . . . . . . 10 (((𝜑𝑐𝐵) ∧ 𝑏𝐴) → (𝑐 𝑏 ↔ ¬ 𝑏 < 𝑐))
2322ralbidva 3117 . . . . . . . . 9 ((𝜑𝑐𝐵) → (∀𝑏𝐴 𝑐 𝑏 ↔ ∀𝑏𝐴 ¬ 𝑏 < 𝑐))
24 breq1 5078 . . . . . . . . . . . 12 (𝑏 = 𝑑 → (𝑏 < 𝑐𝑑 < 𝑐))
2524notbid 318 . . . . . . . . . . 11 (𝑏 = 𝑑 → (¬ 𝑏 < 𝑐 ↔ ¬ 𝑑 < 𝑐))
2625cbvralvw 3382 . . . . . . . . . 10 (∀𝑏𝐴 ¬ 𝑏 < 𝑐 ↔ ∀𝑑𝐴 ¬ 𝑑 < 𝑐)
27 ralnex 3166 . . . . . . . . . 10 (∀𝑑𝐴 ¬ 𝑑 < 𝑐 ↔ ¬ ∃𝑑𝐴 𝑑 < 𝑐)
2826, 27bitri 274 . . . . . . . . 9 (∀𝑏𝐴 ¬ 𝑏 < 𝑐 ↔ ¬ ∃𝑑𝐴 𝑑 < 𝑐)
2923, 28bitrdi 287 . . . . . . . 8 ((𝜑𝑐𝐵) → (∀𝑏𝐴 𝑐 𝑏 ↔ ¬ ∃𝑑𝐴 𝑑 < 𝑐))
3029adantlr 712 . . . . . . 7 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → (∀𝑏𝐴 𝑐 𝑏 ↔ ¬ ∃𝑑𝐴 𝑑 < 𝑐))
311ad2antrr 723 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → 𝐾 ∈ Toset)
32 simplr 766 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → 𝑎𝐵)
33 simpr 485 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → 𝑐𝐵)
347, 8, 9tltnle 18129 . . . . . . . . 9 ((𝐾 ∈ Toset ∧ 𝑎𝐵𝑐𝐵) → (𝑎 < 𝑐 ↔ ¬ 𝑐 𝑎))
3531, 32, 33, 34syl3anc 1370 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → (𝑎 < 𝑐 ↔ ¬ 𝑐 𝑎))
3635con2bid 355 . . . . . . 7 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → (𝑐 𝑎 ↔ ¬ 𝑎 < 𝑐))
3730, 36imbi12d 345 . . . . . 6 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → ((∀𝑏𝐴 𝑐 𝑏𝑐 𝑎) ↔ (¬ ∃𝑑𝐴 𝑑 < 𝑐 → ¬ 𝑎 < 𝑐)))
38 con34b 316 . . . . . 6 ((𝑎 < 𝑐 → ∃𝑑𝐴 𝑑 < 𝑐) ↔ (¬ ∃𝑑𝐴 𝑑 < 𝑐 → ¬ 𝑎 < 𝑐))
3937, 38bitr4di 289 . . . . 5 (((𝜑𝑎𝐵) ∧ 𝑐𝐵) → ((∀𝑏𝐴 𝑐 𝑏𝑐 𝑎) ↔ (𝑎 < 𝑐 → ∃𝑑𝐴 𝑑 < 𝑐)))
4039ralbidva 3117 . . . 4 ((𝜑𝑎𝐵) → (∀𝑐𝐵 (∀𝑏𝐴 𝑐 𝑏𝑐 𝑎) ↔ ∀𝑐𝐵 (𝑎 < 𝑐 → ∃𝑑𝐴 𝑑 < 𝑐)))
41 breq2 5079 . . . . . 6 (𝑏 = 𝑐 → (𝑎 < 𝑏𝑎 < 𝑐))
42 breq2 5079 . . . . . . 7 (𝑏 = 𝑐 → (𝑑 < 𝑏𝑑 < 𝑐))
4342rexbidv 3225 . . . . . 6 (𝑏 = 𝑐 → (∃𝑑𝐴 𝑑 < 𝑏 ↔ ∃𝑑𝐴 𝑑 < 𝑐))
4441, 43imbi12d 345 . . . . 5 (𝑏 = 𝑐 → ((𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏) ↔ (𝑎 < 𝑐 → ∃𝑑𝐴 𝑑 < 𝑐)))
4544cbvralvw 3382 . . . 4 (∀𝑏𝐵 (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏) ↔ ∀𝑐𝐵 (𝑎 < 𝑐 → ∃𝑑𝐴 𝑑 < 𝑐))
4640, 45bitr4di 289 . . 3 ((𝜑𝑎𝐵) → (∀𝑐𝐵 (∀𝑏𝐴 𝑐 𝑏𝑐 𝑎) ↔ ∀𝑏𝐵 (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏)))
4713, 46anbi12d 631 . 2 ((𝜑𝑎𝐵) → ((∀𝑏𝐴 𝑎 𝑏 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑐 𝑏𝑐 𝑎)) ↔ (∀𝑏𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏𝐵 (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏))))
48 vex 3435 . . . . . 6 𝑎 ∈ V
49 vex 3435 . . . . . 6 𝑏 ∈ V
5048, 49brcnv 5786 . . . . 5 (𝑎 < 𝑏𝑏 < 𝑎)
5150notbii 320 . . . 4 𝑎 < 𝑏 ↔ ¬ 𝑏 < 𝑎)
5251ralbii 3092 . . 3 (∀𝑏𝐴 ¬ 𝑎 < 𝑏 ↔ ∀𝑏𝐴 ¬ 𝑏 < 𝑎)
5349, 48brcnv 5786 . . . . 5 (𝑏 < 𝑎𝑎 < 𝑏)
54 vex 3435 . . . . . . 7 𝑑 ∈ V
5549, 54brcnv 5786 . . . . . 6 (𝑏 < 𝑑𝑑 < 𝑏)
5655rexbii 3180 . . . . 5 (∃𝑑𝐴 𝑏 < 𝑑 ↔ ∃𝑑𝐴 𝑑 < 𝑏)
5753, 56imbi12i 351 . . . 4 ((𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑) ↔ (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏))
5857ralbii 3092 . . 3 (∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑) ↔ ∀𝑏𝐵 (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏))
5952, 58anbi12i 627 . 2 ((∀𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑)) ↔ (∀𝑏𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏𝐵 (𝑎 < 𝑏 → ∃𝑑𝐴 𝑑 < 𝑏)))
6047, 59bitr4di 289 1 ((𝜑𝑎𝐵) → ((∀𝑏𝐴 𝑎 𝑏 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑐 𝑏𝑐 𝑎)) ↔ (∀𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  wral 3064  wrex 3065  wss 3888   class class class wbr 5075  ccnv 5585  cfv 6428  Basecbs 16901  lecple 16958  ltcplt 18015  Tosetctos 18123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5486  df-xp 5592  df-rel 5593  df-cnv 5594  df-co 5595  df-dm 5596  df-iota 6386  df-fun 6430  df-fv 6436  df-proset 18002  df-poset 18020  df-plt 18037  df-toset 18124
This theorem is referenced by:  tosglb  31240  xrsclat  31276
  Copyright terms: Public domain W3C validator