Metamath Proof Explorer


Theorem nodenselem8

Description: Lemma for nodense . Give a condition for surreal less-than when two surreals have the same birthday. (Contributed by Scott Fenton, 19-Jun-2011)

Ref Expression
Assertion nodenselem8 ANoBNobdayA=bdayBA<sBAaOn|AaBa=1𝑜BaOn|AaBa=2𝑜

Proof

Step Hyp Ref Expression
1 nodenselem5 ANoBNobdayA=bdayBA<sBaOn|AaBabdayA
2 1 exp32 ANoBNobdayA=bdayBA<sBaOn|AaBabdayA
3 2 3impia ANoBNobdayA=bdayBA<sBaOn|AaBabdayA
4 sltval2 ANoBNoA<sBAaOn|AaBa1𝑜1𝑜2𝑜2𝑜BaOn|AaBa
5 4 3adant3 ANoBNobdayA=bdayBA<sBAaOn|AaBa1𝑜1𝑜2𝑜2𝑜BaOn|AaBa
6 fvex AaOn|AaBaV
7 fvex BaOn|AaBaV
8 6 7 brtp AaOn|AaBa1𝑜1𝑜2𝑜2𝑜BaOn|AaBaAaOn|AaBa=1𝑜BaOn|AaBa=AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜AaOn|AaBa=BaOn|AaBa=2𝑜
9 eleq2 bdayA=bdayBaOn|AaBabdayAaOn|AaBabdayB
10 9 biimpd bdayA=bdayBaOn|AaBabdayAaOn|AaBabdayB
11 nosgnn0 ¬1𝑜2𝑜
12 nofnbday BNoBFnbdayB
13 fnfvelrn BFnbdayBaOn|AaBabdayBBaOn|AaBaranB
14 eleq1 BaOn|AaBa=BaOn|AaBaranBranB
15 13 14 syl5ibcom BFnbdayBaOn|AaBabdayBBaOn|AaBa=ranB
16 12 15 sylan BNoaOn|AaBabdayBBaOn|AaBa=ranB
17 norn BNoranB1𝑜2𝑜
18 17 sseld BNoranB1𝑜2𝑜
19 18 adantr BNoaOn|AaBabdayBranB1𝑜2𝑜
20 16 19 syld BNoaOn|AaBabdayBBaOn|AaBa=1𝑜2𝑜
21 11 20 mtoi BNoaOn|AaBabdayB¬BaOn|AaBa=
22 21 ex BNoaOn|AaBabdayB¬BaOn|AaBa=
23 22 adantl ANoBNoaOn|AaBabdayB¬BaOn|AaBa=
24 10 23 syl9r ANoBNobdayA=bdayBaOn|AaBabdayA¬BaOn|AaBa=
25 24 3impia ANoBNobdayA=bdayBaOn|AaBabdayA¬BaOn|AaBa=
26 25 imp ANoBNobdayA=bdayBaOn|AaBabdayA¬BaOn|AaBa=
27 26 intnand ANoBNobdayA=bdayBaOn|AaBabdayA¬AaOn|AaBa=1𝑜BaOn|AaBa=
28 nofnbday ANoAFnbdayA
29 fnfvelrn AFnbdayAaOn|AaBabdayAAaOn|AaBaranA
30 eleq1 AaOn|AaBa=AaOn|AaBaranAranA
31 29 30 syl5ibcom AFnbdayAaOn|AaBabdayAAaOn|AaBa=ranA
32 28 31 sylan ANoaOn|AaBabdayAAaOn|AaBa=ranA
33 norn ANoranA1𝑜2𝑜
34 33 sseld ANoranA1𝑜2𝑜
35 34 adantr ANoaOn|AaBabdayAranA1𝑜2𝑜
36 32 35 syld ANoaOn|AaBabdayAAaOn|AaBa=1𝑜2𝑜
37 11 36 mtoi ANoaOn|AaBabdayA¬AaOn|AaBa=
38 37 3ad2antl1 ANoBNobdayA=bdayBaOn|AaBabdayA¬AaOn|AaBa=
39 38 intnanrd ANoBNobdayA=bdayBaOn|AaBabdayA¬AaOn|AaBa=BaOn|AaBa=2𝑜
40 3orel13 ¬AaOn|AaBa=1𝑜BaOn|AaBa=¬AaOn|AaBa=BaOn|AaBa=2𝑜AaOn|AaBa=1𝑜BaOn|AaBa=AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜AaOn|AaBa=BaOn|AaBa=2𝑜AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜
41 27 39 40 syl2anc ANoBNobdayA=bdayBaOn|AaBabdayAAaOn|AaBa=1𝑜BaOn|AaBa=AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜AaOn|AaBa=BaOn|AaBa=2𝑜AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜
42 41 ex ANoBNobdayA=bdayBaOn|AaBabdayAAaOn|AaBa=1𝑜BaOn|AaBa=AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜AaOn|AaBa=BaOn|AaBa=2𝑜AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜
43 42 com23 ANoBNobdayA=bdayBAaOn|AaBa=1𝑜BaOn|AaBa=AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜AaOn|AaBa=BaOn|AaBa=2𝑜aOn|AaBabdayAAaOn|AaBa=1𝑜BaOn|AaBa=2𝑜
44 8 43 biimtrid ANoBNobdayA=bdayBAaOn|AaBa1𝑜1𝑜2𝑜2𝑜BaOn|AaBaaOn|AaBabdayAAaOn|AaBa=1𝑜BaOn|AaBa=2𝑜
45 5 44 sylbid ANoBNobdayA=bdayBA<sBaOn|AaBabdayAAaOn|AaBa=1𝑜BaOn|AaBa=2𝑜
46 3 45 mpdd ANoBNobdayA=bdayBA<sBAaOn|AaBa=1𝑜BaOn|AaBa=2𝑜
47 3mix2 AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜AaOn|AaBa=1𝑜BaOn|AaBa=AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜AaOn|AaBa=BaOn|AaBa=2𝑜
48 47 8 sylibr AaOn|AaBa=1𝑜BaOn|AaBa=2𝑜AaOn|AaBa1𝑜1𝑜2𝑜2𝑜BaOn|AaBa
49 48 5 imbitrrid ANoBNobdayA=bdayBAaOn|AaBa=1𝑜BaOn|AaBa=2𝑜A<sB
50 46 49 impbid ANoBNobdayA=bdayBA<sBAaOn|AaBa=1𝑜BaOn|AaBa=2𝑜