Metamath Proof Explorer

Theorem fineqvlem

Description: Lemma for fineqv . (Contributed by Mario Carneiro, 20-Jan-2013) (Proof shortened by Stefan O'Rear, 3-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fineqvlem 
|- ( ( A e. V /\ -. A e. Fin ) -> _om ~<_ ~P ~P A )

Proof

Step Hyp Ref Expression
1 pwexg 
 |-  ( A e. V -> ~P A e. _V )
2 1 adantr 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ~P A e. _V )
3 2 pwexd 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ~P ~P A e. _V )
4 ssrab2 
 |-  { d e. ~P A | d ~~ b } C_ ~P A
5 elpw2g 
 |-  ( ~P A e. _V -> ( { d e. ~P A | d ~~ b } e. ~P ~P A <-> { d e. ~P A | d ~~ b } C_ ~P A ) )
6 2 5 syl 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( { d e. ~P A | d ~~ b } e. ~P ~P A <-> { d e. ~P A | d ~~ b } C_ ~P A ) )
7 4 6 mpbiri 
 |-  ( ( A e. V /\ -. A e. Fin ) -> { d e. ~P A | d ~~ b } e. ~P ~P A )
8 7 a1d 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( b e. _om -> { d e. ~P A | d ~~ b } e. ~P ~P A ) )
9 isinf 
 |-  ( -. A e. Fin -> A. b e. _om E. e ( e C_ A /\ e ~~ b ) )
10 9 r19.21bi 
 |-  ( ( -. A e. Fin /\ b e. _om ) -> E. e ( e C_ A /\ e ~~ b ) )
11 10 ad2ant2lr 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ ( b e. _om /\ c e. _om ) ) -> E. e ( e C_ A /\ e ~~ b ) )
12 velpw 
 |-  ( e e. ~P A <-> e C_ A )
13 12 biimpri 
 |-  ( e C_ A -> e e. ~P A )
14 13 anim1i 
 |-  ( ( e C_ A /\ e ~~ b ) -> ( e e. ~P A /\ e ~~ b ) )
15 breq1 
 |-  ( d = e -> ( d ~~ b <-> e ~~ b ) )
16 15 elrab 
 |-  ( e e. { d e. ~P A | d ~~ b } <-> ( e e. ~P A /\ e ~~ b ) )
17 14 16 sylibr 
 |-  ( ( e C_ A /\ e ~~ b ) -> e e. { d e. ~P A | d ~~ b } )
18 17 eximi 
 |-  ( E. e ( e C_ A /\ e ~~ b ) -> E. e e e. { d e. ~P A | d ~~ b } )
19 11 18 syl 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ ( b e. _om /\ c e. _om ) ) -> E. e e e. { d e. ~P A | d ~~ b } )
20 eleq2 
 |-  ( { d e. ~P A | d ~~ b } = { d e. ~P A | d ~~ c } -> ( e e. { d e. ~P A | d ~~ b } <-> e e. { d e. ~P A | d ~~ c } ) )
21 20 biimpcd 
 |-  ( e e. { d e. ~P A | d ~~ b } -> ( { d e. ~P A | d ~~ b } = { d e. ~P A | d ~~ c } -> e e. { d e. ~P A | d ~~ c } ) )
22 21 adantl 
 |-  ( ( ( ( A e. V /\ -. A e. Fin ) /\ ( b e. _om /\ c e. _om ) ) /\ e e. { d e. ~P A | d ~~ b } ) -> ( { d e. ~P A | d ~~ b } = { d e. ~P A | d ~~ c } -> e e. { d e. ~P A | d ~~ c } ) )
23 16 simprbi 
 |-  ( e e. { d e. ~P A | d ~~ b } -> e ~~ b )
24 breq1 
 |-  ( d = e -> ( d ~~ c <-> e ~~ c ) )
25 24 elrab 
 |-  ( e e. { d e. ~P A | d ~~ c } <-> ( e e. ~P A /\ e ~~ c ) )
26 25 simprbi 
 |-  ( e e. { d e. ~P A | d ~~ c } -> e ~~ c )
27 ensym 
 |-  ( e ~~ b -> b ~~ e )
28 entr 
 |-  ( ( b ~~ e /\ e ~~ c ) -> b ~~ c )
29 27 28 sylan 
 |-  ( ( e ~~ b /\ e ~~ c ) -> b ~~ c )
30 23 26 29 syl2an 
 |-  ( ( e e. { d e. ~P A | d ~~ b } /\ e e. { d e. ~P A | d ~~ c } ) -> b ~~ c )
31 30 ex 
 |-  ( e e. { d e. ~P A | d ~~ b } -> ( e e. { d e. ~P A | d ~~ c } -> b ~~ c ) )
32 31 adantl 
 |-  ( ( ( ( A e. V /\ -. A e. Fin ) /\ ( b e. _om /\ c e. _om ) ) /\ e e. { d e. ~P A | d ~~ b } ) -> ( e e. { d e. ~P A | d ~~ c } -> b ~~ c ) )
33 nneneq 
 |-  ( ( b e. _om /\ c e. _om ) -> ( b ~~ c <-> b = c ) )
34 33 biimpd 
 |-  ( ( b e. _om /\ c e. _om ) -> ( b ~~ c -> b = c ) )
35 34 ad2antlr 
 |-  ( ( ( ( A e. V /\ -. A e. Fin ) /\ ( b e. _om /\ c e. _om ) ) /\ e e. { d e. ~P A | d ~~ b } ) -> ( b ~~ c -> b = c ) )
36 22 32 35 3syld 
 |-  ( ( ( ( A e. V /\ -. A e. Fin ) /\ ( b e. _om /\ c e. _om ) ) /\ e e. { d e. ~P A | d ~~ b } ) -> ( { d e. ~P A | d ~~ b } = { d e. ~P A | d ~~ c } -> b = c ) )
37 19 36 exlimddv 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ ( b e. _om /\ c e. _om ) ) -> ( { d e. ~P A | d ~~ b } = { d e. ~P A | d ~~ c } -> b = c ) )
38 breq2 
 |-  ( b = c -> ( d ~~ b <-> d ~~ c ) )
39 38 rabbidv 
 |-  ( b = c -> { d e. ~P A | d ~~ b } = { d e. ~P A | d ~~ c } )
40 37 39 impbid1 
 |-  ( ( ( A e. V /\ -. A e. Fin ) /\ ( b e. _om /\ c e. _om ) ) -> ( { d e. ~P A | d ~~ b } = { d e. ~P A | d ~~ c } <-> b = c ) )
41 40 ex 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( ( b e. _om /\ c e. _om ) -> ( { d e. ~P A | d ~~ b } = { d e. ~P A | d ~~ c } <-> b = c ) ) )
42 8 41 dom2d 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( ~P ~P A e. _V -> _om ~<_ ~P ~P A ) )
43 3 42 mpd 
 |-  ( ( A e. V /\ -. A e. Fin ) -> _om ~<_ ~P ~P A )