Metamath Proof Explorer

Theorem hfun

Description: The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015)

Ref Expression
Assertion hfun ⊢A∈Hf∧B∈Hf→A∪B∈Hf

Proof

Step Hyp Ref Expression
1 rankung ⊢A∈Hf∧B∈Hf→rank⁡A∪B=rank⁡A∪rank⁡B
2 elhf2g ⊢A∈Hf→A∈Hf↔rank⁡A∈ω
3 2 ibi ⊢A∈Hf→rank⁡A∈ω
4 elhf2g ⊢B∈Hf→B∈Hf↔rank⁡B∈ω
5 4 ibi ⊢B∈Hf→rank⁡B∈ω
6 eleq1a ⊢rank⁡B∈ω→rank⁡A∪rank⁡B=rank⁡B→rank⁡A∪rank⁡B∈ω
7 6 adantl ⊢rank⁡A∈ω∧rank⁡B∈ω→rank⁡A∪rank⁡B=rank⁡B→rank⁡A∪rank⁡B∈ω
8 uncom ⊢rank⁡B∪rank⁡A=rank⁡A∪rank⁡B
9 8 eqeq1i ⊢rank⁡B∪rank⁡A=rank⁡A↔rank⁡A∪rank⁡B=rank⁡A
10 9 biimpi ⊢rank⁡B∪rank⁡A=rank⁡A→rank⁡A∪rank⁡B=rank⁡A
11 10 eleq1d ⊢rank⁡B∪rank⁡A=rank⁡A→rank⁡A∪rank⁡B∈ω↔rank⁡A∈ω
12 11 biimprcd ⊢rank⁡A∈ω→rank⁡B∪rank⁡A=rank⁡A→rank⁡A∪rank⁡B∈ω
13 12 adantr ⊢rank⁡A∈ω∧rank⁡B∈ω→rank⁡B∪rank⁡A=rank⁡A→rank⁡A∪rank⁡B∈ω
14 nnord ⊢rank⁡A∈ω→Ord⁡rank⁡A
15 nnord ⊢rank⁡B∈ω→Ord⁡rank⁡B
16 ordtri2or2 ⊢Ord⁡rank⁡A∧Ord⁡rank⁡B→rank⁡A⊆rank⁡B∨rank⁡B⊆rank⁡A
17 14 15 16 syl2an ⊢rank⁡A∈ω∧rank⁡B∈ω→rank⁡A⊆rank⁡B∨rank⁡B⊆rank⁡A
18 ssequn1 ⊢rank⁡A⊆rank⁡B↔rank⁡A∪rank⁡B=rank⁡B
19 ssequn1 ⊢rank⁡B⊆rank⁡A↔rank⁡B∪rank⁡A=rank⁡A
20 18 19 orbi12i ⊢rank⁡A⊆rank⁡B∨rank⁡B⊆rank⁡A↔rank⁡A∪rank⁡B=rank⁡B∨rank⁡B∪rank⁡A=rank⁡A
21 17 20 sylib ⊢rank⁡A∈ω∧rank⁡B∈ω→rank⁡A∪rank⁡B=rank⁡B∨rank⁡B∪rank⁡A=rank⁡A
22 7 13 21 mpjaod ⊢rank⁡A∈ω∧rank⁡B∈ω→rank⁡A∪rank⁡B∈ω
23 3 5 22 syl2an ⊢A∈Hf∧B∈Hf→rank⁡A∪rank⁡B∈ω
24 1 23 eqeltrd ⊢A∈Hf∧B∈Hf→rank⁡A∪B∈ω
25 unexg ⊢A∈Hf∧B∈Hf→A∪B∈V
26 elhf2g ⊢A∪B∈V→A∪B∈Hf↔rank⁡A∪B∈ω
27 25 26 syl ⊢A∈Hf∧B∈Hf→A∪B∈Hf↔rank⁡A∪B∈ω
28 24 27 mpbird ⊢A∈Hf∧B∈Hf→A∪B∈Hf