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