Metamath Proof Explorer

Theorem nosep2o

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

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

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ No )
2 simp1 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ No )
3 simp3 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
4 3 necomd ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ≠ 𝐴 )
5 nosepne ⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ∧ 𝐵 ≠ 𝐴 ) → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ≠ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) )
6 1 2 4 5 syl3anc ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ≠ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) )
7 6 adantr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ≠ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) )
8 simpr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o )
9 7 8 neeqtrd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ≠ 2o )
10 9 neneqd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ¬ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o )
11 simpl2 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → 𝐵 ∈ No )
12 nofv ⊢ ( 𝐵 ∈ No → ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) )
13 11 12 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) )
14 3orel3 ⊢ ( ¬ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o → ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ) ) )
15 10 13 14 sylc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ) )
16 15 orcomd ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ) )
17 16 8 jca ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) )
18 andir ⊢ ( ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∨ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ↔ ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ) )
19 17 18 sylib ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ) )
20 3mix2 ⊢ ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ) )
21 3mix3 ⊢ ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ) )
22 20 21 jaoi ⊢ ( ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ) → ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ) )
23 19 22 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ) )
24 fvex ⊢ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ∈ V
25 fvex ⊢ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ∈ V
26 24 25 brtp ⊢ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ↔ ( ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 1o ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ∨ ( ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = ∅ ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) ) )
27 23 26 sylibr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) )
28 simpl1 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → 𝐴 ∈ No )
29 sltval2 ⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐵 <s 𝐴 ↔ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ) )
30 11 28 29 syl2anc ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → ( 𝐵 <s 𝐴 ↔ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ) )
31 27 30 mpbird ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) = 2o ) → 𝐵 <s 𝐴 )