Metamath Proof Explorer

Theorem nosep1o

Description: If the value of a surreal at a separator is 1o then the surreal is lesser. (Contributed by Scott Fenton, 7-Dec-2021)

Ref Expression
Assertion nosep1o ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → 𝐴 <s 𝐵 )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o )
2 nosepne ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
3 2 adantr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
4 1 3 eqnetrrd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → 1o ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
5 4 necomd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ 1o )
6 5 neneqd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ¬ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o )
7 simpl2 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → 𝐵 ∈ No )
8 nofv ⊢ ( 𝐵 ∈ No → ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) )
9 7 8 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) )
10 3orel2 ⊢ ( ¬ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o → ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) → ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
11 6 9 10 sylc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) )
12 eqid ⊢ 1o = 1o
13 11 12 jctil ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ( 1o = 1o ∧ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
14 andi ⊢ ( ( 1o = 1o ∧ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) ↔ ( ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
15 13 14 sylib ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ( ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
16 3mix1 ⊢ ( ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) → ( ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( 1o = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
17 3mix2 ⊢ ( ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) → ( ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( 1o = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
18 16 17 jaoi ⊢ ( ( ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) → ( ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( 1o = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
19 15 18 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ( ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( 1o = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
20 1oex ⊢ 1o ∈ V
21 fvex ⊢ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ∈ V
22 20 21 brtp ⊢ ( 1o { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ↔ ( ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ∅ ) ∨ ( 1o = 1o ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ∨ ( 1o = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 2o ) ) )
23 19 22 sylibr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → 1o { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
24 1 23 eqbrtrd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
25 simpl1 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → 𝐴 ∈ No )
26 sltval2 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ) )
27 25 7 26 syl2anc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → ( 𝐴 <s 𝐵 ↔ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ) )
28 24 27 mpbird ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = 1o ) → 𝐴 <s 𝐵 )