Metamath Proof Explorer

Theorem elrfi

Description: Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion elrfi 
|- ( ( B e. V /\ C C_ ~P B ) -> ( A e. ( fi ` ( { B } u. C ) ) <-> E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. ( fi ` ( { B } u. C ) ) -> A e. _V )
2 1 a1i 
 |-  ( ( B e. V /\ C C_ ~P B ) -> ( A e. ( fi ` ( { B } u. C ) ) -> A e. _V ) )
3 inex1g 
 |-  ( B e. V -> ( B i^i |^| v ) e. _V )
4 eleq1 
 |-  ( A = ( B i^i |^| v ) -> ( A e. _V <-> ( B i^i |^| v ) e. _V ) )
5 3 4 syl5ibrcom 
 |-  ( B e. V -> ( A = ( B i^i |^| v ) -> A e. _V ) )
6 5 rexlimdvw 
 |-  ( B e. V -> ( E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) -> A e. _V ) )
7 6 adantr 
 |-  ( ( B e. V /\ C C_ ~P B ) -> ( E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) -> A e. _V ) )
8 simpr 
 |-  ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) -> A e. _V )
9 snex 
 |-  { B } e. _V
10 pwexg 
 |-  ( B e. V -> ~P B e. _V )
11 10 ad2antrr 
 |-  ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) -> ~P B e. _V )
12 simplr 
 |-  ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) -> C C_ ~P B )
13 11 12 ssexd 
 |-  ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) -> C e. _V )
14 unexg 
 |-  ( ( { B } e. _V /\ C e. _V ) -> ( { B } u. C ) e. _V )
15 9 13 14 sylancr 
 |-  ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) -> ( { B } u. C ) e. _V )
16 elfi 
 |-  ( ( A e. _V /\ ( { B } u. C ) e. _V ) -> ( A e. ( fi ` ( { B } u. C ) ) <-> E. w e. ( ~P ( { B } u. C ) i^i Fin ) A = |^| w ) )
17 8 15 16 syl2anc 
 |-  ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) -> ( A e. ( fi ` ( { B } u. C ) ) <-> E. w e. ( ~P ( { B } u. C ) i^i Fin ) A = |^| w ) )
18 inss1 
 |-  ( ~P ( { B } u. C ) i^i Fin ) C_ ~P ( { B } u. C )
19 uncom 
 |-  ( { B } u. C ) = ( C u. { B } )
20 19 pweqi 
 |-  ~P ( { B } u. C ) = ~P ( C u. { B } )
21 18 20 sseqtri 
 |-  ( ~P ( { B } u. C ) i^i Fin ) C_ ~P ( C u. { B } )
22 21 sseli 
 |-  ( w e. ( ~P ( { B } u. C ) i^i Fin ) -> w e. ~P ( C u. { B } ) )
23 9 elpwun 
 |-  ( w e. ~P ( C u. { B } ) <-> ( w \ { B } ) e. ~P C )
24 22 23 sylib 
 |-  ( w e. ( ~P ( { B } u. C ) i^i Fin ) -> ( w \ { B } ) e. ~P C )
25 24 ad2antrl 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> ( w \ { B } ) e. ~P C )
26 inss2 
 |-  ( ~P ( { B } u. C ) i^i Fin ) C_ Fin
27 26 sseli 
 |-  ( w e. ( ~P ( { B } u. C ) i^i Fin ) -> w e. Fin )
28 diffi 
 |-  ( w e. Fin -> ( w \ { B } ) e. Fin )
29 27 28 syl 
 |-  ( w e. ( ~P ( { B } u. C ) i^i Fin ) -> ( w \ { B } ) e. Fin )
30 29 ad2antrl 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> ( w \ { B } ) e. Fin )
31 25 30 elind 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> ( w \ { B } ) e. ( ~P C i^i Fin ) )
32 incom 
 |-  ( B i^i A ) = ( A i^i B )
33 simprr 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> A = |^| w )
34 simplr 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> A e. _V )
35 33 34 eqeltrrd 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> |^| w e. _V )
36 intex 
 |-  ( w =/= (/) <-> |^| w e. _V )
37 35 36 sylibr 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> w =/= (/) )
38 intssuni 
 |-  ( w =/= (/) -> |^| w C_ U. w )
39 37 38 syl 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> |^| w C_ U. w )
40 18 sseli 
 |-  ( w e. ( ~P ( { B } u. C ) i^i Fin ) -> w e. ~P ( { B } u. C ) )
41 40 elpwid 
 |-  ( w e. ( ~P ( { B } u. C ) i^i Fin ) -> w C_ ( { B } u. C ) )
42 41 ad2antrl 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> w C_ ( { B } u. C ) )
43 pwidg 
 |-  ( B e. V -> B e. ~P B )
44 43 snssd 
 |-  ( B e. V -> { B } C_ ~P B )
45 44 adantr 
 |-  ( ( B e. V /\ C C_ ~P B ) -> { B } C_ ~P B )
46 simpr 
 |-  ( ( B e. V /\ C C_ ~P B ) -> C C_ ~P B )
47 45 46 unssd 
 |-  ( ( B e. V /\ C C_ ~P B ) -> ( { B } u. C ) C_ ~P B )
48 47 ad2antrr 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> ( { B } u. C ) C_ ~P B )
49 42 48 sstrd 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> w C_ ~P B )
50 sspwuni 
 |-  ( w C_ ~P B <-> U. w C_ B )
51 49 50 sylib 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> U. w C_ B )
52 39 51 sstrd 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> |^| w C_ B )
53 33 52 eqsstrd 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> A C_ B )
54 df-ss 
 |-  ( A C_ B <-> ( A i^i B ) = A )
55 53 54 sylib 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> ( A i^i B ) = A )
56 32 55 eqtr2id 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> A = ( B i^i A ) )
57 ineq2 
 |-  ( A = |^| w -> ( B i^i A ) = ( B i^i |^| w ) )
58 57 ad2antll 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> ( B i^i A ) = ( B i^i |^| w ) )
59 56 58 eqtrd 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> A = ( B i^i |^| w ) )
60 intun 
 |-  |^| ( { B } u. w ) = ( |^| { B } i^i |^| w )
61 intsng 
 |-  ( B e. V -> |^| { B } = B )
62 61 ineq1d 
 |-  ( B e. V -> ( |^| { B } i^i |^| w ) = ( B i^i |^| w ) )
63 60 62 eqtr2id 
 |-  ( B e. V -> ( B i^i |^| w ) = |^| ( { B } u. w ) )
64 63 ad3antrrr 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> ( B i^i |^| w ) = |^| ( { B } u. w ) )
65 59 64 eqtrd 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> A = |^| ( { B } u. w ) )
66 undif2 
 |-  ( { B } u. ( w \ { B } ) ) = ( { B } u. w )
67 66 inteqi 
 |-  |^| ( { B } u. ( w \ { B } ) ) = |^| ( { B } u. w )
68 65 67 eqtr4di 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> A = |^| ( { B } u. ( w \ { B } ) ) )
69 intun 
 |-  |^| ( { B } u. ( w \ { B } ) ) = ( |^| { B } i^i |^| ( w \ { B } ) )
70 61 ineq1d 
 |-  ( B e. V -> ( |^| { B } i^i |^| ( w \ { B } ) ) = ( B i^i |^| ( w \ { B } ) ) )
71 69 70 syl5eq 
 |-  ( B e. V -> |^| ( { B } u. ( w \ { B } ) ) = ( B i^i |^| ( w \ { B } ) ) )
72 71 ad3antrrr 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> |^| ( { B } u. ( w \ { B } ) ) = ( B i^i |^| ( w \ { B } ) ) )
73 68 72 eqtrd 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> A = ( B i^i |^| ( w \ { B } ) ) )
74 inteq 
 |-  ( v = ( w \ { B } ) -> |^| v = |^| ( w \ { B } ) )
75 74 ineq2d 
 |-  ( v = ( w \ { B } ) -> ( B i^i |^| v ) = ( B i^i |^| ( w \ { B } ) ) )
76 75 rspceeqv 
 |-  ( ( ( w \ { B } ) e. ( ~P C i^i Fin ) /\ A = ( B i^i |^| ( w \ { B } ) ) ) -> E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) )
77 31 73 76 syl2anc 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ ( w e. ( ~P ( { B } u. C ) i^i Fin ) /\ A = |^| w ) ) -> E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) )
78 77 rexlimdvaa 
 |-  ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) -> ( E. w e. ( ~P ( { B } u. C ) i^i Fin ) A = |^| w -> E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) ) )
79 ssun1 
 |-  { B } C_ ( { B } u. C )
80 79 a1i 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ v e. ( ~P C i^i Fin ) ) -> { B } C_ ( { B } u. C ) )
81 inss1 
 |-  ( ~P C i^i Fin ) C_ ~P C
82 81 sseli 
 |-  ( v e. ( ~P C i^i Fin ) -> v e. ~P C )
83 elpwi 
 |-  ( v e. ~P C -> v C_ C )
84 ssun4 
 |-  ( v C_ C -> v C_ ( { B } u. C ) )
85 82 83 84 3syl 
 |-  ( v e. ( ~P C i^i Fin ) -> v C_ ( { B } u. C ) )
86 85 adantl 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ v e. ( ~P C i^i Fin ) ) -> v C_ ( { B } u. C ) )
87 80 86 unssd 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ v e. ( ~P C i^i Fin ) ) -> ( { B } u. v ) C_ ( { B } u. C ) )
88 vex 
 |-  v e. _V
89 9 88 unex 
 |-  ( { B } u. v ) e. _V
90 89 elpw 
 |-  ( ( { B } u. v ) e. ~P ( { B } u. C ) <-> ( { B } u. v ) C_ ( { B } u. C ) )
91 87 90 sylibr 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ v e. ( ~P C i^i Fin ) ) -> ( { B } u. v ) e. ~P ( { B } u. C ) )
92 snfi 
 |-  { B } e. Fin
93 inss2 
 |-  ( ~P C i^i Fin ) C_ Fin
94 93 sseli 
 |-  ( v e. ( ~P C i^i Fin ) -> v e. Fin )
95 94 adantl 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ v e. ( ~P C i^i Fin ) ) -> v e. Fin )
96 unfi 
 |-  ( ( { B } e. Fin /\ v e. Fin ) -> ( { B } u. v ) e. Fin )
97 92 95 96 sylancr 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ v e. ( ~P C i^i Fin ) ) -> ( { B } u. v ) e. Fin )
98 91 97 elind 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ v e. ( ~P C i^i Fin ) ) -> ( { B } u. v ) e. ( ~P ( { B } u. C ) i^i Fin ) )
99 61 eqcomd 
 |-  ( B e. V -> B = |^| { B } )
100 99 ineq1d 
 |-  ( B e. V -> ( B i^i |^| v ) = ( |^| { B } i^i |^| v ) )
101 intun 
 |-  |^| ( { B } u. v ) = ( |^| { B } i^i |^| v )
102 100 101 eqtr4di 
 |-  ( B e. V -> ( B i^i |^| v ) = |^| ( { B } u. v ) )
103 102 ad3antrrr 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ v e. ( ~P C i^i Fin ) ) -> ( B i^i |^| v ) = |^| ( { B } u. v ) )
104 inteq 
 |-  ( w = ( { B } u. v ) -> |^| w = |^| ( { B } u. v ) )
105 104 rspceeqv 
 |-  ( ( ( { B } u. v ) e. ( ~P ( { B } u. C ) i^i Fin ) /\ ( B i^i |^| v ) = |^| ( { B } u. v ) ) -> E. w e. ( ~P ( { B } u. C ) i^i Fin ) ( B i^i |^| v ) = |^| w )
106 98 103 105 syl2anc 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ v e. ( ~P C i^i Fin ) ) -> E. w e. ( ~P ( { B } u. C ) i^i Fin ) ( B i^i |^| v ) = |^| w )
107 eqeq1 
 |-  ( A = ( B i^i |^| v ) -> ( A = |^| w <-> ( B i^i |^| v ) = |^| w ) )
108 107 rexbidv 
 |-  ( A = ( B i^i |^| v ) -> ( E. w e. ( ~P ( { B } u. C ) i^i Fin ) A = |^| w <-> E. w e. ( ~P ( { B } u. C ) i^i Fin ) ( B i^i |^| v ) = |^| w ) )
109 106 108 syl5ibrcom 
 |-  ( ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) /\ v e. ( ~P C i^i Fin ) ) -> ( A = ( B i^i |^| v ) -> E. w e. ( ~P ( { B } u. C ) i^i Fin ) A = |^| w ) )
110 109 rexlimdva 
 |-  ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) -> ( E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) -> E. w e. ( ~P ( { B } u. C ) i^i Fin ) A = |^| w ) )
111 78 110 impbid 
 |-  ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) -> ( E. w e. ( ~P ( { B } u. C ) i^i Fin ) A = |^| w <-> E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) ) )
112 17 111 bitrd 
 |-  ( ( ( B e. V /\ C C_ ~P B ) /\ A e. _V ) -> ( A e. ( fi ` ( { B } u. C ) ) <-> E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) ) )
113 112 ex 
 |-  ( ( B e. V /\ C C_ ~P B ) -> ( A e. _V -> ( A e. ( fi ` ( { B } u. C ) ) <-> E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) ) ) )
114 2 7 113 pm5.21ndd 
 |-  ( ( B e. V /\ C C_ ~P B ) -> ( A e. ( fi ` ( { B } u. C ) ) <-> E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) ) )