Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvrnbtwn Structured version   Visualization version   GIF version

Theorem cvrnbtwn 34073
 Description: There is no element between the two arguments of the covers relation. (cvnbtwn 29015 analog.) (Contributed by NM, 18-Oct-2011.)
Hypotheses
Ref Expression
cvrfval.b 𝐵 = (Base‘𝐾)
cvrfval.s < = (lt‘𝐾)
cvrfval.c 𝐶 = ( ⋖ ‘𝐾)
Assertion
Ref Expression
cvrnbtwn ((𝐾𝐴 ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ 𝑋𝐶𝑌) → ¬ (𝑋 < 𝑍𝑍 < 𝑌))

Proof of Theorem cvrnbtwn
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 cvrfval.b . . . . 5 𝐵 = (Base‘𝐾)
2 cvrfval.s . . . . 5 < = (lt‘𝐾)
3 cvrfval.c . . . . 5 𝐶 = ( ⋖ ‘𝐾)
41, 2, 3cvrval 34071 . . . 4 ((𝐾𝐴𝑋𝐵𝑌𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ¬ ∃𝑧𝐵 (𝑋 < 𝑧𝑧 < 𝑌))))
543adant3r3 1273 . . 3 ((𝐾𝐴 ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ¬ ∃𝑧𝐵 (𝑋 < 𝑧𝑧 < 𝑌))))
6 ralnex 2987 . . . . . . 7 (∀𝑧𝐵 ¬ (𝑋 < 𝑧𝑧 < 𝑌) ↔ ¬ ∃𝑧𝐵 (𝑋 < 𝑧𝑧 < 𝑌))
7 breq2 4622 . . . . . . . . . 10 (𝑧 = 𝑍 → (𝑋 < 𝑧𝑋 < 𝑍))
8 breq1 4621 . . . . . . . . . 10 (𝑧 = 𝑍 → (𝑧 < 𝑌𝑍 < 𝑌))
97, 8anbi12d 746 . . . . . . . . 9 (𝑧 = 𝑍 → ((𝑋 < 𝑧𝑧 < 𝑌) ↔ (𝑋 < 𝑍𝑍 < 𝑌)))
109notbid 308 . . . . . . . 8 (𝑧 = 𝑍 → (¬ (𝑋 < 𝑧𝑧 < 𝑌) ↔ ¬ (𝑋 < 𝑍𝑍 < 𝑌)))
1110rspcv 3294 . . . . . . 7 (𝑍𝐵 → (∀𝑧𝐵 ¬ (𝑋 < 𝑧𝑧 < 𝑌) → ¬ (𝑋 < 𝑍𝑍 < 𝑌)))
126, 11syl5bir 233 . . . . . 6 (𝑍𝐵 → (¬ ∃𝑧𝐵 (𝑋 < 𝑧𝑧 < 𝑌) → ¬ (𝑋 < 𝑍𝑍 < 𝑌)))
1312adantld 483 . . . . 5 (𝑍𝐵 → ((𝑋 < 𝑌 ∧ ¬ ∃𝑧𝐵 (𝑋 < 𝑧𝑧 < 𝑌)) → ¬ (𝑋 < 𝑍𝑍 < 𝑌)))
14133ad2ant3 1082 . . . 4 ((𝑋𝐵𝑌𝐵𝑍𝐵) → ((𝑋 < 𝑌 ∧ ¬ ∃𝑧𝐵 (𝑋 < 𝑧𝑧 < 𝑌)) → ¬ (𝑋 < 𝑍𝑍 < 𝑌)))
1514adantl 482 . . 3 ((𝐾𝐴 ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 < 𝑌 ∧ ¬ ∃𝑧𝐵 (𝑋 < 𝑧𝑧 < 𝑌)) → ¬ (𝑋 < 𝑍𝑍 < 𝑌)))
165, 15sylbid 230 . 2 ((𝐾𝐴 ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑌 → ¬ (𝑋 < 𝑍𝑍 < 𝑌)))
17163impia 1258 1 ((𝐾𝐴 ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ 𝑋𝐶𝑌) → ¬ (𝑋 < 𝑍𝑍 < 𝑌))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908   class class class wbr 4618  ‘cfv 5852  Basecbs 15792  ltcplt 16873   ⋖ ccvr 34064 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-8 1989  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-pow 4808  ax-pr 4872  ax-un 6909 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-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-pw 4137  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-covers 34068 This theorem is referenced by:  cvrnbtwn2  34077  cvrnbtwn3  34078  cvrnbtwn4  34081  ltltncvr  34224
 Copyright terms: Public domain W3C validator