Metamath Proof Explorer

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 ∈ Hf → ⋃ A ∈ Hf

Proof

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