Metamath Proof Explorer

Theorem isf34lem4

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis compss.a 
|- F = ( x e. ~P A |-> ( A \ x ) )
Assertion isf34lem4 
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` U. X ) = |^| ( F " X ) )

Proof

Step Hyp Ref Expression
1 compss.a 
 |-  F = ( x e. ~P A |-> ( A \ x ) )
2 sspwuni 
 |-  ( X C_ ~P A <-> U. X C_ A )
3 1 isf34lem1 
 |-  ( ( A e. V /\ U. X C_ A ) -> ( F ` U. X ) = ( A \ U. X ) )
4 2 3 sylan2b 
 |-  ( ( A e. V /\ X C_ ~P A ) -> ( F ` U. X ) = ( A \ U. X ) )
5 4 adantrr 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` U. X ) = ( A \ U. X ) )
6 simplrr 
 |-  ( ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) /\ ( a e. ~P A /\ ( A \ a ) e. X ) ) -> -. b e. U. X )
7 simprl 
 |-  ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) -> b e. A )
8 7 ad2antrr 
 |-  ( ( ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) /\ ( a e. ~P A /\ ( A \ a ) e. X ) ) /\ -. b e. a ) -> b e. A )
9 simpr 
 |-  ( ( ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) /\ ( a e. ~P A /\ ( A \ a ) e. X ) ) /\ -. b e. a ) -> -. b e. a )
10 8 9 eldifd 
 |-  ( ( ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) /\ ( a e. ~P A /\ ( A \ a ) e. X ) ) /\ -. b e. a ) -> b e. ( A \ a ) )
11 simplrr 
 |-  ( ( ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) /\ ( a e. ~P A /\ ( A \ a ) e. X ) ) /\ -. b e. a ) -> ( A \ a ) e. X )
12 elunii 
 |-  ( ( b e. ( A \ a ) /\ ( A \ a ) e. X ) -> b e. U. X )
13 10 11 12 syl2anc 
 |-  ( ( ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) /\ ( a e. ~P A /\ ( A \ a ) e. X ) ) /\ -. b e. a ) -> b e. U. X )
14 13 ex 
 |-  ( ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) /\ ( a e. ~P A /\ ( A \ a ) e. X ) ) -> ( -. b e. a -> b e. U. X ) )
15 6 14 mt3d 
 |-  ( ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) /\ ( a e. ~P A /\ ( A \ a ) e. X ) ) -> b e. a )
16 15 expr 
 |-  ( ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) /\ a e. ~P A ) -> ( ( A \ a ) e. X -> b e. a ) )
17 16 ralrimiva 
 |-  ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. A /\ -. b e. U. X ) ) -> A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) )
18 17 ex 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( ( b e. A /\ -. b e. U. X ) -> A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) ) )
19 n0 
 |-  ( X =/= (/) <-> E. c c e. X )
20 simpr 
 |-  ( ( A e. V /\ X C_ ~P A ) -> X C_ ~P A )
21 20 sselda 
 |-  ( ( ( A e. V /\ X C_ ~P A ) /\ c e. X ) -> c e. ~P A )
22 21 elpwid 
 |-  ( ( ( A e. V /\ X C_ ~P A ) /\ c e. X ) -> c C_ A )
23 dfss4 
 |-  ( c C_ A <-> ( A \ ( A \ c ) ) = c )
24 22 23 sylib 
 |-  ( ( ( A e. V /\ X C_ ~P A ) /\ c e. X ) -> ( A \ ( A \ c ) ) = c )
25 simpr 
 |-  ( ( ( A e. V /\ X C_ ~P A ) /\ c e. X ) -> c e. X )
26 24 25 eqeltrd 
 |-  ( ( ( A e. V /\ X C_ ~P A ) /\ c e. X ) -> ( A \ ( A \ c ) ) e. X )
27 difss 
 |-  ( A \ c ) C_ A
28 elpw2g 
 |-  ( A e. V -> ( ( A \ c ) e. ~P A <-> ( A \ c ) C_ A ) )
29 27 28 mpbiri 
 |-  ( A e. V -> ( A \ c ) e. ~P A )
30 29 ad2antrr 
 |-  ( ( ( A e. V /\ X C_ ~P A ) /\ c e. X ) -> ( A \ c ) e. ~P A )
31 difeq2 
 |-  ( a = ( A \ c ) -> ( A \ a ) = ( A \ ( A \ c ) ) )
32 31 eleq1d 
 |-  ( a = ( A \ c ) -> ( ( A \ a ) e. X <-> ( A \ ( A \ c ) ) e. X ) )
33 eleq2 
 |-  ( a = ( A \ c ) -> ( b e. a <-> b e. ( A \ c ) ) )
34 32 33 imbi12d 
 |-  ( a = ( A \ c ) -> ( ( ( A \ a ) e. X -> b e. a ) <-> ( ( A \ ( A \ c ) ) e. X -> b e. ( A \ c ) ) ) )
35 34 rspcv 
 |-  ( ( A \ c ) e. ~P A -> ( A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) -> ( ( A \ ( A \ c ) ) e. X -> b e. ( A \ c ) ) ) )
36 30 35 syl 
 |-  ( ( ( A e. V /\ X C_ ~P A ) /\ c e. X ) -> ( A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) -> ( ( A \ ( A \ c ) ) e. X -> b e. ( A \ c ) ) ) )
37 26 36 mpid 
 |-  ( ( ( A e. V /\ X C_ ~P A ) /\ c e. X ) -> ( A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) -> b e. ( A \ c ) ) )
38 eldifi 
 |-  ( b e. ( A \ c ) -> b e. A )
39 37 38 syl6 
 |-  ( ( ( A e. V /\ X C_ ~P A ) /\ c e. X ) -> ( A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) -> b e. A ) )
40 39 ex 
 |-  ( ( A e. V /\ X C_ ~P A ) -> ( c e. X -> ( A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) -> b e. A ) ) )
41 40 exlimdv 
 |-  ( ( A e. V /\ X C_ ~P A ) -> ( E. c c e. X -> ( A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) -> b e. A ) ) )
42 19 41 syl5bi 
 |-  ( ( A e. V /\ X C_ ~P A ) -> ( X =/= (/) -> ( A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) -> b e. A ) ) )
43 42 impr 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) -> b e. A ) )
44 eluni 
 |-  ( b e. U. X <-> E. c ( b e. c /\ c e. X ) )
45 29 ad2antrr 
 |-  ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. c /\ c e. X ) ) -> ( A \ c ) e. ~P A )
46 26 adantlrr 
 |-  ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ c e. X ) -> ( A \ ( A \ c ) ) e. X )
47 46 adantrl 
 |-  ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. c /\ c e. X ) ) -> ( A \ ( A \ c ) ) e. X )
48 elndif 
 |-  ( b e. c -> -. b e. ( A \ c ) )
49 48 ad2antrl 
 |-  ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. c /\ c e. X ) ) -> -. b e. ( A \ c ) )
50 47 49 jcnd 
 |-  ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. c /\ c e. X ) ) -> -. ( ( A \ ( A \ c ) ) e. X -> b e. ( A \ c ) ) )
51 34 notbid 
 |-  ( a = ( A \ c ) -> ( -. ( ( A \ a ) e. X -> b e. a ) <-> -. ( ( A \ ( A \ c ) ) e. X -> b e. ( A \ c ) ) ) )
52 51 rspcev 
 |-  ( ( ( A \ c ) e. ~P A /\ -. ( ( A \ ( A \ c ) ) e. X -> b e. ( A \ c ) ) ) -> E. a e. ~P A -. ( ( A \ a ) e. X -> b e. a ) )
53 45 50 52 syl2anc 
 |-  ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. c /\ c e. X ) ) -> E. a e. ~P A -. ( ( A \ a ) e. X -> b e. a ) )
54 rexnal 
 |-  ( E. a e. ~P A -. ( ( A \ a ) e. X -> b e. a ) <-> -. A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) )
55 53 54 sylib 
 |-  ( ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) /\ ( b e. c /\ c e. X ) ) -> -. A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) )
56 55 ex 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( ( b e. c /\ c e. X ) -> -. A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) ) )
57 56 exlimdv 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( E. c ( b e. c /\ c e. X ) -> -. A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) ) )
58 44 57 syl5bi 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( b e. U. X -> -. A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) ) )
59 58 con2d 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) -> -. b e. U. X ) )
60 43 59 jcad 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) -> ( b e. A /\ -. b e. U. X ) ) )
61 18 60 impbid 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( ( b e. A /\ -. b e. U. X ) <-> A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) ) )
62 eldif 
 |-  ( b e. ( A \ U. X ) <-> ( b e. A /\ -. b e. U. X ) )
63 vex 
 |-  b e. _V
64 63 elintrab 
 |-  ( b e. |^| { a e. ~P A | ( A \ a ) e. X } <-> A. a e. ~P A ( ( A \ a ) e. X -> b e. a ) )
65 61 62 64 3bitr4g 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( b e. ( A \ U. X ) <-> b e. |^| { a e. ~P A | ( A \ a ) e. X } ) )
66 65 eqrdv 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( A \ U. X ) = |^| { a e. ~P A | ( A \ a ) e. X } )
67 5 66 eqtrd 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` U. X ) = |^| { a e. ~P A | ( A \ a ) e. X } )
68 1 compss 
 |-  ( F " X ) = { a e. ~P A | ( A \ a ) e. X }
69 68 inteqi 
 |-  |^| ( F " X ) = |^| { a e. ~P A | ( A \ a ) e. X }
70 67 69 eqtr4di 
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` U. X ) = |^| ( F " X ) )