Theorem ackbij1lem2

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

	Ref	Expression
Assertion	ackbij1lem2	$$⊢A\in B\to B\cap \mathrm{suc}A=\left\{A\right\}\cup \left(B\cap A\right)$$

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		uncom	$$⊢\left(B\cap A\right)\cup \left(B\cap \left\{A\right\}\right)=\left(B\cap \left\{A\right\}\right)\cup \left(B\cap A\right)$$
5	2 3 4	3eqtri	$$⊢B\cap \mathrm{suc}A=\left(B\cap \left\{A\right\}\right)\cup \left(B\cap A\right)$$
6		snssi	$$⊢A\in B\to \left\{A\right\}\subseteq B$$
7		sseqin2	$$⊢\left\{A\right\}\subseteq B\leftrightarrow B\cap \left\{A\right\}=\left\{A\right\}$$
8	6 7	sylib	$$⊢A\in B\to B\cap \left\{A\right\}=\left\{A\right\}$$
9	8	uneq1d	$$⊢A\in B\to \left(B\cap \left\{A\right\}\right)\cup \left(B\cap A\right)=\left\{A\right\}\cup \left(B\cap A\right)$$
10	5 9	eqtrid	$$⊢A\in B\to B\cap \mathrm{suc}A=\left\{A\right\}\cup \left(B\cap A\right)$$