Metamath Proof Explorer

Theorem elrfirn2

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

Ref Expression
Assertion elrfirn2 ⊢B∈V∧∀y∈IC⊆B→A∈fi⁡B∪ran⁡y∈I⟼C↔∃v∈𝒫I∩FinA=B∩⋂y∈vC

Proof

Step Hyp Ref Expression
1 elpw2g ⊢B∈V→C∈𝒫B↔C⊆B
2 1 biimprd ⊢B∈V→C⊆B→C∈𝒫B
3 2 ralimdv ⊢B∈V→∀y∈IC⊆B→∀y∈IC∈𝒫B
4 3 imp ⊢B∈V∧∀y∈IC⊆B→∀y∈IC∈𝒫B
5 eqid ⊢y∈I⟼C=y∈I⟼C
6 5 fmpt ⊢∀y∈IC∈𝒫B↔y∈I⟼C:I⟶𝒫B
7 4 6 sylib ⊢B∈V∧∀y∈IC⊆B→y∈I⟼C:I⟶𝒫B
8 elrfirn ⊢B∈V∧y∈I⟼C:I⟶𝒫B→A∈fi⁡B∪ran⁡y∈I⟼C↔∃v∈𝒫I∩FinA=B∩⋂z∈vy∈I⟼C⁡z
9 7 8 syldan ⊢B∈V∧∀y∈IC⊆B→A∈fi⁡B∪ran⁡y∈I⟼C↔∃v∈𝒫I∩FinA=B∩⋂z∈vy∈I⟼C⁡z
10 inss1 ⊢𝒫I∩Fin⊆𝒫I
11 10 sseli ⊢v∈𝒫I∩Fin→v∈𝒫I
12 11 elpwid ⊢v∈𝒫I∩Fin→v⊆I
13 nffvmpt1 ⊢Ⅎ_yy∈I⟼C⁡z
14 nfcv ⊢Ⅎ_zy∈I⟼C⁡y
15 fveq2 ⊢z=y→y∈I⟼C⁡z=y∈I⟼C⁡y
16 13 14 15 cbviin ⊢⋂z∈vy∈I⟼C⁡z=⋂y∈vy∈I⟼C⁡y
17 simplr ⊢B∈V∧y∈I∧C⊆B→y∈I
18 simpll ⊢B∈V∧y∈I∧C⊆B→B∈V
19 simpr ⊢B∈V∧y∈I∧C⊆B→C⊆B
20 18 19 ssexd ⊢B∈V∧y∈I∧C⊆B→C∈V
21 5 fvmpt2 ⊢y∈I∧C∈V→y∈I⟼C⁡y=C
22 17 20 21 syl2anc ⊢B∈V∧y∈I∧C⊆B→y∈I⟼C⁡y=C
23 22 ex ⊢B∈V∧y∈I→C⊆B→y∈I⟼C⁡y=C
24 23 ralimdva ⊢B∈V→∀y∈IC⊆B→∀y∈Iy∈I⟼C⁡y=C
25 24 imp ⊢B∈V∧∀y∈IC⊆B→∀y∈Iy∈I⟼C⁡y=C
26 ssralv ⊢v⊆I→∀y∈Iy∈I⟼C⁡y=C→∀y∈vy∈I⟼C⁡y=C
27 25 26 mpan9 ⊢B∈V∧∀y∈IC⊆B∧v⊆I→∀y∈vy∈I⟼C⁡y=C
28 iineq2 ⊢∀y∈vy∈I⟼C⁡y=C→⋂y∈vy∈I⟼C⁡y=⋂y∈vC
29 27 28 syl ⊢B∈V∧∀y∈IC⊆B∧v⊆I→⋂y∈vy∈I⟼C⁡y=⋂y∈vC
30 16 29 eqtrid ⊢B∈V∧∀y∈IC⊆B∧v⊆I→⋂z∈vy∈I⟼C⁡z=⋂y∈vC
31 30 ineq2d ⊢B∈V∧∀y∈IC⊆B∧v⊆I→B∩⋂z∈vy∈I⟼C⁡z=B∩⋂y∈vC
32 31 eqeq2d ⊢B∈V∧∀y∈IC⊆B∧v⊆I→A=B∩⋂z∈vy∈I⟼C⁡z↔A=B∩⋂y∈vC
33 12 32 sylan2 ⊢B∈V∧∀y∈IC⊆B∧v∈𝒫I∩Fin→A=B∩⋂z∈vy∈I⟼C⁡z↔A=B∩⋂y∈vC
34 33 rexbidva ⊢B∈V∧∀y∈IC⊆B→∃v∈𝒫I∩FinA=B∩⋂z∈vy∈I⟼C⁡z↔∃v∈𝒫I∩FinA=B∩⋂y∈vC
35 9 34 bitrd ⊢B∈V∧∀y∈IC⊆B→A∈fi⁡B∪ran⁡y∈I⟼C↔∃v∈𝒫I∩FinA=B∩⋂y∈vC