Metamath Proof Explorer


Theorem nodenselem5

Description: Lemma for nodense . If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion nodenselem5 A No B No bday A = bday B A < s B a On | A a B a bday A

Proof

Step Hyp Ref Expression
1 simpll A No B No bday A = bday B A < s B A No
2 simplr A No B No bday A = bday B A < s B B No
3 sltso < s Or No
4 sonr < s Or No A No ¬ A < s A
5 3 4 mpan A No ¬ A < s A
6 breq2 A = B A < s A A < s B
7 6 notbid A = B ¬ A < s A ¬ A < s B
8 5 7 syl5ibcom A No A = B ¬ A < s B
9 8 necon2ad A No A < s B A B
10 9 adantr A No B No A < s B A B
11 10 imp A No B No A < s B A B
12 11 adantrl A No B No bday A = bday B A < s B A B
13 nosepdm A No B No A B a On | A a B a dom A dom B
14 1 2 12 13 syl3anc A No B No bday A = bday B A < s B a On | A a B a dom A dom B
15 simprl A No B No bday A = bday B A < s B bday A = bday B
16 15 uneq2d A No B No bday A = bday B A < s B bday A bday A = bday A bday B
17 unidm bday A bday A = bday A
18 16 17 eqtr3di A No B No bday A = bday B A < s B bday A bday B = bday A
19 bdayval A No bday A = dom A
20 1 19 syl A No B No bday A = bday B A < s B bday A = dom A
21 bdayval B No bday B = dom B
22 2 21 syl A No B No bday A = bday B A < s B bday B = dom B
23 20 22 uneq12d A No B No bday A = bday B A < s B bday A bday B = dom A dom B
24 18 23 20 3eqtr3d A No B No bday A = bday B A < s B dom A dom B = dom A
25 14 24 eleqtrd A No B No bday A = bday B A < s B a On | A a B a dom A
26 25 20 eleqtrrd A No B No bday A = bday B A < s B a On | A a B a bday A