Theorem infdju1

Description: An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	infdju1	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx A$$

Proof

Step	Hyp	Ref	Expression
1		difun2	$$⊢\left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\right)\setminus \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)=\left(\left\{\varnothing \right\}\times A\right)\setminus \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)$$
2		df-dju	$$⊢\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)$$
3		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
4	3	xpeq2i	$$⊢\left\{1_{𝑜}\right\}\times 1_{𝑜}=\left\{1_{𝑜}\right\}\times \left\{\varnothing \right\}$$
5		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
6		0ex	$$⊢\varnothing \in \mathrm{V}$$
7	5 6	xpsn	$$⊢\left\{1_{𝑜}\right\}\times \left\{\varnothing \right\}=\left\{⟨1_{𝑜},\varnothing ⟩\right\}$$
8	4 7	eqtr2i	$$⊢\left\{⟨1_{𝑜},\varnothing ⟩\right\}=\left\{1_{𝑜}\right\}\times 1_{𝑜}$$
9	2 8	difeq12i	$$⊢\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\setminus \left\{⟨1_{𝑜},\varnothing ⟩\right\}=\left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\right)\setminus \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)$$
10		xp01disjl	$$⊢\left(\left\{\varnothing \right\}\times A\right)\cap \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)=\varnothing$$
11		disj3	$$⊢\left(\left\{\varnothing \right\}\times A\right)\cap \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)=\varnothing \leftrightarrow \left\{\varnothing \right\}\times A=\left(\left\{\varnothing \right\}\times A\right)\setminus \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)$$
12	10 11	mpbi	$$⊢\left\{\varnothing \right\}\times A=\left(\left\{\varnothing \right\}\times A\right)\setminus \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)$$
13	1 9 12	3eqtr4i	$$⊢\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\setminus \left\{⟨1_{𝑜},\varnothing ⟩\right\}=\left\{\varnothing \right\}\times A$$
14		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
15	14	brrelex2i	$$⊢\mathrm{\omega }\preccurlyeq A\to A\in \mathrm{V}$$
16		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
17		djudoml	$$⊢\left(A\in \mathrm{V}\wedge 1_{𝑜}\in \mathrm{On}\right)\to A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
18	15 16 17	sylancl	$$⊢\mathrm{\omega }\preccurlyeq A\to A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
19		domtr	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\right)\to \mathrm{\omega }\preccurlyeq \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
20	18 19	mpdan	$$⊢\mathrm{\omega }\preccurlyeq A\to \mathrm{\omega }\preccurlyeq \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
21		infdifsn	$$⊢\mathrm{\omega }\preccurlyeq \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\to \left(\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\setminus \left\{⟨1_{𝑜},\varnothing ⟩\right\}\right)\approx \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
22	20 21	syl	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\setminus \left\{⟨1_{𝑜},\varnothing ⟩\right\}\right)\approx \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
23	13 22	eqbrtrrid	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(\left\{\varnothing \right\}\times A\right)\approx \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
24	23	ensymd	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx \left(\left\{\varnothing \right\}\times A\right)$$
25		xpsnen2g	$$⊢\left(\varnothing \in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(\left\{\varnothing \right\}\times A\right)\approx A$$
26	6 15 25	sylancr	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(\left\{\varnothing \right\}\times A\right)\approx A$$
27		entr	$$⊢\left(\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx \left(\left\{\varnothing \right\}\times A\right)\wedge \left(\left\{\varnothing \right\}\times A\right)\approx A\right)\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx A$$
28	24 26 27	syl2anc	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx A$$