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 ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → ( 𝐴 ∪ 𝐵 ) ∈ Hf )

Proof

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