# Metamath Proof Explorer

## 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}↔{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 syl5eq ${⊢}{A}\in {B}\to {B}\cap \mathrm{suc}{A}=\left\{{A}\right\}\cup \left({B}\cap {A}\right)$