Theorem ackbij1lem1

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

	Ref	Expression
Assertion	ackbij1lem1	|- ( -. A e. B -> ( B i^i suc A ) = ( 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	2 3	eqtri	|- ( B i^i suc A ) = ( ( B i^i A ) u. ( B i^i { A } ) )
5		disjsn	|- ( ( B i^i { A } ) = (/) <-> -. A e. B )
6	5	biimpri	|- ( -. A e. B -> ( B i^i { A } ) = (/) )
7	6	uneq2d	|- ( -. A e. B -> ( ( B i^i A ) u. ( B i^i { A } ) ) = ( ( B i^i A ) u. (/) ) )
8		un0	|- ( ( B i^i A ) u. (/) ) = ( B i^i A )
9	7 8	eqtrdi	|- ( -. A e. B -> ( ( B i^i A ) u. ( B i^i { A } ) ) = ( B i^i A ) )
10	4 9	syl5eq	|- ( -. A e. B -> ( B i^i suc A ) = ( B i^i A ) )