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	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge \left(\mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\wedge A{<}_{s}B\right)\right)\to {A\upharpoonright }_{\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}}\in \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		simpll	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge \left(\mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\wedge A{<}_{s}B\right)\right)\to A\in \mathrm{No}$$
2		nodenselem4	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge A{<}_{s}B\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}$$
3	2	adantrl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge \left(\mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\wedge A{<}_{s}B\right)\right)\to \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}$$
4		noreson	$$⊢\left(A\in \mathrm{No}\wedge \bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}\in \mathrm{On}\right)\to {A\upharpoonright }_{\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}}\in \mathrm{No}$$
5	1 3 4	syl2anc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge \left(\mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\wedge A{<}_{s}B\right)\right)\to {A\upharpoonright }_{\bigcap \left\{a\in \mathrm{On}|A\left(a\right)\ne B\left(a\right)\right\}}\in \mathrm{No}$$