Metamath Proof Explorer


Theorem nosepeq

Description: The values of two surreals at a point less than their separators are equal. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nosepeq ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ 𝑋 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( 𝐴𝑋 ) = ( 𝐵𝑋 ) )

Proof

Step Hyp Ref Expression
1 nosepon ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) → { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ On )
2 onelon ( ( { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ∈ On ∧ 𝑋 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → 𝑋 ∈ On )
3 1 2 sylan ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ 𝑋 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → 𝑋 ∈ On )
4 simpr ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ 𝑋 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → 𝑋 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } )
5 fveq2 ( 𝑥 = 𝑋 → ( 𝐴𝑥 ) = ( 𝐴𝑋 ) )
6 fveq2 ( 𝑥 = 𝑋 → ( 𝐵𝑥 ) = ( 𝐵𝑋 ) )
7 5 6 neeq12d ( 𝑥 = 𝑋 → ( ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) ↔ ( 𝐴𝑋 ) ≠ ( 𝐵𝑋 ) ) )
8 7 onnminsb ( 𝑋 ∈ On → ( 𝑋 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } → ¬ ( 𝐴𝑋 ) ≠ ( 𝐵𝑋 ) ) )
9 3 4 8 sylc ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ 𝑋 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ¬ ( 𝐴𝑋 ) ≠ ( 𝐵𝑋 ) )
10 df-ne ( ( 𝐴𝑋 ) ≠ ( 𝐵𝑋 ) ↔ ¬ ( 𝐴𝑋 ) = ( 𝐵𝑋 ) )
11 10 con2bii ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ↔ ¬ ( 𝐴𝑋 ) ≠ ( 𝐵𝑋 ) )
12 9 11 sylibr ( ( ( 𝐴 No 𝐵 No 𝐴𝐵 ) ∧ 𝑋 { 𝑥 ∈ On ∣ ( 𝐴𝑥 ) ≠ ( 𝐵𝑥 ) } ) → ( 𝐴𝑋 ) = ( 𝐵𝑋 ) )