Theorem ficardun

Description: The cardinality of the union of disjoint, finite sets is the ordinal sum of their cardinalities. (Contributed by Paul Chapman, 5-Jun-2009) (Proof shortened by Mario Carneiro, 28-Apr-2015) Avoid ax-rep . (Revised by BTernaryTau, 3-Jul-2024)

	Ref	Expression
Assertion	ficardun	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\wedge A\cap B=\varnothing \right)\to \mathrm{card}\left(A\cup B\right)=\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ficardadju	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\approx \left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)$$
2	1	3adant3	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\wedge A\cap B=\varnothing \right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\approx \left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)$$
3	2	ensymd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\wedge A\cap B=\varnothing \right)\to \left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)\approx \left(A\mathrm{\bigsqcup ︀}B\right)$$
4		endjudisj	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\wedge A\cap B=\varnothing \right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\approx \left(A\cup B\right)$$
5		entr	$$⊢\left(\left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)\approx \left(A\mathrm{\bigsqcup ︀}B\right)\wedge \left(A\mathrm{\bigsqcup ︀}B\right)\approx \left(A\cup B\right)\right)\to \left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)\approx \left(A\cup B\right)$$
6	3 4 5	syl2anc	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\wedge A\cap B=\varnothing \right)\to \left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)\approx \left(A\cup B\right)$$
7		carden2b	$$⊢\left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)\approx \left(A\cup B\right)\to \mathrm{card}\left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)=\mathrm{card}\left(A\cup B\right)$$
8	6 7	syl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\wedge A\cap B=\varnothing \right)\to \mathrm{card}\left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)=\mathrm{card}\left(A\cup B\right)$$
9		ficardom	$$⊢A\in \mathrm{Fin}\to \mathrm{card}\left(A\right)\in \mathrm{\omega }$$
10		ficardom	$$⊢B\in \mathrm{Fin}\to \mathrm{card}\left(B\right)\in \mathrm{\omega }$$
11		nnacl	$$⊢\left(\mathrm{card}\left(A\right)\in \mathrm{\omega }\wedge \mathrm{card}\left(B\right)\in \mathrm{\omega }\right)\to \mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\in \mathrm{\omega }$$
12		cardnn	$$⊢\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\in \mathrm{\omega }\to \mathrm{card}\left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)=\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)$$
13	11 12	syl	$$⊢\left(\mathrm{card}\left(A\right)\in \mathrm{\omega }\wedge \mathrm{card}\left(B\right)\in \mathrm{\omega }\right)\to \mathrm{card}\left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)=\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)$$
14	9 10 13	syl2an	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \mathrm{card}\left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)=\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)$$
15	14	3adant3	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\wedge A\cap B=\varnothing \right)\to \mathrm{card}\left(\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)\right)=\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)$$
16	8 15	eqtr3d	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\wedge A\cap B=\varnothing \right)\to \mathrm{card}\left(A\cup B\right)=\mathrm{card}\left(A\right){+}_{𝑜}\mathrm{card}\left(B\right)$$