Theorem ackbij1lem2

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

	Ref	Expression
Assertion	ackbij1lem2	|- ( A e. B -> ( B i^i suc A ) = ( { A } u. ( B i^i A ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-suc	|- suc A = ( A u. { A } )
2	1	ineq2i	|- ( B i^i suc A ) = ( B i^i ( A u. { A } ) )
3		indi	|- ( B i^i ( A u. { A } ) ) = ( ( B i^i A ) u. ( B i^i { A } ) )
4		uncom	|- ( ( B i^i A ) u. ( B i^i { A } ) ) = ( ( B i^i { A } ) u. ( B i^i A ) )
5	2 3 4	3eqtri	|- ( B i^i suc A ) = ( ( B i^i { A } ) u. ( B i^i A ) )
6		snssi	|- ( A e. B -> { A } C_ B )
7		sseqin2	|- ( { A } C_ B <-> ( B i^i { A } ) = { A } )
8	6 7	sylib	|- ( A e. B -> ( B i^i { A } ) = { A } )
9	8	uneq1d	|- ( A e. B -> ( ( B i^i { A } ) u. ( B i^i A ) ) = ( { A } u. ( B i^i A ) ) )
10	5 9	eqtrid	|- ( A e. B -> ( B i^i suc A ) = ( { A } u. ( B i^i A ) ) )