Theorem fin23lem7

Description: Lemma for isfin2-2 . The componentwise complement of a nonempty collection of sets is nonempty. (Contributed by Stefan O'Rear, 31-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

	Ref	Expression
Assertion	fin23lem7	|- ( ( A e. V /\ B C_ ~P A /\ B =/= (/) ) -> { x e. ~P A | ( A \ x ) e. B } =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( B =/= (/) <-> E. y y e. B )
2		difss	|- ( A \ y ) C_ A
3		elpw2g	|- ( A e. V -> ( ( A \ y ) e. ~P A <-> ( A \ y ) C_ A ) )
4	3	ad2antrr	|- ( ( ( A e. V /\ B C_ ~P A ) /\ y e. B ) -> ( ( A \ y ) e. ~P A <-> ( A \ y ) C_ A ) )
5	2 4	mpbiri	|- ( ( ( A e. V /\ B C_ ~P A ) /\ y e. B ) -> ( A \ y ) e. ~P A )
6		simpr	|- ( ( A e. V /\ B C_ ~P A ) -> B C_ ~P A )
7	6	sselda	|- ( ( ( A e. V /\ B C_ ~P A ) /\ y e. B ) -> y e. ~P A )
8	7	elpwid	|- ( ( ( A e. V /\ B C_ ~P A ) /\ y e. B ) -> y C_ A )
9		dfss4	|- ( y C_ A <-> ( A \ ( A \ y ) ) = y )
10	8 9	sylib	|- ( ( ( A e. V /\ B C_ ~P A ) /\ y e. B ) -> ( A \ ( A \ y ) ) = y )
11		simpr	|- ( ( ( A e. V /\ B C_ ~P A ) /\ y e. B ) -> y e. B )
12	10 11	eqeltrd	|- ( ( ( A e. V /\ B C_ ~P A ) /\ y e. B ) -> ( A \ ( A \ y ) ) e. B )
13		difeq2	|- ( x = ( A \ y ) -> ( A \ x ) = ( A \ ( A \ y ) ) )
14	13	eleq1d	|- ( x = ( A \ y ) -> ( ( A \ x ) e. B <-> ( A \ ( A \ y ) ) e. B ) )
15	14	rspcev	|- ( ( ( A \ y ) e. ~P A /\ ( A \ ( A \ y ) ) e. B ) -> E. x e. ~P A ( A \ x ) e. B )
16	5 12 15	syl2anc	|- ( ( ( A e. V /\ B C_ ~P A ) /\ y e. B ) -> E. x e. ~P A ( A \ x ) e. B )
17	16	ex	|- ( ( A e. V /\ B C_ ~P A ) -> ( y e. B -> E. x e. ~P A ( A \ x ) e. B ) )
18	17	exlimdv	|- ( ( A e. V /\ B C_ ~P A ) -> ( E. y y e. B -> E. x e. ~P A ( A \ x ) e. B ) )
19	1 18	syl5bi	|- ( ( A e. V /\ B C_ ~P A ) -> ( B =/= (/) -> E. x e. ~P A ( A \ x ) e. B ) )
20	19	3impia	|- ( ( A e. V /\ B C_ ~P A /\ B =/= (/) ) -> E. x e. ~P A ( A \ x ) e. B )
21		rabn0	|- ( { x e. ~P A | ( A \ x ) e. B } =/= (/) <-> E. x e. ~P A ( A \ x ) e. B )
22	20 21	sylibr	|- ( ( A e. V /\ B C_ ~P A /\ B =/= (/) ) -> { x e. ~P A | ( A \ x ) e. B } =/= (/) )