Theorem ackbij1lem1

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

	Ref	Expression
Assertion	ackbij1lem1	$$⊢\neg A\in B\to B\cap \mathrm{suc}A=B\cap A$$

Proof

Step	Hyp	Ref	Expression
1		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
2	1	ineq2i	$$⊢B\cap \mathrm{suc}A=B\cap \left(A\cup \left\{A\right\}\right)$$
3		indi	$$⊢B\cap \left(A\cup \left\{A\right\}\right)=\left(B\cap A\right)\cup \left(B\cap \left\{A\right\}\right)$$
4	2 3	eqtri	$$⊢B\cap \mathrm{suc}A=\left(B\cap A\right)\cup \left(B\cap \left\{A\right\}\right)$$
5		disjsn	$$⊢B\cap \left\{A\right\}=\varnothing \leftrightarrow \neg A\in B$$
6	5	biimpri	$$⊢\neg A\in B\to B\cap \left\{A\right\}=\varnothing$$
7	6	uneq2d	$$⊢\neg A\in B\to \left(B\cap A\right)\cup \left(B\cap \left\{A\right\}\right)=\left(B\cap A\right)\cup \varnothing$$
8		un0	$$⊢\left(B\cap A\right)\cup \varnothing =B\cap A$$
9	7 8	eqtrdi	$$⊢\neg A\in B\to \left(B\cap A\right)\cup \left(B\cap \left\{A\right\}\right)=B\cap A$$
10	4 9	syl5eq	$$⊢\neg A\in B\to B\cap \mathrm{suc}A=B\cap A$$