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 e. Hf /\ B e. Hf ) -> ( A u. B ) e. Hf )

Proof

Step Hyp Ref Expression
1 rankung 
 |-  ( ( A e. Hf /\ B e. Hf ) -> ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) ) )
2 elhf2g 
 |-  ( A e. Hf -> ( A e. Hf <-> ( rank ` A ) e. _om ) )
3 2 ibi 
 |-  ( A e. Hf -> ( rank ` A ) e. _om )
4 elhf2g 
 |-  ( B e. Hf -> ( B e. Hf <-> ( rank ` B ) e. _om ) )
5 4 ibi 
 |-  ( B e. Hf -> ( rank ` B ) e. _om )
6 eleq1a 
 |-  ( ( rank ` B ) e. _om -> ( ( ( rank ` A ) u. ( rank ` B ) ) = ( rank ` B ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. _om ) )
7 6 adantl 
 |-  ( ( ( rank ` A ) e. _om /\ ( rank ` B ) e. _om ) -> ( ( ( rank ` A ) u. ( rank ` B ) ) = ( rank ` B ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. _om ) )
8 uncom 
 |-  ( ( rank ` B ) u. ( rank ` A ) ) = ( ( rank ` A ) u. ( rank ` B ) )
9 8 eqeq1i 
 |-  ( ( ( rank ` B ) u. ( rank ` A ) ) = ( rank ` A ) <-> ( ( rank ` A ) u. ( rank ` B ) ) = ( rank ` A ) )
10 9 biimpi 
 |-  ( ( ( rank ` B ) u. ( rank ` A ) ) = ( rank ` A ) -> ( ( rank ` A ) u. ( rank ` B ) ) = ( rank ` A ) )
11 10 eleq1d 
 |-  ( ( ( rank ` B ) u. ( rank ` A ) ) = ( rank ` A ) -> ( ( ( rank ` A ) u. ( rank ` B ) ) e. _om <-> ( rank ` A ) e. _om ) )
12 11 biimprcd 
 |-  ( ( rank ` A ) e. _om -> ( ( ( rank ` B ) u. ( rank ` A ) ) = ( rank ` A ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. _om ) )
13 12 adantr 
 |-  ( ( ( rank ` A ) e. _om /\ ( rank ` B ) e. _om ) -> ( ( ( rank ` B ) u. ( rank ` A ) ) = ( rank ` A ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. _om ) )
14 nnord 
 |-  ( ( rank ` A ) e. _om -> Ord ( rank ` A ) )
15 nnord 
 |-  ( ( rank ` B ) e. _om -> Ord ( rank ` B ) )
16 ordtri2or2 
 |-  ( ( Ord ( rank ` A ) /\ Ord ( rank ` B ) ) -> ( ( rank ` A ) C_ ( rank ` B ) \/ ( rank ` B ) C_ ( rank ` A ) ) )
17 14 15 16 syl2an 
 |-  ( ( ( rank ` A ) e. _om /\ ( rank ` B ) e. _om ) -> ( ( rank ` A ) C_ ( rank ` B ) \/ ( rank ` B ) C_ ( rank ` A ) ) )
18 ssequn1 
 |-  ( ( rank ` A ) C_ ( rank ` B ) <-> ( ( rank ` A ) u. ( rank ` B ) ) = ( rank ` B ) )
19 ssequn1 
 |-  ( ( rank ` B ) C_ ( rank ` A ) <-> ( ( rank ` B ) u. ( rank ` A ) ) = ( rank ` A ) )
20 18 19 orbi12i 
 |-  ( ( ( rank ` A ) C_ ( rank ` B ) \/ ( rank ` B ) C_ ( rank ` A ) ) <-> ( ( ( rank ` A ) u. ( rank ` B ) ) = ( rank ` B ) \/ ( ( rank ` B ) u. ( rank ` A ) ) = ( rank ` A ) ) )
21 17 20 sylib 
 |-  ( ( ( rank ` A ) e. _om /\ ( rank ` B ) e. _om ) -> ( ( ( rank ` A ) u. ( rank ` B ) ) = ( rank ` B ) \/ ( ( rank ` B ) u. ( rank ` A ) ) = ( rank ` A ) ) )
22 7 13 21 mpjaod 
 |-  ( ( ( rank ` A ) e. _om /\ ( rank ` B ) e. _om ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. _om )
23 3 5 22 syl2an 
 |-  ( ( A e. Hf /\ B e. Hf ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. _om )
24 1 23 eqeltrd 
 |-  ( ( A e. Hf /\ B e. Hf ) -> ( rank ` ( A u. B ) ) e. _om )
25 unexg 
 |-  ( ( A e. Hf /\ B e. Hf ) -> ( A u. B ) e. _V )
26 elhf2g 
 |-  ( ( A u. B ) e. _V -> ( ( A u. B ) e. Hf <-> ( rank ` ( A u. B ) ) e. _om ) )
27 25 26 syl 
 |-  ( ( A e. Hf /\ B e. Hf ) -> ( ( A u. B ) e. Hf <-> ( rank ` ( A u. B ) ) e. _om ) )
28 24 27 mpbird 
 |-  ( ( A e. Hf /\ B e. Hf ) -> ( A u. B ) e. Hf )