Theorem hfuni

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

	Ref	Expression
Assertion	hfuni	|- ( A e. Hf -> U. A e. Hf )

Proof

Step	Hyp	Ref	Expression
1		rankuni	|- ( rank ` U. A ) = U. ( rank ` A )
2		rankon	|- ( rank ` A ) e. On
3		ontr	|- ( ( rank ` A ) e. On -> Tr ( rank ` A ) )
4	2 3	ax-mp	|- Tr ( rank ` A )
5		df-tr	|- ( Tr ( rank ` A ) <-> U. ( rank ` A ) C_ ( rank ` A ) )
6	4 5	mpbi	|- U. ( rank ` A ) C_ ( rank ` A )
7		elhf2g	|- ( A e. Hf -> ( A e. Hf <-> ( rank ` A ) e. _om ) )
8	7	ibi	|- ( A e. Hf -> ( rank ` A ) e. _om )
9		rankon	|- ( rank ` U. A ) e. On
10	1 9	eqeltrri	|- U. ( rank ` A ) e. On
11	10	onordi	|- Ord U. ( rank ` A )
12		ordom	|- Ord _om
13		ordtr2	|- ( ( Ord U. ( rank ` A ) /\ Ord _om ) -> ( ( U. ( rank ` A ) C_ ( rank ` A ) /\ ( rank ` A ) e. _om ) -> U. ( rank ` A ) e. _om ) )
14	11 12 13	mp2an	|- ( ( U. ( rank ` A ) C_ ( rank ` A ) /\ ( rank ` A ) e. _om ) -> U. ( rank ` A ) e. _om )
15	6 8 14	sylancr	|- ( A e. Hf -> U. ( rank ` A ) e. _om )
16	1 15	eqeltrid	|- ( A e. Hf -> ( rank ` U. A ) e. _om )
17		uniexg	|- ( A e. Hf -> U. A e. _V )
18		elhf2g	|- ( U. A e. _V -> ( U. A e. Hf <-> ( rank ` U. A ) e. _om ) )
19	17 18	syl	|- ( A e. Hf -> ( U. A e. Hf <-> ( rank ` U. A ) e. _om ) )
20	16 19	mpbird	|- ( A e. Hf -> U. A e. Hf )