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 ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ ( bday ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐴 ∈ No )
2 simplr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐵 ∈ No )
3 sltso ⊢ <s Or No
4 sonr ⊢ ( ( <s Or No ∧ 𝐴 ∈ No ) → ¬ 𝐴 <s 𝐴 )
5 3 4 mpan ⊢ ( 𝐴 ∈ No → ¬ 𝐴 <s 𝐴 )
6 breq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 <s 𝐴 ↔ 𝐴 <s 𝐵 ) )
7 6 notbid ⊢ ( 𝐴 = 𝐵 → ( ¬ 𝐴 <s 𝐴 ↔ ¬ 𝐴 <s 𝐵 ) )
8 5 7 syl5ibcom ⊢ ( 𝐴 ∈ No → ( 𝐴 = 𝐵 → ¬ 𝐴 <s 𝐵 ) )
9 8 necon2ad ⊢ ( 𝐴 ∈ No → ( 𝐴 <s 𝐵 → 𝐴 ≠ 𝐵 ) )
10 9 adantr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 → 𝐴 ≠ 𝐵 ) )
11 10 imp ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 <s 𝐵 ) → 𝐴 ≠ 𝐵 )
12 11 adantrl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐴 ≠ 𝐵 )
13 nosepdm ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) )
14 1 2 12 13 syl3anc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) )
15 simprl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) )
16 15 uneq2d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐴 ) ) = ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
17 unidm ⊢ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐴 ) ) = ( bday ‘ 𝐴 )
18 16 17 eqtr3di ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) = ( bday ‘ 𝐴 ) )
19 bdayval ⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) = dom 𝐴 )
20 1 19 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday ‘ 𝐴 ) = dom 𝐴 )
21 bdayval ⊢ ( 𝐵 ∈ No → ( bday ‘ 𝐵 ) = dom 𝐵 )
22 2 21 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday ‘ 𝐵 ) = dom 𝐵 )
23 20 22 uneq12d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) = ( dom 𝐴 ∪ dom 𝐵 ) )
24 18 23 20 3eqtr3d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( dom 𝐴 ∪ dom 𝐵 ) = dom 𝐴 )
25 14 24 eleqtrd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ dom 𝐴 )
26 25 20 eleqtrrd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ ( bday ‘ 𝐴 ) )