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		ontr	⊢ ( ( rank ‘ 𝐴 ) ∈ On → Tr ( rank ‘ 𝐴 ) )
4	2 3	ax-mp	⊢ Tr ( rank ‘ 𝐴 )
5		df-tr	⊢ ( Tr ( rank ‘ 𝐴 ) ↔ ∪ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 ) )
6	4 5	mpbi	⊢ ∪ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 )
7		elhf2g	⊢ ( 𝐴 ∈ Hf → ( 𝐴 ∈ Hf ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
8	7	ibi	⊢ ( 𝐴 ∈ Hf → ( rank ‘ 𝐴 ) ∈ ω )
9		rankon	⊢ ( rank ‘ ∪ 𝐴 ) ∈ On
10	1 9	eqeltrri	⊢ ∪ ( rank ‘ 𝐴 ) ∈ On
11	10	onordi	⊢ Ord ∪ ( rank ‘ 𝐴 )
12		ordom	⊢ Ord ω
13		ordtr2	⊢ ( ( Ord ∪ ( rank ‘ 𝐴 ) ∧ Ord ω ) → ( ( ∪ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ ω ) → ∪ ( rank ‘ 𝐴 ) ∈ ω ) )
14	11 12 13	mp2an	⊢ ( ( ∪ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ ω ) → ∪ ( rank ‘ 𝐴 ) ∈ ω )
15	6 8 14	sylancr	⊢ ( 𝐴 ∈ Hf → ∪ ( rank ‘ 𝐴 ) ∈ ω )
16	1 15	eqeltrid	⊢ ( 𝐴 ∈ Hf → ( rank ‘ ∪ 𝐴 ) ∈ ω )
17		uniexg	⊢ ( 𝐴 ∈ Hf → ∪ 𝐴 ∈ V )
18		elhf2g	⊢ ( ∪ 𝐴 ∈ V → ( ∪ 𝐴 ∈ Hf ↔ ( rank ‘ ∪ 𝐴 ) ∈ ω ) )
19	17 18	syl	⊢ ( 𝐴 ∈ Hf → ( ∪ 𝐴 ∈ Hf ↔ ( rank ‘ ∪ 𝐴 ) ∈ ω ) )
20	16 19	mpbird	⊢ ( 𝐴 ∈ Hf → ∪ 𝐴 ∈ Hf )