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 ∈ I C ⊆ B → A ∈ fi ⁡ B ∪ ran ⁡ y ∈ I ⟼ C ↔ ∃ v ∈ 𝒫 I ∩ Fin A = B ∩ ⋂ y ∈ v C

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 ∈ I C ⊆ B → ∀ y ∈ I C ∈ 𝒫 B
4 3 imp ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B → ∀ y ∈ I C ∈ 𝒫 B
5 eqid ⊢ y ∈ I ⟼ C = y ∈ I ⟼ C
6 5 fmpt ⊢ ∀ y ∈ I C ∈ 𝒫 B ↔ y ∈ I ⟼ C : I ⟶ 𝒫 B
7 4 6 sylib ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B → y ∈ I ⟼ C : I ⟶ 𝒫 B
8 elrfirn ⊢ B ∈ V ∧ y ∈ I ⟼ C : I ⟶ 𝒫 B → A ∈ fi ⁡ B ∪ ran ⁡ y ∈ I ⟼ C ↔ ∃ v ∈ 𝒫 I ∩ Fin A = B ∩ ⋂ z ∈ v y ∈ I ⟼ C ⁡ z
9 7 8 syldan ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B → A ∈ fi ⁡ B ∪ ran ⁡ y ∈ I ⟼ C ↔ ∃ v ∈ 𝒫 I ∩ Fin A = B ∩ ⋂ z ∈ v y ∈ 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 ⊢ Ⅎ _ y y ∈ I ⟼ C ⁡ z
14 nfcv ⊢ Ⅎ _ z y ∈ I ⟼ C ⁡ y
15 fveq2 ⊢ z = y → y ∈ I ⟼ C ⁡ z = y ∈ I ⟼ C ⁡ y
16 13 14 15 cbviin ⊢ ⋂ z ∈ v y ∈ I ⟼ C ⁡ z = ⋂ y ∈ v y ∈ 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 ∈ I C ⊆ B → ∀ y ∈ I y ∈ I ⟼ C ⁡ y = C
25 24 imp ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B → ∀ y ∈ I y ∈ I ⟼ C ⁡ y = C
26 ssralv ⊢ v ⊆ I → ∀ y ∈ I y ∈ I ⟼ C ⁡ y = C → ∀ y ∈ v y ∈ I ⟼ C ⁡ y = C
27 25 26 mpan9 ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B ∧ v ⊆ I → ∀ y ∈ v y ∈ I ⟼ C ⁡ y = C
28 iineq2 ⊢ ∀ y ∈ v y ∈ I ⟼ C ⁡ y = C → ⋂ y ∈ v y ∈ I ⟼ C ⁡ y = ⋂ y ∈ v C
29 27 28 syl ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B ∧ v ⊆ I → ⋂ y ∈ v y ∈ I ⟼ C ⁡ y = ⋂ y ∈ v C
30 16 29 eqtrid ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B ∧ v ⊆ I → ⋂ z ∈ v y ∈ I ⟼ C ⁡ z = ⋂ y ∈ v C
31 30 ineq2d ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B ∧ v ⊆ I → B ∩ ⋂ z ∈ v y ∈ I ⟼ C ⁡ z = B ∩ ⋂ y ∈ v C
32 31 eqeq2d ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B ∧ v ⊆ I → A = B ∩ ⋂ z ∈ v y ∈ I ⟼ C ⁡ z ↔ A = B ∩ ⋂ y ∈ v C
33 12 32 sylan2 ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B ∧ v ∈ 𝒫 I ∩ Fin → A = B ∩ ⋂ z ∈ v y ∈ I ⟼ C ⁡ z ↔ A = B ∩ ⋂ y ∈ v C
34 33 rexbidva ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B → ∃ v ∈ 𝒫 I ∩ Fin A = B ∩ ⋂ z ∈ v y ∈ I ⟼ C ⁡ z ↔ ∃ v ∈ 𝒫 I ∩ Fin A = B ∩ ⋂ y ∈ v C
35 9 34 bitrd ⊢ B ∈ V ∧ ∀ y ∈ I C ⊆ B → A ∈ fi ⁡ B ∪ ran ⁡ y ∈ I ⟼ C ↔ ∃ v ∈ 𝒫 I ∩ Fin A = B ∩ ⋂ y ∈ v C