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∈V∧C⊆𝒫B→A∈fi⁡B∪C↔∃v∈𝒫C∩FinA=B∩⋂v

Proof

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