Metamath Proof Explorer

Theorem ficardun2

Description: The cardinality of the union of finite sets is at most the ordinal sum of their cardinalities. (Contributed by Mario Carneiro, 5-Feb-2013) Avoid ax-rep . (Revised by BTernaryTau, 3-Jul-2024)

Ref Expression
Assertion ficardun2 
|- ( ( A e. Fin /\ B e. Fin ) -> ( card ` ( A u. B ) ) C_ ( ( card ` A ) +o ( card ` B ) ) )

Proof

Step Hyp Ref Expression
1 undjudom 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) ~<_ ( A |_| B ) )
2 ficardadju 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) )
3 domentr 
 |-  ( ( ( A u. B ) ~<_ ( A |_| B ) /\ ( A |_| B ) ~~ ( ( card ` A ) +o ( card ` B ) ) ) -> ( A u. B ) ~<_ ( ( card ` A ) +o ( card ` B ) ) )
4 1 2 3 syl2anc 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) ~<_ ( ( card ` A ) +o ( card ` B ) ) )
5 unfi 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
6 finnum 
 |-  ( ( A u. B ) e. Fin -> ( A u. B ) e. dom card )
7 5 6 syl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. dom card )
8 ficardom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )
9 ficardom 
 |-  ( B e. Fin -> ( card ` B ) e. _om )
10 nnacl 
 |-  ( ( ( card ` A ) e. _om /\ ( card ` B ) e. _om ) -> ( ( card ` A ) +o ( card ` B ) ) e. _om )
11 8 9 10 syl2an 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( card ` A ) +o ( card ` B ) ) e. _om )
12 nnon 
 |-  ( ( ( card ` A ) +o ( card ` B ) ) e. _om -> ( ( card ` A ) +o ( card ` B ) ) e. On )
13 onenon 
 |-  ( ( ( card ` A ) +o ( card ` B ) ) e. On -> ( ( card ` A ) +o ( card ` B ) ) e. dom card )
14 11 12 13 3syl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( card ` A ) +o ( card ` B ) ) e. dom card )
15 carddom2 
 |-  ( ( ( A u. B ) e. dom card /\ ( ( card ` A ) +o ( card ` B ) ) e. dom card ) -> ( ( card ` ( A u. B ) ) C_ ( card ` ( ( card ` A ) +o ( card ` B ) ) ) <-> ( A u. B ) ~<_ ( ( card ` A ) +o ( card ` B ) ) ) )
16 7 14 15 syl2anc 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( card ` ( A u. B ) ) C_ ( card ` ( ( card ` A ) +o ( card ` B ) ) ) <-> ( A u. B ) ~<_ ( ( card ` A ) +o ( card ` B ) ) ) )
17 4 16 mpbird 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( card ` ( A u. B ) ) C_ ( card ` ( ( card ` A ) +o ( card ` B ) ) ) )
18 cardnn 
 |-  ( ( ( card ` A ) +o ( card ` B ) ) e. _om -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
19 11 18 syl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( card ` ( ( card ` A ) +o ( card ` B ) ) ) = ( ( card ` A ) +o ( card ` B ) ) )
20 17 19 sseqtrd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( card ` ( A u. B ) ) C_ ( ( card ` A ) +o ( card ` B ) ) )