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<sB→⋂a∈On|A⁡a≠B⁡a∈bday⁡A

Proof

Step Hyp Ref Expression
1 simpll ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→A∈No
2 simplr ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→B∈No
3 sltso ⊢<sOrNo
4 sonr ⊢<sOrNo∧A∈No→¬A<sA
5 3 4 mpan ⊢A∈No→¬A<sA
6 breq2 ⊢A=B→A<sA↔A<sB
7 6 notbid ⊢A=B→¬A<sA↔¬A<sB
8 5 7 syl5ibcom ⊢A∈No→A=B→¬A<sB
9 8 necon2ad ⊢A∈No→A<sB→A≠B
10 9 adantr ⊢A∈No∧B∈No→A<sB→A≠B
11 10 imp ⊢A∈No∧B∈No∧A<sB→A≠B
12 11 adantrl ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→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<sB→⋂a∈On|A⁡a≠B⁡a∈dom⁡A∪dom⁡B
15 simprl ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→bday⁡A=bday⁡B
16 15 uneq2d ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→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<sB→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<sB→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<sB→bday⁡B=dom⁡B
23 20 22 uneq12d ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→bday⁡A∪bday⁡B=dom⁡A∪dom⁡B
24 18 23 20 3eqtr3d ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→dom⁡A∪dom⁡B=dom⁡A
25 14 24 eleqtrd ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→⋂a∈On|A⁡a≠B⁡a∈dom⁡A
26 25 20 eleqtrrd ⊢A∈No∧B∈No∧bday⁡A=bday⁡B∧A<sB→⋂a∈On|A⁡a≠B⁡a∈bday⁡A