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 ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ ran ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 elpw2g ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐶 ∈ 𝒫 𝐵 ↔ 𝐶 ⊆ 𝐵 ) )
2 1 biimprd ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐶 ⊆ 𝐵 → 𝐶 ∈ 𝒫 𝐵 ) )
3 2 ralimdv ⊢ ( 𝐵 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 → ∀ 𝑦 ∈ 𝐼 𝐶 ∈ 𝒫 𝐵 ) )
4 3 imp ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) → ∀ 𝑦 ∈ 𝐼 𝐶 ∈ 𝒫 𝐵 )
5 eqid ⊢ ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) = ( 𝑦 ∈ 𝐼 ↦ 𝐶 )
6 5 fmpt ⊢ ( ∀ 𝑦 ∈ 𝐼 𝐶 ∈ 𝒫 𝐵 ↔ ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) : 𝐼 ⟶ 𝒫 𝐵 )
7 4 6 sylib ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) → ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) : 𝐼 ⟶ 𝒫 𝐵 )
8 elrfirn ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) : 𝐼 ⟶ 𝒫 𝐵 ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ ran ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑧 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑧 ) ) ) )
9 7 8 syldan ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ ran ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑧 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑧 ) ) ) )
10 inss1 ⊢ ( 𝒫 𝐼 ∩ Fin ) ⊆ 𝒫 𝐼
11 10 sseli ⊢ ( 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) → 𝑣 ∈ 𝒫 𝐼 )
12 11 elpwid ⊢ ( 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) → 𝑣 ⊆ 𝐼 )
13 nffvmpt1 ⊢ Ⅎ 𝑦 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑧 )
14 nfcv ⊢ Ⅎ 𝑧 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 )
15 fveq2 ⊢ ( 𝑧 = 𝑦 → ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑧 ) = ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) )
16 13 14 15 cbviin ⊢ ∩ 𝑧 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑧 ) = ∩ 𝑦 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 )
17 simplr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼 ) ∧ 𝐶 ⊆ 𝐵 ) → 𝑦 ∈ 𝐼 )
18 simpll ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼 ) ∧ 𝐶 ⊆ 𝐵 ) → 𝐵 ∈ 𝑉 )
19 simpr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼 ) ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 ⊆ 𝐵 )
20 18 19 ssexd ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼 ) ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 ∈ V )
21 5 fvmpt2 ⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝐶 ∈ V ) → ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐶 )
22 17 20 21 syl2anc ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼 ) ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐶 )
23 22 ex ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐶 ⊆ 𝐵 → ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐶 ) )
24 23 ralimdva ⊢ ( 𝐵 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 → ∀ 𝑦 ∈ 𝐼 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐶 ) )
25 24 imp ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) → ∀ 𝑦 ∈ 𝐼 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐶 )
26 ssralv ⊢ ( 𝑣 ⊆ 𝐼 → ( ∀ 𝑦 ∈ 𝐼 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐶 → ∀ 𝑦 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐶 ) )
27 25 26 mpan9 ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) ∧ 𝑣 ⊆ 𝐼 ) → ∀ 𝑦 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐶 )
28 iineq2 ⊢ ( ∀ 𝑦 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = 𝐶 → ∩ 𝑦 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = ∩ 𝑦 ∈ 𝑣 𝐶 )
29 27 28 syl ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) ∧ 𝑣 ⊆ 𝐼 ) → ∩ 𝑦 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑦 ) = ∩ 𝑦 ∈ 𝑣 𝐶 )
30 16 29 syl5eq ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) ∧ 𝑣 ⊆ 𝐼 ) → ∩ 𝑧 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑧 ) = ∩ 𝑦 ∈ 𝑣 𝐶 )
31 30 ineq2d ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) ∧ 𝑣 ⊆ 𝐼 ) → ( 𝐵 ∩ ∩ 𝑧 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑧 ) ) = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 𝐶 ) )
32 31 eqeq2d ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) ∧ 𝑣 ⊆ 𝐼 ) → ( 𝐴 = ( 𝐵 ∩ ∩ 𝑧 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑧 ) ) ↔ 𝐴 = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 𝐶 ) ) )
33 12 32 sylan2 ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → ( 𝐴 = ( 𝐵 ∩ ∩ 𝑧 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑧 ) ) ↔ 𝐴 = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 𝐶 ) ) )
34 33 rexbidva ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑧 ∈ 𝑣 ( ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ‘ 𝑧 ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 𝐶 ) ) )
35 9 34 bitrd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐼 𝐶 ⊆ 𝐵 ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ ran ( 𝑦 ∈ 𝐼 ↦ 𝐶 ) ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 𝐶 ) ) )