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 unidm ⊢ bday ⁡ A ∪ bday ⁡ A = bday ⁡ A
16 simprl ⊢ A ∈ No ∧ B ∈ No ∧ bday ⁡ A = bday ⁡ B ∧ A < s B → bday ⁡ A = bday ⁡ B
17 16 uneq2d ⊢ A ∈ No ∧ B ∈ No ∧ bday ⁡ A = bday ⁡ B ∧ A < s B → bday ⁡ A ∪ bday ⁡ A = bday ⁡ A ∪ bday ⁡ B
18 15 17 syl5reqr ⊢ 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