hfuni

Description: The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015)

		Ref	Expression
	Assertion	hfuni	$⊢ A \in Hf \to ⋃ A \in Hf$

Step	Hyp	Ref	Expression
1		rankuni	$⊢ rank (⋃ A) = ⋃ rank (A)$
2		rankon	$⊢ rank (A) \in On$
3		ontr	$⊢ rank (A) \in On \to Tr rank (A)$
4	2 3	ax-mp	$⊢ Tr rank (A)$
5		df-tr	$⊢ Tr rank (A) \leftrightarrow ⋃ rank (A) \subseteq rank (A)$
6	4 5	mpbi	$⊢ ⋃ rank (A) \subseteq rank (A)$
7		elhf2g	$⊢ A \in Hf \to (A \in Hf \leftrightarrow rank (A) \in ω)$
8	7	ibi	$⊢ A \in Hf \to rank (A) \in ω$
9		rankon	$⊢ rank (⋃ A) \in On$
10	1 9	eqeltrri	$⊢ ⋃ rank (A) \in On$
11	10	onordi	$⊢ Ord ⋃ rank (A)$
12		ordom	$⊢ Ord ω$
13		ordtr2	$⊢ (Ord ⋃ rank (A) \land Ord ω) \to ((⋃ rank (A) \subseteq rank (A) \land rank (A) \in ω) \to ⋃ rank (A) \in ω)$
14	11 12 13	mp2an	$⊢ (⋃ rank (A) \subseteq rank (A) \land rank (A) \in ω) \to ⋃ rank (A) \in ω$
15	6 8 14	sylancr	$⊢ A \in Hf \to ⋃ rank (A) \in ω$
16	1 15	eqeltrid	$⊢ A \in Hf \to rank (⋃ A) \in ω$
17		uniexg	$⊢ A \in Hf \to ⋃ A \in V$
18		elhf2g	$⊢ ⋃ A \in V \to (⋃ A \in Hf \leftrightarrow rank (⋃ A) \in ω)$
19	17 18	syl	$⊢ A \in Hf \to (⋃ A \in Hf \leftrightarrow rank (⋃ A) \in ω)$
20	16 19	mpbird	$⊢ A \in Hf \to ⋃ A \in Hf$

Metamath Proof Explorer