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 𝐴 ) = ( 𝐵 ∩ 𝐴 ) )