Metamath Proof Explorer

Theorem fin23lem11

Description: Lemma for isfin2-2 . (Contributed by Stefan O'Rear, 31-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Hypotheses fin23lem11.1 
|- ( z = ( A \ x ) -> ( ps <-> ch ) )
fin23lem11.2 
|- ( w = ( A \ v ) -> ( ph <-> th ) )
fin23lem11.3 
|- ( ( x C_ A /\ v C_ A ) -> ( ch <-> th ) )
Assertion fin23lem11 
|- ( B C_ ~P A -> ( E. x e. { c e. ~P A | ( A \ c ) e. B } A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph -> E. z e. B A. v e. B -. ps ) )

Proof

Step Hyp Ref Expression
1 fin23lem11.1 
 |-  ( z = ( A \ x ) -> ( ps <-> ch ) )
2 fin23lem11.2 
 |-  ( w = ( A \ v ) -> ( ph <-> th ) )
3 fin23lem11.3 
 |-  ( ( x C_ A /\ v C_ A ) -> ( ch <-> th ) )
4 difeq2 
 |-  ( c = x -> ( A \ c ) = ( A \ x ) )
5 4 eleq1d 
 |-  ( c = x -> ( ( A \ c ) e. B <-> ( A \ x ) e. B ) )
6 5 elrab 
 |-  ( x e. { c e. ~P A | ( A \ c ) e. B } <-> ( x e. ~P A /\ ( A \ x ) e. B ) )
7 simp2r 
 |-  ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) -> ( A \ x ) e. B )
8 2 notbid 
 |-  ( w = ( A \ v ) -> ( -. ph <-> -. th ) )
9 simpl3 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph )
10 difeq2 
 |-  ( c = ( A \ v ) -> ( A \ c ) = ( A \ ( A \ v ) ) )
11 10 eleq1d 
 |-  ( c = ( A \ v ) -> ( ( A \ c ) e. B <-> ( A \ ( A \ v ) ) e. B ) )
12 difss 
 |-  ( A \ v ) C_ A
13 ssun1 
 |-  A C_ ( A u. x )
14 undif1 
 |-  ( ( A \ x ) u. x ) = ( A u. x )
15 13 14 sseqtrri 
 |-  A C_ ( ( A \ x ) u. x )
16 simpl2r 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> ( A \ x ) e. B )
17 simpl2l 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> x e. ~P A )
18 unexg 
 |-  ( ( ( A \ x ) e. B /\ x e. ~P A ) -> ( ( A \ x ) u. x ) e. _V )
19 16 17 18 syl2anc 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> ( ( A \ x ) u. x ) e. _V )
20 ssexg 
 |-  ( ( A C_ ( ( A \ x ) u. x ) /\ ( ( A \ x ) u. x ) e. _V ) -> A e. _V )
21 15 19 20 sylancr 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> A e. _V )
22 elpw2g 
 |-  ( A e. _V -> ( ( A \ v ) e. ~P A <-> ( A \ v ) C_ A ) )
23 21 22 syl 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> ( ( A \ v ) e. ~P A <-> ( A \ v ) C_ A ) )
24 12 23 mpbiri 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> ( A \ v ) e. ~P A )
25 simpl1 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> B C_ ~P A )
26 simpr 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> v e. B )
27 25 26 sseldd 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> v e. ~P A )
28 27 elpwid 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> v C_ A )
29 dfss4 
 |-  ( v C_ A <-> ( A \ ( A \ v ) ) = v )
30 28 29 sylib 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> ( A \ ( A \ v ) ) = v )
31 30 26 eqeltrd 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> ( A \ ( A \ v ) ) e. B )
32 11 24 31 elrabd 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> ( A \ v ) e. { c e. ~P A | ( A \ c ) e. B } )
33 8 9 32 rspcdva 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> -. th )
34 simplrl 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) ) /\ v e. B ) -> x e. ~P A )
35 34 elpwid 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) ) /\ v e. B ) -> x C_ A )
36 ssel2 
 |-  ( ( B C_ ~P A /\ v e. B ) -> v e. ~P A )
37 36 adantlr 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) ) /\ v e. B ) -> v e. ~P A )
38 37 elpwid 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) ) /\ v e. B ) -> v C_ A )
39 35 38 3 syl2anc 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) ) /\ v e. B ) -> ( ch <-> th ) )
40 39 notbid 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) ) /\ v e. B ) -> ( -. ch <-> -. th ) )
41 40 3adantl3 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> ( -. ch <-> -. th ) )
42 33 41 mpbird 
 |-  ( ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) /\ v e. B ) -> -. ch )
43 42 ralrimiva 
 |-  ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) -> A. v e. B -. ch )
44 1 notbid 
 |-  ( z = ( A \ x ) -> ( -. ps <-> -. ch ) )
45 44 ralbidv 
 |-  ( z = ( A \ x ) -> ( A. v e. B -. ps <-> A. v e. B -. ch ) )
46 45 rspcev 
 |-  ( ( ( A \ x ) e. B /\ A. v e. B -. ch ) -> E. z e. B A. v e. B -. ps )
47 7 43 46 syl2anc 
 |-  ( ( B C_ ~P A /\ ( x e. ~P A /\ ( A \ x ) e. B ) /\ A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph ) -> E. z e. B A. v e. B -. ps )
48 47 3exp 
 |-  ( B C_ ~P A -> ( ( x e. ~P A /\ ( A \ x ) e. B ) -> ( A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph -> E. z e. B A. v e. B -. ps ) ) )
49 6 48 biimtrid 
 |-  ( B C_ ~P A -> ( x e. { c e. ~P A | ( A \ c ) e. B } -> ( A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph -> E. z e. B A. v e. B -. ps ) ) )
50 49 rexlimdv 
 |-  ( B C_ ~P A -> ( E. x e. { c e. ~P A | ( A \ c ) e. B } A. w e. { c e. ~P A | ( A \ c ) e. B } -. ph -> E. z e. B A. v e. B -. ps ) )