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 13 3 syl ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → Ord dom 𝐴 )
15 ordirr ( Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴 )
16 ndmfv ( ¬ dom 𝐴 ∈ dom 𝐴 → ( 𝐴 ‘ dom 𝐴 ) = ∅ )
17 14 15 16 3syl ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( 𝐴 ‘ dom 𝐴 ) = ∅ )
18 17 eqeq1d ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( ( 𝐴 ‘ dom 𝐴 ) = ( 𝐵 ‘ dom 𝐴 ) ↔ ∅ = ( 𝐵 ‘ dom 𝐴 ) ) )
19 eqcom ( ∅ = ( 𝐵 ‘ dom 𝐴 ) ↔ ( 𝐵 ‘ dom 𝐴 ) = ∅ )
20 18 19 bitrdi ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( ( 𝐴 ‘ dom 𝐴 ) = ( 𝐵 ‘ dom 𝐴 ) ↔ ( 𝐵 ‘ dom 𝐴 ) = ∅ ) )
21 simpl2 ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → 𝐵 No )
22 nofun ( 𝐵 No → Fun 𝐵 )
23 21 22 syl ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → Fun 𝐵 )
24 nosgnn0 ¬ ∅ ∈ { 1o , 2o }
25 norn ( 𝐵 No → ran 𝐵 ⊆ { 1o , 2o } )
26 21 25 syl ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ran 𝐵 ⊆ { 1o , 2o } )
27 26 sseld ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( ∅ ∈ ran 𝐵 → ∅ ∈ { 1o , 2o } ) )
28 24 27 mtoi ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ¬ ∅ ∈ ran 𝐵 )
29 funeldmb ( ( Fun 𝐵 ∧ ¬ ∅ ∈ ran 𝐵 ) → ( dom 𝐴 ∈ dom 𝐵 ↔ ( 𝐵 ‘ dom 𝐴 ) ≠ ∅ ) )
30 23 28 29 syl2anc ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( dom 𝐴 ∈ dom 𝐵 ↔ ( 𝐵 ‘ dom 𝐴 ) ≠ ∅ ) )
31 30 necon2bbid ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( ( 𝐵 ‘ dom 𝐴 ) = ∅ ↔ ¬ dom 𝐴 ∈ dom 𝐵 ) )
32 nodmord ( 𝐵 No → Ord dom 𝐵 )
33 32 3ad2ant2 ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) → Ord dom 𝐵 )
34 ordtr1 ( Ord dom 𝐵 → ( ( dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∧ { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ dom 𝐵 ) → dom 𝐴 ∈ dom 𝐵 ) )
35 33 34 syl ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) → ( ( dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∧ { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ dom 𝐵 ) → dom 𝐴 ∈ dom 𝐵 ) )
36 35 expdimp ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ dom 𝐵 → dom 𝐴 ∈ dom 𝐵 ) )
37 36 con3d ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( ¬ dom 𝐴 ∈ dom 𝐵 → ¬ { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ dom 𝐵 ) )
38 31 37 sylbid ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( ( 𝐵 ‘ dom 𝐴 ) = ∅ → ¬ { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ dom 𝐵 ) )
39 20 38 sylbid ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( ( 𝐴 ‘ dom 𝐴 ) = ( 𝐵 ‘ dom 𝐴 ) → ¬ { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ dom 𝐵 ) )
40 12 39 mpd ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ¬ { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ dom 𝐵 )
41 ndmfv ( ¬ { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ dom 𝐵 → ( 𝐵 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) = ∅ )
42 40 41 syl ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( 𝐵 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) = ∅ )
43 11 42 eqtr4d ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) = ( 𝐵 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) )
44 2 43 mtand ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) → ¬ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } )
45 nosepon ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) → { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ On )
46 nodmon ( 𝐴 No → dom 𝐴 ∈ On )
47 46 3ad2ant1 ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) → dom 𝐴 ∈ On )
48 ontri1 ( ( { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ On ∧ dom 𝐴 ∈ On ) → ( { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ⊆ dom 𝐴 ↔ ¬ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) )
49 45 47 48 syl2anc ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) → ( { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ⊆ dom 𝐴 ↔ ¬ dom 𝐴 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) )
50 44 49 mpbird ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) → { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ⊆ dom 𝐴 )