harword

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

		Ref	Expression
	Assertion	harword	$⊢ X ≼ Y \to har (X) \subseteq har (Y)$

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

Metamath Proof Explorer