This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 ∩ suc 𝐴 ) = ( { 𝐴 } ∪ ( 𝐵 ∩ 𝐴 ) ) )