Theorem harword

Description: Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015)

	Ref	Expression
Assertion	harword	$$⊢X\preccurlyeq Y\to \mathrm{har}\left(X\right)\subseteq \mathrm{har}\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		domtr	$$⊢\left(y\preccurlyeq X\wedge X\preccurlyeq Y\right)\to y\preccurlyeq Y$$
2	1	expcom	$$⊢X\preccurlyeq Y\to \left(y\preccurlyeq X\to y\preccurlyeq Y\right)$$
3	2	adantr	$$⊢\left(X\preccurlyeq Y\wedge y\in \mathrm{On}\right)\to \left(y\preccurlyeq X\to y\preccurlyeq Y\right)$$
4	3	ss2rabdv	$$⊢X\preccurlyeq Y\to \left\{y\in \mathrm{On}|y\preccurlyeq X\right\}\subseteq \left\{y\in \mathrm{On}|y\preccurlyeq Y\right\}$$
5		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
6	5	brrelex1i	$$⊢X\preccurlyeq Y\to X\in \mathrm{V}$$
7		harval	$$⊢X\in \mathrm{V}\to \mathrm{har}\left(X\right)=\left\{y\in \mathrm{On}|y\preccurlyeq X\right\}$$
8	6 7	syl	$$⊢X\preccurlyeq Y\to \mathrm{har}\left(X\right)=\left\{y\in \mathrm{On}|y\preccurlyeq X\right\}$$
9	5	brrelex2i	$$⊢X\preccurlyeq Y\to Y\in \mathrm{V}$$
10		harval	$$⊢Y\in \mathrm{V}\to \mathrm{har}\left(Y\right)=\left\{y\in \mathrm{On}|y\preccurlyeq Y\right\}$$
11	9 10	syl	$$⊢X\preccurlyeq Y\to \mathrm{har}\left(Y\right)=\left\{y\in \mathrm{On}|y\preccurlyeq Y\right\}$$
12	4 8 11	3sstr4d	$$⊢X\preccurlyeq Y\to \mathrm{har}\left(X\right)\subseteq \mathrm{har}\left(Y\right)$$