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

Theorem xporderlem 7804
 Description: Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.)
Hypothesis
Ref Expression
xporderlem.1 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
Assertion
Ref Expression
xporderlem (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝑎,𝑦   𝑥,𝑏,𝑦   𝑥,𝑐,𝑦   𝑥,𝑑,𝑦
Allowed substitution hints:   𝐴(𝑎,𝑏,𝑐,𝑑)   𝐵(𝑎,𝑏,𝑐,𝑑)   𝑅(𝑎,𝑏,𝑐,𝑑)   𝑆(𝑎,𝑏,𝑐,𝑑)   𝑇(𝑥,𝑦,𝑎,𝑏,𝑐,𝑑)

Proof of Theorem xporderlem
StepHypRef Expression
1 df-br 5031 . . 3 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ 𝑇)
2 xporderlem.1 . . . 4 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
32eleq2i 2881 . . 3 (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ 𝑇 ↔ ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))})
41, 3bitri 278 . 2 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))})
5 opex 5321 . . 3 𝑎, 𝑏⟩ ∈ V
6 opex 5321 . . 3 𝑐, 𝑑⟩ ∈ V
7 eleq1 2877 . . . . . 6 (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
8 opelxp 5555 . . . . . 6 (⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵) ↔ (𝑎𝐴𝑏𝐵))
97, 8syl6bb 290 . . . . 5 (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ∈ (𝐴 × 𝐵) ↔ (𝑎𝐴𝑏𝐵)))
109anbi1d 632 . . . 4 (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ ((𝑎𝐴𝑏𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
11 vex 3444 . . . . . . 7 𝑎 ∈ V
12 vex 3444 . . . . . . 7 𝑏 ∈ V
1311, 12op1std 7681 . . . . . 6 (𝑥 = ⟨𝑎, 𝑏⟩ → (1st𝑥) = 𝑎)
1413breq1d 5040 . . . . 5 (𝑥 = ⟨𝑎, 𝑏⟩ → ((1st𝑥)𝑅(1st𝑦) ↔ 𝑎𝑅(1st𝑦)))
1513eqeq1d 2800 . . . . . 6 (𝑥 = ⟨𝑎, 𝑏⟩ → ((1st𝑥) = (1st𝑦) ↔ 𝑎 = (1st𝑦)))
1611, 12op2ndd 7682 . . . . . . 7 (𝑥 = ⟨𝑎, 𝑏⟩ → (2nd𝑥) = 𝑏)
1716breq1d 5040 . . . . . 6 (𝑥 = ⟨𝑎, 𝑏⟩ → ((2nd𝑥)𝑆(2nd𝑦) ↔ 𝑏𝑆(2nd𝑦)))
1815, 17anbi12d 633 . . . . 5 (𝑥 = ⟨𝑎, 𝑏⟩ → (((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)) ↔ (𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦))))
1914, 18orbi12d 916 . . . 4 (𝑥 = ⟨𝑎, 𝑏⟩ → (((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))) ↔ (𝑎𝑅(1st𝑦) ∨ (𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦)))))
2010, 19anbi12d 633 . . 3 (𝑥 = ⟨𝑎, 𝑏⟩ → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)))) ↔ (((𝑎𝐴𝑏𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ (𝑎𝑅(1st𝑦) ∨ (𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦))))))
21 eleq1 2877 . . . . . 6 (𝑦 = ⟨𝑐, 𝑑⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵)))
22 opelxp 5555 . . . . . 6 (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ↔ (𝑐𝐴𝑑𝐵))
2321, 22syl6bb 290 . . . . 5 (𝑦 = ⟨𝑐, 𝑑⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ (𝑐𝐴𝑑𝐵)))
2423anbi2d 631 . . . 4 (𝑦 = ⟨𝑐, 𝑑⟩ → (((𝑎𝐴𝑏𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵))))
25 vex 3444 . . . . . . 7 𝑐 ∈ V
26 vex 3444 . . . . . . 7 𝑑 ∈ V
2725, 26op1std 7681 . . . . . 6 (𝑦 = ⟨𝑐, 𝑑⟩ → (1st𝑦) = 𝑐)
2827breq2d 5042 . . . . 5 (𝑦 = ⟨𝑐, 𝑑⟩ → (𝑎𝑅(1st𝑦) ↔ 𝑎𝑅𝑐))
2927eqeq2d 2809 . . . . . 6 (𝑦 = ⟨𝑐, 𝑑⟩ → (𝑎 = (1st𝑦) ↔ 𝑎 = 𝑐))
3025, 26op2ndd 7682 . . . . . . 7 (𝑦 = ⟨𝑐, 𝑑⟩ → (2nd𝑦) = 𝑑)
3130breq2d 5042 . . . . . 6 (𝑦 = ⟨𝑐, 𝑑⟩ → (𝑏𝑆(2nd𝑦) ↔ 𝑏𝑆𝑑))
3229, 31anbi12d 633 . . . . 5 (𝑦 = ⟨𝑐, 𝑑⟩ → ((𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦)) ↔ (𝑎 = 𝑐𝑏𝑆𝑑)))
3328, 32orbi12d 916 . . . 4 (𝑦 = ⟨𝑐, 𝑑⟩ → ((𝑎𝑅(1st𝑦) ∨ (𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦))) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
3424, 33anbi12d 633 . . 3 (𝑦 = ⟨𝑐, 𝑑⟩ → ((((𝑎𝐴𝑏𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ (𝑎𝑅(1st𝑦) ∨ (𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦)))) ↔ (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)))))
355, 6, 20, 34opelopab 5394 . 2 (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))} ↔ (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
36 an4 655 . . 3 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) ↔ ((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)))
3736anbi1i 626 . 2 ((((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
384, 35, 373bitri 300 1 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  ⟨cop 4531   class class class wbr 5030  {copab 5092   × cxp 5517  ‘cfv 6324  1st c1st 7669  2nd c2nd 7670 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6283  df-fun 6326  df-fv 6332  df-1st 7671  df-2nd 7672 This theorem is referenced by:  poxp  7805  soxp  7806
 Copyright terms: Public domain W3C validator