Theorem dju1en

Description: Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of Enderton p. 143. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	dju1en	$$⊢\left(A\in V\wedge \neg A\in A\right)\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx \mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		enrefg	$$⊢A\in V\to A\approx A$$
2	1	adantr	$$⊢\left(A\in V\wedge \neg A\in A\right)\to A\approx A$$
3		ensn1g	$$⊢A\in V\to \left\{A\right\}\approx 1_{𝑜}$$
4	3	ensymd	$$⊢A\in V\to 1_{𝑜}\approx \left\{A\right\}$$
5	4	adantr	$$⊢\left(A\in V\wedge \neg A\in A\right)\to 1_{𝑜}\approx \left\{A\right\}$$
6		simpr	$$⊢\left(A\in V\wedge \neg A\in A\right)\to \neg A\in A$$
7		disjsn	$$⊢A\cap \left\{A\right\}=\varnothing \leftrightarrow \neg A\in A$$
8	6 7	sylibr	$$⊢\left(A\in V\wedge \neg A\in A\right)\to A\cap \left\{A\right\}=\varnothing$$
9		djuenun	$$⊢\left(A\approx A\wedge 1_{𝑜}\approx \left\{A\right\}\wedge A\cap \left\{A\right\}=\varnothing \right)\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx \left(A\cup \left\{A\right\}\right)$$
10	2 5 8 9	syl3anc	$$⊢\left(A\in V\wedge \neg A\in A\right)\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx \left(A\cup \left\{A\right\}\right)$$
11		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
12	10 11	breqtrrdi	$$⊢\left(A\in V\wedge \neg A\in A\right)\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx \mathrm{suc}A$$