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

Metamath Proof Explorer

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 biimtrid 
 |-  ( ( 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 } =/= (/) )