Theorem ficardun2OLD

Description: Obsolete version of ficardun2 as of 3-Jul-2024. (Contributed by Mario Carneiro, 5-Feb-2013) (Proof modification is discouraged.) (New usage is discouraged.)

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