MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  legtrid Structured version   Visualization version   GIF version

Theorem legtrid 26537
Description: Trichotomy law for the less-than relationship. Proposition 5.10 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
Hypotheses
Ref Expression
legval.p 𝑃 = (Base‘𝐺)
legval.d = (dist‘𝐺)
legval.i 𝐼 = (Itv‘𝐺)
legval.l = (≤G‘𝐺)
legval.g (𝜑𝐺 ∈ TarskiG)
legid.a (𝜑𝐴𝑃)
legid.b (𝜑𝐵𝑃)
legtrd.c (𝜑𝐶𝑃)
legtrd.d (𝜑𝐷𝑃)
Assertion
Ref Expression
legtrid (𝜑 → ((𝐴 𝐵) (𝐶 𝐷) ∨ (𝐶 𝐷) (𝐴 𝐵)))

Proof of Theorem legtrid
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 legval.p . . . . 5 𝑃 = (Base‘𝐺)
2 legval.d . . . . 5 = (dist‘𝐺)
3 legval.i . . . . 5 𝐼 = (Itv‘𝐺)
4 legval.l . . . . 5 = (≤G‘𝐺)
5 legval.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
65adantr 484 . . . . 5 ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐺 ∈ TarskiG)
7 legid.a . . . . . 6 (𝜑𝐴𝑃)
87adantr 484 . . . . 5 ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐴𝑃)
9 legid.b . . . . . 6 (𝜑𝐵𝑃)
109adantr 484 . . . . 5 ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐵𝑃)
111, 2, 3, 4, 6, 8, 10legid 26533 . . . 4 ((𝜑 ∧ (♯‘𝑃) = 1) → (𝐴 𝐵) (𝐴 𝐵))
12 legtrd.c . . . . . 6 (𝜑𝐶𝑃)
1312adantr 484 . . . . 5 ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐶𝑃)
14 simpr 488 . . . . 5 ((𝜑 ∧ (♯‘𝑃) = 1) → (♯‘𝑃) = 1)
15 legtrd.d . . . . . 6 (𝜑𝐷𝑃)
1615adantr 484 . . . . 5 ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐷𝑃)
171, 2, 3, 6, 8, 10, 13, 14, 16tgldim0cgr 26451 . . . 4 ((𝜑 ∧ (♯‘𝑃) = 1) → (𝐴 𝐵) = (𝐶 𝐷))
1811, 17breqtrd 5057 . . 3 ((𝜑 ∧ (♯‘𝑃) = 1) → (𝐴 𝐵) (𝐶 𝐷))
1918orcd 872 . 2 ((𝜑 ∧ (♯‘𝑃) = 1) → ((𝐴 𝐵) (𝐶 𝐷) ∨ (𝐶 𝐷) (𝐴 𝐵)))
205ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → 𝐺 ∈ TarskiG)
21 simplr 769 . . . . . . . . . 10 (((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) → 𝑥𝑃)
2221adantr 484 . . . . . . . . 9 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → 𝑥𝑃)
237ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → 𝐴𝑃)
249ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → 𝐵𝑃)
25 simprl 771 . . . . . . . . 9 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → 𝑦𝑃)
26 simplrr 778 . . . . . . . . . 10 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → 𝐴𝑥)
2726necomd 2989 . . . . . . . . 9 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → 𝑥𝐴)
28 simplrl 777 . . . . . . . . . 10 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → 𝐴 ∈ (𝐵𝐼𝑥))
291, 2, 3, 20, 24, 23, 22, 28tgbtwncom 26434 . . . . . . . . 9 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → 𝐴 ∈ (𝑥𝐼𝐵))
30 simprrl 781 . . . . . . . . 9 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → 𝐴 ∈ (𝑥𝐼𝑦))
311, 3, 20, 22, 23, 24, 25, 27, 29, 30tgbtwnconn2 26522 . . . . . . . 8 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → (𝐵 ∈ (𝐴𝐼𝑦) ∨ 𝑦 ∈ (𝐴𝐼𝐵)))
32 simprrr 782 . . . . . . . 8 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → (𝐴 𝑦) = (𝐶 𝐷))
3331, 32jca 515 . . . . . . 7 ((((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) ∧ (𝑦𝑃 ∧ (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))) → ((𝐵 ∈ (𝐴𝐼𝑦) ∨ 𝑦 ∈ (𝐴𝐼𝐵)) ∧ (𝐴 𝑦) = (𝐶 𝐷)))
345ad2antrr 726 . . . . . . . 8 (((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) → 𝐺 ∈ TarskiG)
357ad2antrr 726 . . . . . . . 8 (((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) → 𝐴𝑃)
3612ad2antrr 726 . . . . . . . 8 (((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) → 𝐶𝑃)
3715ad2antrr 726 . . . . . . . 8 (((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) → 𝐷𝑃)
381, 2, 3, 34, 21, 35, 36, 37axtgsegcon 26410 . . . . . . 7 (((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) → ∃𝑦𝑃 (𝐴 ∈ (𝑥𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)))
3933, 38reximddv 3185 . . . . . 6 (((𝜑𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) → ∃𝑦𝑃 ((𝐵 ∈ (𝐴𝐼𝑦) ∨ 𝑦 ∈ (𝐴𝐼𝐵)) ∧ (𝐴 𝑦) = (𝐶 𝐷)))
4039adantllr 719 . . . . 5 ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑥𝑃) ∧ (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥)) → ∃𝑦𝑃 ((𝐵 ∈ (𝐴𝐼𝑦) ∨ 𝑦 ∈ (𝐴𝐼𝐵)) ∧ (𝐴 𝑦) = (𝐶 𝐷)))
415adantr 484 . . . . . 6 ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 𝐺 ∈ TarskiG)
429adantr 484 . . . . . 6 ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 𝐵𝑃)
437adantr 484 . . . . . 6 ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 𝐴𝑃)
44 simpr 488 . . . . . 6 ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 2 ≤ (♯‘𝑃))
451, 2, 3, 41, 42, 43, 44tgbtwndiff 26452 . . . . 5 ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → ∃𝑥𝑃 (𝐴 ∈ (𝐵𝐼𝑥) ∧ 𝐴𝑥))
4640, 45r19.29a 3199 . . . 4 ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → ∃𝑦𝑃 ((𝐵 ∈ (𝐴𝐼𝑦) ∨ 𝑦 ∈ (𝐴𝐼𝐵)) ∧ (𝐴 𝑦) = (𝐶 𝐷)))
47 andir 1008 . . . . . . 7 (((𝐵 ∈ (𝐴𝐼𝑦) ∨ 𝑦 ∈ (𝐴𝐼𝐵)) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ↔ ((𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐴 𝑦) = (𝐶 𝐷))))
48 eqcom 2745 . . . . . . . . 9 ((𝐴 𝑦) = (𝐶 𝐷) ↔ (𝐶 𝐷) = (𝐴 𝑦))
4948anbi2i 626 . . . . . . . 8 ((𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ↔ (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦)))
5049orbi2i 912 . . . . . . 7 (((𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐴 𝑦) = (𝐶 𝐷))) ↔ ((𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦))))
5147, 50bitri 278 . . . . . 6 (((𝐵 ∈ (𝐴𝐼𝑦) ∨ 𝑦 ∈ (𝐴𝐼𝐵)) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ↔ ((𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦))))
5251rexbii 3161 . . . . 5 (∃𝑦𝑃 ((𝐵 ∈ (𝐴𝐼𝑦) ∨ 𝑦 ∈ (𝐴𝐼𝐵)) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ↔ ∃𝑦𝑃 ((𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦))))
53 r19.43 3255 . . . . 5 (∃𝑦𝑃 ((𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦))) ↔ (∃𝑦𝑃 (𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ ∃𝑦𝑃 (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦))))
5452, 53bitri 278 . . . 4 (∃𝑦𝑃 ((𝐵 ∈ (𝐴𝐼𝑦) ∨ 𝑦 ∈ (𝐴𝐼𝐵)) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ↔ (∃𝑦𝑃 (𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ ∃𝑦𝑃 (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦))))
5546, 54sylib 221 . . 3 ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑦𝑃 (𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ ∃𝑦𝑃 (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦))))
561, 2, 3, 4, 5, 7, 9, 12, 15legov2 26532 . . . . 5 (𝜑 → ((𝐴 𝐵) (𝐶 𝐷) ↔ ∃𝑦𝑃 (𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷))))
571, 2, 3, 4, 5, 12, 15, 7, 9legov 26531 . . . . 5 (𝜑 → ((𝐶 𝐷) (𝐴 𝐵) ↔ ∃𝑦𝑃 (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦))))
5856, 57orbi12d 918 . . . 4 (𝜑 → (((𝐴 𝐵) (𝐶 𝐷) ∨ (𝐶 𝐷) (𝐴 𝐵)) ↔ (∃𝑦𝑃 (𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ ∃𝑦𝑃 (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦)))))
5958adantr 484 . . 3 ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → (((𝐴 𝐵) (𝐶 𝐷) ∨ (𝐶 𝐷) (𝐴 𝐵)) ↔ (∃𝑦𝑃 (𝐵 ∈ (𝐴𝐼𝑦) ∧ (𝐴 𝑦) = (𝐶 𝐷)) ∨ ∃𝑦𝑃 (𝑦 ∈ (𝐴𝐼𝐵) ∧ (𝐶 𝐷) = (𝐴 𝑦)))))
6055, 59mpbird 260 . 2 ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → ((𝐴 𝐵) (𝐶 𝐷) ∨ (𝐶 𝐷) (𝐴 𝐵)))
611, 7tgldimor 26448 . 2 (𝜑 → ((♯‘𝑃) = 1 ∨ 2 ≤ (♯‘𝑃)))
6219, 60, 61mpjaodan 958 1 (𝜑 → ((𝐴 𝐵) (𝐶 𝐷) ∨ (𝐶 𝐷) (𝐴 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 846   = wceq 1542  wcel 2113  wne 2934  wrex 3054   class class class wbr 5031  cfv 6340  (class class class)co 7171  1c1 10617  cle 10755  2c2 11772  chash 13783  Basecbs 16587  distcds 16678  TarskiGcstrkg 26376  Itvcitv 26382  ≤Gcleg 26528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7480  ax-cnex 10672  ax-resscn 10673  ax-1cn 10674  ax-icn 10675  ax-addcl 10676  ax-addrcl 10677  ax-mulcl 10678  ax-mulrcl 10679  ax-mulcom 10680  ax-addass 10681  ax-mulass 10682  ax-distr 10683  ax-i2m1 10684  ax-1ne0 10685  ax-1rid 10686  ax-rnegex 10687  ax-rrecex 10688  ax-cnre 10689  ax-pre-lttri 10690  ax-pre-lttrn 10691  ax-pre-ltadd 10692  ax-pre-mulgt0 10693
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3683  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-int 4838  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7128  df-ov 7174  df-oprab 7175  df-mpo 7176  df-om 7601  df-1st 7715  df-2nd 7716  df-wrecs 7977  df-recs 8038  df-rdg 8076  df-1o 8132  df-oadd 8136  df-er 8321  df-pm 8441  df-en 8557  df-dom 8558  df-sdom 8559  df-fin 8560  df-dju 9404  df-card 9442  df-pnf 10756  df-mnf 10757  df-xr 10758  df-ltxr 10759  df-le 10760  df-sub 10951  df-neg 10952  df-nn 11718  df-2 11780  df-3 11781  df-n0 11978  df-xnn0 12050  df-z 12064  df-uz 12326  df-fz 12983  df-fzo 13126  df-hash 13784  df-word 13957  df-concat 14013  df-s1 14040  df-s2 14300  df-s3 14301  df-trkgc 26394  df-trkgb 26395  df-trkgcb 26396  df-trkg 26399  df-cgrg 26457  df-leg 26529
This theorem is referenced by:  legso  26545  krippen  26637  midex  26683  opphllem5  26697  opphllem6  26698
  Copyright terms: Public domain W3C validator