Metamath Proof Explorer

Theorem sltval

Description: The value of the surreal less-than relation. (Contributed by Scott Fenton, 14-Jun-2011)

Ref Expression
Assertion sltval ⊢A∈No∧B∈No→A<sB↔∃x∈On∀y∈xA⁡y=B⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x

Proof

Step Hyp Ref Expression
1 eleq1 ⊢f=A→f∈No↔A∈No
2 1 anbi1d ⊢f=A→f∈No∧g∈No↔A∈No∧g∈No
3 fveq1 ⊢f=A→f⁡y=A⁡y
4 3 eqeq1d ⊢f=A→f⁡y=g⁡y↔A⁡y=g⁡y
5 4 ralbidv ⊢f=A→∀y∈xf⁡y=g⁡y↔∀y∈xA⁡y=g⁡y
6 fveq1 ⊢f=A→f⁡x=A⁡x
7 6 breq1d ⊢f=A→f⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x↔A⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x
8 5 7 anbi12d ⊢f=A→∀y∈xf⁡y=g⁡y∧f⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x↔∀y∈xA⁡y=g⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x
9 8 rexbidv ⊢f=A→∃x∈On∀y∈xf⁡y=g⁡y∧f⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x↔∃x∈On∀y∈xA⁡y=g⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x
10 2 9 anbi12d ⊢f=A→f∈No∧g∈No∧∃x∈On∀y∈xf⁡y=g⁡y∧f⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x↔A∈No∧g∈No∧∃x∈On∀y∈xA⁡y=g⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x
11 eleq1 ⊢g=B→g∈No↔B∈No
12 11 anbi2d ⊢g=B→A∈No∧g∈No↔A∈No∧B∈No
13 fveq1 ⊢g=B→g⁡y=B⁡y
14 13 eqeq2d ⊢g=B→A⁡y=g⁡y↔A⁡y=B⁡y
15 14 ralbidv ⊢g=B→∀y∈xA⁡y=g⁡y↔∀y∈xA⁡y=B⁡y
16 fveq1 ⊢g=B→g⁡x=B⁡x
17 16 breq2d ⊢g=B→A⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x↔A⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x
18 15 17 anbi12d ⊢g=B→∀y∈xA⁡y=g⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x↔∀y∈xA⁡y=B⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x
19 18 rexbidv ⊢g=B→∃x∈On∀y∈xA⁡y=g⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x↔∃x∈On∀y∈xA⁡y=B⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x
20 12 19 anbi12d ⊢g=B→A∈No∧g∈No∧∃x∈On∀y∈xA⁡y=g⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x↔A∈No∧B∈No∧∃x∈On∀y∈xA⁡y=B⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x
21 df-slt ⊢<s=fg|f∈No∧g∈No∧∃x∈On∀y∈xf⁡y=g⁡y∧f⁡x1𝑜∅1𝑜2𝑜∅2𝑜g⁡x
22 10 20 21 brabg ⊢A∈No∧B∈No→A<sB↔A∈No∧B∈No∧∃x∈On∀y∈xA⁡y=B⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x
23 22 bianabs ⊢A∈No∧B∈No→A<sB↔∃x∈On∀y∈xA⁡y=B⁡y∧A⁡x1𝑜∅1𝑜2𝑜∅2𝑜B⁡x