[STATEMENT]
lemma card_of_Un_ordLeq_infinite[simp]:
assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
shows "|A Un B| \<le>o |C|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |A \<union> B| \<le>o |C|
[PROOF STEP]
using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq
ordLeq_transitive
[PROOF STATE]
proof (prove)
using this:
infinite C
|A| \<le>o |C|
|B| \<le>o |C|
\<lbrakk>infinite ?C; |?A| \<le>o |?C|; |?B| \<le>o |?C|\<rbrakk> \<Longrightarrow> |?A <+> ?B| \<le>o |?C|
|?A \<union> ?B| \<le>o |?A <+> ?B|
\<lbrakk>?r \<le>o ?r'; ?r' \<le>o ?r''\<rbrakk> \<Longrightarrow> ?r \<le>o ?r''

goal (1 subgoal):
 1. |A \<union> B| \<le>o |C|
[PROOF STEP]
by metis