Metamath Proof Explorer

Theorem nosepssdm

Description: Given two non-equal surreals, their separator is less-than or equal to the domain of one of them. Part of Lemma 2.1.1 of Lipparini p. 3. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nosepssdm ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ⊆ dom 𝐴 )

Proof

Step Hyp Ref Expression
1 nosepne ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
2 1 neneqd ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ¬ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
3 nodmord ⊢ ( 𝐴 ∈ No → Ord dom 𝐴 )
4 3 3ad2ant1 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → Ord dom 𝐴 )
5 ordn2lp ⊢ ( Ord dom 𝐴 → ¬ ( dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∧ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ) )
6 4 5 syl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ¬ ( dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∧ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ) )
7 imnan ⊢ ( ( dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } → ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ) ↔ ¬ ( dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∧ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ) )
8 6 7 sylibr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ( dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } → ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 ) )
9 8 imp ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 )
10 ndmfv ⊢ ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐴 → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ )
11 9 10 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ )
12 nosepeq ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( 𝐴 ‘ dom 𝐴 ) = ( 𝐵 ‘ dom 𝐴 ) )
13 simpl1 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → 𝐴 ∈ No )
14 ordirr ⊢ ( Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴 )
15 ndmfv ⊢ ( ¬ dom 𝐴 ∈ dom 𝐴 → ( 𝐴 ‘ dom 𝐴 ) = ∅ )
16 13 3 14 15 4syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( 𝐴 ‘ dom 𝐴 ) = ∅ )
17 16 eqeq1d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( ( 𝐴 ‘ dom 𝐴 ) = ( 𝐵 ‘ dom 𝐴 ) ↔ ∅ = ( 𝐵 ‘ dom 𝐴 ) ) )
18 eqcom ⊢ ( ∅ = ( 𝐵 ‘ dom 𝐴 ) ↔ ( 𝐵 ‘ dom 𝐴 ) = ∅ )
19 17 18 bitrdi ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( ( 𝐴 ‘ dom 𝐴 ) = ( 𝐵 ‘ dom 𝐴 ) ↔ ( 𝐵 ‘ dom 𝐴 ) = ∅ ) )
20 simpl2 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → 𝐵 ∈ No )
21 nofun ⊢ ( 𝐵 ∈ No → Fun 𝐵 )
22 20 21 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → Fun 𝐵 )
23 nosgnn0 ⊢ ¬ ∅ ∈ { 1o , 2o }
24 norn ⊢ ( 𝐵 ∈ No → ran 𝐵 ⊆ { 1o , 2o } )
25 20 24 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ran 𝐵 ⊆ { 1o , 2o } )
26 25 sseld ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( ∅ ∈ ran 𝐵 → ∅ ∈ { 1o , 2o } ) )
27 23 26 mtoi ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ¬ ∅ ∈ ran 𝐵 )
28 funeldmb ⊢ ( ( Fun 𝐵 ∧ ¬ ∅ ∈ ran 𝐵 ) → ( dom 𝐴 ∈ dom 𝐵 ↔ ( 𝐵 ‘ dom 𝐴 ) ≠ ∅ ) )
29 22 27 28 syl2anc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( dom 𝐴 ∈ dom 𝐵 ↔ ( 𝐵 ‘ dom 𝐴 ) ≠ ∅ ) )
30 29 necon2bbid ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( ( 𝐵 ‘ dom 𝐴 ) = ∅ ↔ ¬ dom 𝐴 ∈ dom 𝐵 ) )
31 nodmord ⊢ ( 𝐵 ∈ No → Ord dom 𝐵 )
32 31 3ad2ant2 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → Ord dom 𝐵 )
33 ordtr1 ⊢ ( Ord dom 𝐵 → ( ( dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∧ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) → dom 𝐴 ∈ dom 𝐵 ) )
34 32 33 syl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ( ( dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∧ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) → dom 𝐴 ∈ dom 𝐵 ) )
35 34 expdimp ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 → dom 𝐴 ∈ dom 𝐵 ) )
36 35 con3d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( ¬ dom 𝐴 ∈ dom 𝐵 → ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) )
37 30 36 sylbid ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( ( 𝐵 ‘ dom 𝐴 ) = ∅ → ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) )
38 19 37 sylbid ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( ( 𝐴 ‘ dom 𝐴 ) = ( 𝐵 ‘ dom 𝐴 ) → ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 ) )
39 12 38 mpd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 )
40 ndmfv ⊢ ( ¬ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ dom 𝐵 → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ )
41 39 40 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ )
42 11 41 eqtr4d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
43 2 42 mtand ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ¬ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } )
44 nosepon ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ On )
45 nodmon ⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On )
46 45 3ad2ant1 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → dom 𝐴 ∈ On )
47 ontri1 ⊢ ( ( ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ On ∧ dom 𝐴 ∈ On ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ⊆ dom 𝐴 ↔ ¬ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
48 44 46 47 syl2anc ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ( ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ⊆ dom 𝐴 ↔ ¬ dom 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
49 43 48 mpbird ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ⊆ dom 𝐴 )