smoiun

Description: The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011)

		Ref	Expression
	Assertion	smoiun	$⊢ (Smo B \land A \in dom B) \to ⋃_{x \in A} B (x) \subseteq B (A)$

Step	Hyp	Ref	Expression
1		eliun	$⊢ y \in ⋃_{x \in A} B (x) \leftrightarrow \exists x \in A y \in B (x)$
2		smofvon	$⊢ (Smo B \land A \in dom B) \to B (A) \in On$
3		smoel	$⊢ (Smo B \land A \in dom B \land x \in A) \to B (x) \in B (A)$
4	3	3expia	$⊢ (Smo B \land A \in dom B) \to (x \in A \to B (x) \in B (A))$
5		ontr1	$⊢ B (A) \in On \to ((y \in B (x) \land B (x) \in B (A)) \to y \in B (A))$
6	5	expcomd	$⊢ B (A) \in On \to (B (x) \in B (A) \to (y \in B (x) \to y \in B (A)))$
7	2 4 6	sylsyld	$⊢ (Smo B \land A \in dom B) \to (x \in A \to (y \in B (x) \to y \in B (A)))$
8	7	rexlimdv	$⊢ (Smo B \land A \in dom B) \to (\exists x \in A y \in B (x) \to y \in B (A))$
9	1 8	biimtrid	$⊢ (Smo B \land A \in dom B) \to (y \in ⋃_{x \in A} B (x) \to y \in B (A))$
10	9	ssrdv	$⊢ (Smo B \land A \in dom B) \to ⋃_{x \in A} B (x) \subseteq B (A)$

Metamath Proof Explorer