Theorem hfuni

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

	Ref	Expression
Assertion	hfuni	⊢ ( 𝐴 ∈ Hf → ∪ 𝐴 ∈ Hf )

Proof

Step	Hyp	Ref	Expression
1		rankuni	⊢ ( rank ‘ ∪ 𝐴 ) = ∪ ( rank ‘ 𝐴 )
2		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
3	2	ontrci	⊢ Tr ( rank ‘ 𝐴 )
4		df-tr	⊢ ( Tr ( rank ‘ 𝐴 ) ↔ ∪ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 ) )
5	3 4	mpbi	⊢ ∪ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 )
6		elhf2g	⊢ ( 𝐴 ∈ Hf → ( 𝐴 ∈ Hf ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
7	6	ibi	⊢ ( 𝐴 ∈ Hf → ( rank ‘ 𝐴 ) ∈ ω )
8		rankon	⊢ ( rank ‘ ∪ 𝐴 ) ∈ On
9	1 8	eqeltrri	⊢ ∪ ( rank ‘ 𝐴 ) ∈ On
10	9	onordi	⊢ Ord ∪ ( rank ‘ 𝐴 )
11		ordom	⊢ Ord ω
12		ordtr2	⊢ ( ( Ord ∪ ( rank ‘ 𝐴 ) ∧ Ord ω ) → ( ( ∪ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ ω ) → ∪ ( rank ‘ 𝐴 ) ∈ ω ) )
13	10 11 12	mp2an	⊢ ( ( ∪ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ ω ) → ∪ ( rank ‘ 𝐴 ) ∈ ω )
14	5 7 13	sylancr	⊢ ( 𝐴 ∈ Hf → ∪ ( rank ‘ 𝐴 ) ∈ ω )
15	1 14	eqeltrid	⊢ ( 𝐴 ∈ Hf → ( rank ‘ ∪ 𝐴 ) ∈ ω )
16		uniexg	⊢ ( 𝐴 ∈ Hf → ∪ 𝐴 ∈ V )
17		elhf2g	⊢ ( ∪ 𝐴 ∈ V → ( ∪ 𝐴 ∈ Hf ↔ ( rank ‘ ∪ 𝐴 ) ∈ ω ) )
18	16 17	syl	⊢ ( 𝐴 ∈ Hf → ( ∪ 𝐴 ∈ Hf ↔ ( rank ‘ ∪ 𝐴 ) ∈ ω ) )
19	15 18	mpbird	⊢ ( 𝐴 ∈ Hf → ∪ 𝐴 ∈ Hf )