Theorem nosepne

Description: The value of two non-equal surreals at the first place they differ is different. (Contributed by Scott Fenton, 24-Nov-2021)

	Ref	Expression
Assertion	nosepne	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		ltsso	⊢ <s Or No
2		sotrine	⊢ ( ( <s Or No ∧ ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴 ) ) )
3	1 2	mpan	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴 ) ) )
4		nosepnelem	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵 ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
5	4	3expia	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ) )
6		nosepnelem	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ∧ 𝐵 <s 𝐴 ) → ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ≠ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) )
7		necom	⊢ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) )
8	7	rabbii	⊢ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } = { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) }
9	8	inteqi	⊢ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) }
10	9	fveq2i	⊢ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } )
11	9	fveq2i	⊢ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) = ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } )
12	10 11	neeq12i	⊢ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ↔ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) )
13		necom	⊢ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ↔ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ≠ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) )
14	12 13	bitri	⊢ ( ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ↔ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) ≠ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ) )
15	6 14	sylibr	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ∧ 𝐵 <s 𝐴 ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )
16	15	3expia	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐵 <s 𝐴 → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ) )
17	16	ancoms	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐵 <s 𝐴 → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ) )
18	5 17	jaod	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴 ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ) )
19	3 18	sylbid	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≠ 𝐵 → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ) )
20	19	3impia	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) ≠ ( 𝐵 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ) )