Theorem nodenselem6

Description: The restriction of a surreal to the abstraction from nodenselem4 is still a surreal. (Contributed by Scott Fenton, 16-Jun-2011)

	Ref	Expression
Assertion	nodenselem6	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐴 ∈ No )
2		nodenselem4	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 <s 𝐵 ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On )
3	2	adantrl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On )
4		noreson	⊢ ( ( 𝐴 ∈ No ∧ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ) → ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ No )
5	1 3 4	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ No )