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

Metamath Proof Explorer

Theorem ackbij1lem1

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

Ref Expression
Assertion ackbij1lem1 ( ¬ 𝐴 ∈ 𝐵 → ( 𝐵 ∩ suc 𝐴 ) = ( 𝐵 ∩ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-suc ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
2 1 ineq2i ⊢ ( 𝐵 ∩ suc 𝐴 ) = ( 𝐵 ∩ ( 𝐴 ∪ { 𝐴 } ) )
3 indi ⊢ ( 𝐵 ∩ ( 𝐴 ∪ { 𝐴 } ) ) = ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∩ { 𝐴 } ) )
4 2 3 eqtri ⊢ ( 𝐵 ∩ suc 𝐴 ) = ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∩ { 𝐴 } ) )
5 disjsn ⊢ ( ( 𝐵 ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ 𝐵 )
6 5 biimpri ⊢ ( ¬ 𝐴 ∈ 𝐵 → ( 𝐵 ∩ { 𝐴 } ) = ∅ )
7 6 uneq2d ⊢ ( ¬ 𝐴 ∈ 𝐵 → ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∩ { 𝐴 } ) ) = ( ( 𝐵 ∩ 𝐴 ) ∪ ∅ ) )
8 un0 ⊢ ( ( 𝐵 ∩ 𝐴 ) ∪ ∅ ) = ( 𝐵 ∩ 𝐴 )
9 7 8 eqtrdi ⊢ ( ¬ 𝐴 ∈ 𝐵 → ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∩ { 𝐴 } ) ) = ( 𝐵 ∩ 𝐴 ) )
10 4 9 eqtrid ⊢ ( ¬ 𝐴 ∈ 𝐵 → ( 𝐵 ∩ suc 𝐴 ) = ( 𝐵 ∩ 𝐴 ) )