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 ∩ Fin A = 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 ∩ Fin A = B ∩ ⋂ v → A ∈ V
7 6 adantr ⊢ B ∈ V ∧ C ⊆ 𝒫 B → ∃ v ∈ 𝒫 C ∩ Fin A = 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 ∩ Fin A = ⋂ w
17 8 15 16 syl2anc ⊢ B ∈ V ∧ C ⊆ 𝒫 B ∧ A ∈ V → A ∈ fi ⁡ B ∪ C ↔ ∃ w ∈ 𝒫 B ∪ C ∩ Fin A = ⋂ 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 dfss2 ⊢ 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 ∩ Fin A = B ∩ ⋂ v
77 31 73 76 syl2anc ⊢ B ∈ V ∧ C ⊆ 𝒫 B ∧ A ∈ V ∧ w ∈ 𝒫 B ∪ C ∩ Fin ∧ A = ⋂ w → ∃ v ∈ 𝒫 C ∩ Fin A = B ∩ ⋂ v
78 77 rexlimdvaa ⊢ B ∈ V ∧ C ⊆ 𝒫 B ∧ A ∈ V → ∃ w ∈ 𝒫 B ∪ C ∩ Fin A = ⋂ w → ∃ v ∈ 𝒫 C ∩ Fin A = 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 ∩ Fin B ∩ ⋂ v = ⋂ w
106 98 103 105 syl2anc ⊢ B ∈ V ∧ C ⊆ 𝒫 B ∧ A ∈ V ∧ v ∈ 𝒫 C ∩ Fin → ∃ w ∈ 𝒫 B ∪ C ∩ Fin B ∩ ⋂ v = ⋂ w
107 eqeq1 ⊢ A = B ∩ ⋂ v → A = ⋂ w ↔ B ∩ ⋂ v = ⋂ w
108 107 rexbidv ⊢ A = B ∩ ⋂ v → ∃ w ∈ 𝒫 B ∪ C ∩ Fin A = ⋂ w ↔ ∃ w ∈ 𝒫 B ∪ C ∩ Fin B ∩ ⋂ v = ⋂ w
109 106 108 syl5ibrcom ⊢ B ∈ V ∧ C ⊆ 𝒫 B ∧ A ∈ V ∧ v ∈ 𝒫 C ∩ Fin → A = B ∩ ⋂ v → ∃ w ∈ 𝒫 B ∪ C ∩ Fin A = ⋂ w
110 109 rexlimdva ⊢ B ∈ V ∧ C ⊆ 𝒫 B ∧ A ∈ V → ∃ v ∈ 𝒫 C ∩ Fin A = B ∩ ⋂ v → ∃ w ∈ 𝒫 B ∪ C ∩ Fin A = ⋂ w
111 78 110 impbid ⊢ B ∈ V ∧ C ⊆ 𝒫 B ∧ A ∈ V → ∃ w ∈ 𝒫 B ∪ C ∩ Fin A = ⋂ w ↔ ∃ v ∈ 𝒫 C ∩ Fin A = B ∩ ⋂ v
112 17 111 bitrd ⊢ B ∈ V ∧ C ⊆ 𝒫 B ∧ A ∈ V → A ∈ fi ⁡ B ∪ C ↔ ∃ v ∈ 𝒫 C ∩ Fin A = B ∩ ⋂ v
113 112 ex ⊢ B ∈ V ∧ C ⊆ 𝒫 B → A ∈ V → A ∈ fi ⁡ B ∪ C ↔ ∃ v ∈ 𝒫 C ∩ Fin A = B ∩ ⋂ v
114 2 7 113 pm5.21ndd ⊢ B ∈ V ∧ C ⊆ 𝒫 B → A ∈ fi ⁡ B ∪ C ↔ ∃ v ∈ 𝒫 C ∩ Fin A = B ∩ ⋂ v