Theorem hfuniOLD

Description: Obsolete version of hfuni as of 17-Sep-2026. (Contributed by Scott Fenton, 16-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hfuniOLD	⊢ ( 𝐴 ∈ 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 )