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