Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  xporderlem GIF version

Theorem xporderlem 6175
 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 3966 . . 3 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ 𝑇)
2 xporderlem.1 . . . 4 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
32eleq2i 2224 . . 3 (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ 𝑇 ↔ ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))})
41, 3bitri 183 . 2 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))})
5 vex 2715 . . . 4 𝑎 ∈ V
6 vex 2715 . . . 4 𝑏 ∈ V
75, 6opex 4189 . . 3 𝑎, 𝑏⟩ ∈ V
8 vex 2715 . . . 4 𝑐 ∈ V
9 vex 2715 . . . 4 𝑑 ∈ V
108, 9opex 4189 . . 3 𝑐, 𝑑⟩ ∈ V
11 eleq1 2220 . . . . . 6 (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
12 opelxp 4615 . . . . . 6 (⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵) ↔ (𝑎𝐴𝑏𝐵))
1311, 12bitrdi 195 . . . . 5 (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ∈ (𝐴 × 𝐵) ↔ (𝑎𝐴𝑏𝐵)))
1413anbi1d 461 . . . 4 (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ ((𝑎𝐴𝑏𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
155, 6op1std 6093 . . . . . 6 (𝑥 = ⟨𝑎, 𝑏⟩ → (1st𝑥) = 𝑎)
1615breq1d 3975 . . . . 5 (𝑥 = ⟨𝑎, 𝑏⟩ → ((1st𝑥)𝑅(1st𝑦) ↔ 𝑎𝑅(1st𝑦)))
1715eqeq1d 2166 . . . . . 6 (𝑥 = ⟨𝑎, 𝑏⟩ → ((1st𝑥) = (1st𝑦) ↔ 𝑎 = (1st𝑦)))
185, 6op2ndd 6094 . . . . . . 7 (𝑥 = ⟨𝑎, 𝑏⟩ → (2nd𝑥) = 𝑏)
1918breq1d 3975 . . . . . 6 (𝑥 = ⟨𝑎, 𝑏⟩ → ((2nd𝑥)𝑆(2nd𝑦) ↔ 𝑏𝑆(2nd𝑦)))
2017, 19anbi12d 465 . . . . 5 (𝑥 = ⟨𝑎, 𝑏⟩ → (((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)) ↔ (𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦))))
2116, 20orbi12d 783 . . . 4 (𝑥 = ⟨𝑎, 𝑏⟩ → (((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))) ↔ (𝑎𝑅(1st𝑦) ∨ (𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦)))))
2214, 21anbi12d 465 . . 3 (𝑥 = ⟨𝑎, 𝑏⟩ → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)))) ↔ (((𝑎𝐴𝑏𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ (𝑎𝑅(1st𝑦) ∨ (𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦))))))
23 eleq1 2220 . . . . . 6 (𝑦 = ⟨𝑐, 𝑑⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵)))
24 opelxp 4615 . . . . . 6 (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ↔ (𝑐𝐴𝑑𝐵))
2523, 24bitrdi 195 . . . . 5 (𝑦 = ⟨𝑐, 𝑑⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ (𝑐𝐴𝑑𝐵)))
2625anbi2d 460 . . . 4 (𝑦 = ⟨𝑐, 𝑑⟩ → (((𝑎𝐴𝑏𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ ((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵))))
278, 9op1std 6093 . . . . . 6 (𝑦 = ⟨𝑐, 𝑑⟩ → (1st𝑦) = 𝑐)
2827breq2d 3977 . . . . 5 (𝑦 = ⟨𝑐, 𝑑⟩ → (𝑎𝑅(1st𝑦) ↔ 𝑎𝑅𝑐))
2927eqeq2d 2169 . . . . . 6 (𝑦 = ⟨𝑐, 𝑑⟩ → (𝑎 = (1st𝑦) ↔ 𝑎 = 𝑐))
308, 9op2ndd 6094 . . . . . . 7 (𝑦 = ⟨𝑐, 𝑑⟩ → (2nd𝑦) = 𝑑)
3130breq2d 3977 . . . . . 6 (𝑦 = ⟨𝑐, 𝑑⟩ → (𝑏𝑆(2nd𝑦) ↔ 𝑏𝑆𝑑))
3229, 31anbi12d 465 . . . . 5 (𝑦 = ⟨𝑐, 𝑑⟩ → ((𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦)) ↔ (𝑎 = 𝑐𝑏𝑆𝑑)))
3328, 32orbi12d 783 . . . 4 (𝑦 = ⟨𝑐, 𝑑⟩ → ((𝑎𝑅(1st𝑦) ∨ (𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦))) ↔ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
3426, 33anbi12d 465 . . 3 (𝑦 = ⟨𝑐, 𝑑⟩ → ((((𝑎𝐴𝑏𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ (𝑎𝑅(1st𝑦) ∨ (𝑎 = (1st𝑦) ∧ 𝑏𝑆(2nd𝑦)))) ↔ (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑)))))
357, 10, 22, 34opelopab 4231 . 2 (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))} ↔ (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
36 an4 576 . . 3 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) ↔ ((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)))
3736anbi1i 454 . 2 ((((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))) ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
384, 35, 373bitri 205 1 (⟨𝑎, 𝑏𝑇𝑐, 𝑑⟩ ↔ (((𝑎𝐴𝑐𝐴) ∧ (𝑏𝐵𝑑𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐𝑏𝑆𝑑))))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104   ∨ wo 698   = wceq 1335   ∈ wcel 2128  ⟨cop 3563   class class class wbr 3965  {copab 4024   × cxp 4583  ‘cfv 5169  1st c1st 6083  2nd c2nd 6084 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-sbc 2938  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-mpt 4027  df-id 4253  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-iota 5134  df-fun 5171  df-fv 5177  df-1st 6085  df-2nd 6086 This theorem is referenced by:  poxp  6176
 Copyright terms: Public domain W3C validator