Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sltval Structured version   Visualization version   GIF version

Theorem sltval 33405
 Description: The value of the surreal less than relationship. (Contributed by Scott Fenton, 14-Jun-2011.)
Assertion
Ref Expression
sltval ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem sltval
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2840 . . . . 5 (𝑓 = 𝐴 → (𝑓 No 𝐴 No ))
21anbi1d 633 . . . 4 (𝑓 = 𝐴 → ((𝑓 No 𝑔 No ) ↔ (𝐴 No 𝑔 No )))
3 fveq1 6655 . . . . . . . 8 (𝑓 = 𝐴 → (𝑓𝑦) = (𝐴𝑦))
43eqeq1d 2761 . . . . . . 7 (𝑓 = 𝐴 → ((𝑓𝑦) = (𝑔𝑦) ↔ (𝐴𝑦) = (𝑔𝑦)))
54ralbidv 3127 . . . . . 6 (𝑓 = 𝐴 → (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝐴𝑦) = (𝑔𝑦)))
6 fveq1 6655 . . . . . . 7 (𝑓 = 𝐴 → (𝑓𝑥) = (𝐴𝑥))
76breq1d 5040 . . . . . 6 (𝑓 = 𝐴 → ((𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥) ↔ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))
85, 7anbi12d 634 . . . . 5 (𝑓 = 𝐴 → ((∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)) ↔ (∀𝑦𝑥 (𝐴𝑦) = (𝑔𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥))))
98rexbidv 3222 . . . 4 (𝑓 = 𝐴 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝑔𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥))))
102, 9anbi12d 634 . . 3 (𝑓 = 𝐴 → (((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥))) ↔ ((𝐴 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝑔𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))))
11 eleq1 2840 . . . . 5 (𝑔 = 𝐵 → (𝑔 No 𝐵 No ))
1211anbi2d 632 . . . 4 (𝑔 = 𝐵 → ((𝐴 No 𝑔 No ) ↔ (𝐴 No 𝐵 No )))
13 fveq1 6655 . . . . . . . 8 (𝑔 = 𝐵 → (𝑔𝑦) = (𝐵𝑦))
1413eqeq2d 2770 . . . . . . 7 (𝑔 = 𝐵 → ((𝐴𝑦) = (𝑔𝑦) ↔ (𝐴𝑦) = (𝐵𝑦)))
1514ralbidv 3127 . . . . . 6 (𝑔 = 𝐵 → (∀𝑦𝑥 (𝐴𝑦) = (𝑔𝑦) ↔ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)))
16 fveq1 6655 . . . . . . 7 (𝑔 = 𝐵 → (𝑔𝑥) = (𝐵𝑥))
1716breq2d 5042 . . . . . 6 (𝑔 = 𝐵 → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥) ↔ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
1815, 17anbi12d 634 . . . . 5 (𝑔 = 𝐵 → ((∀𝑦𝑥 (𝐴𝑦) = (𝑔𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)) ↔ (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
1918rexbidv 3222 . . . 4 (𝑔 = 𝐵 → (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝑔𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
2012, 19anbi12d 634 . . 3 (𝑔 = 𝐵 → (((𝐴 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝑔𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥))) ↔ ((𝐴 No 𝐵 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))))
21 df-slt 33402 . . 3 <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))}
2210, 20, 21brabg 5394 . 2 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ((𝐴 No 𝐵 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))))
2322bianabs 546 1 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∀wral 3071  ∃wrex 3072  ∅c0 4226  {ctp 4524  ⟨cop 4526   class class class wbr 5030  Oncon0 6167  ‘cfv 6333  1oc1o 8103  2oc2o 8104   No csur 33398
 Copyright terms: Public domain W3C validator