Theorem ackbij1lem2

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

	Ref	Expression
Assertion	ackbij1lem2	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 ∩ suc 𝐴 ) = ( { 𝐴 } ∪ ( 𝐵 ∩ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
2	1	ineq2i	⊢ ( 𝐵 ∩ suc 𝐴 ) = ( 𝐵 ∩ ( 𝐴 ∪ { 𝐴 } ) )
3		indi	⊢ ( 𝐵 ∩ ( 𝐴 ∪ { 𝐴 } ) ) = ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∩ { 𝐴 } ) )
4		uncom	⊢ ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∩ { 𝐴 } ) ) = ( ( 𝐵 ∩ { 𝐴 } ) ∪ ( 𝐵 ∩ 𝐴 ) )
5	2 3 4	3eqtri	⊢ ( 𝐵 ∩ suc 𝐴 ) = ( ( 𝐵 ∩ { 𝐴 } ) ∪ ( 𝐵 ∩ 𝐴 ) )
6		snssi	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 )
7		sseqin2	⊢ ( { 𝐴 } ⊆ 𝐵 ↔ ( 𝐵 ∩ { 𝐴 } ) = { 𝐴 } )
8	6 7	sylib	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 ∩ { 𝐴 } ) = { 𝐴 } )
9	8	uneq1d	⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐵 ∩ { 𝐴 } ) ∪ ( 𝐵 ∩ 𝐴 ) ) = ( { 𝐴 } ∪ ( 𝐵 ∩ 𝐴 ) ) )
10	5 9	syl5eq	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 ∩ suc 𝐴 ) = ( { 𝐴 } ∪ ( 𝐵 ∩ 𝐴 ) ) )