Metamath Proof Explorer

Theorem elrfirn

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

Ref Expression
Assertion elrfirn ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ ran 𝐹 ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 frn ⊢ ( 𝐹 : 𝐼 ⟶ 𝒫 𝐵 → ran 𝐹 ⊆ 𝒫 𝐵 )
2 elrfi ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ran 𝐹 ⊆ 𝒫 𝐵 ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ ran 𝐹 ) ) ↔ ∃ 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑤 ) ) )
3 1 2 sylan2 ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ ran 𝐹 ) ) ↔ ∃ 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑤 ) ) )
4 imassrn ⊢ ( 𝐹 “ 𝑣 ) ⊆ ran 𝐹
5 pwexg ⊢ ( 𝐵 ∈ 𝑉 → 𝒫 𝐵 ∈ V )
6 ssexg ⊢ ( ( ran 𝐹 ⊆ 𝒫 𝐵 ∧ 𝒫 𝐵 ∈ V ) → ran 𝐹 ∈ V )
7 1 5 6 syl2anr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) → ran 𝐹 ∈ V )
8 elpw2g ⊢ ( ran 𝐹 ∈ V → ( ( 𝐹 “ 𝑣 ) ∈ 𝒫 ran 𝐹 ↔ ( 𝐹 “ 𝑣 ) ⊆ ran 𝐹 ) )
9 7 8 syl ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) → ( ( 𝐹 “ 𝑣 ) ∈ 𝒫 ran 𝐹 ↔ ( 𝐹 “ 𝑣 ) ⊆ ran 𝐹 ) )
10 4 9 mpbiri ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) → ( 𝐹 “ 𝑣 ) ∈ 𝒫 ran 𝐹 )
11 10 adantr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → ( 𝐹 “ 𝑣 ) ∈ 𝒫 ran 𝐹 )
12 ffun ⊢ ( 𝐹 : 𝐼 ⟶ 𝒫 𝐵 → Fun 𝐹 )
13 12 ad2antlr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → Fun 𝐹 )
14 inss2 ⊢ ( 𝒫 𝐼 ∩ Fin ) ⊆ Fin
15 14 sseli ⊢ ( 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) → 𝑣 ∈ Fin )
16 15 adantl ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → 𝑣 ∈ Fin )
17 imafi ⊢ ( ( Fun 𝐹 ∧ 𝑣 ∈ Fin ) → ( 𝐹 “ 𝑣 ) ∈ Fin )
18 13 16 17 syl2anc ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → ( 𝐹 “ 𝑣 ) ∈ Fin )
19 11 18 elind ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → ( 𝐹 “ 𝑣 ) ∈ ( 𝒫 ran 𝐹 ∩ Fin ) )
20 ffn ⊢ ( 𝐹 : 𝐼 ⟶ 𝒫 𝐵 → 𝐹 Fn 𝐼 )
21 20 ad2antlr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) ) → 𝐹 Fn 𝐼 )
22 inss1 ⊢ ( 𝒫 ran 𝐹 ∩ Fin ) ⊆ 𝒫 ran 𝐹
23 22 sseli ⊢ ( 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) → 𝑤 ∈ 𝒫 ran 𝐹 )
24 23 elpwid ⊢ ( 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) → 𝑤 ⊆ ran 𝐹 )
25 24 adantl ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) ) → 𝑤 ⊆ ran 𝐹 )
26 inss2 ⊢ ( 𝒫 ran 𝐹 ∩ Fin ) ⊆ Fin
27 26 sseli ⊢ ( 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) → 𝑤 ∈ Fin )
28 27 adantl ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) ) → 𝑤 ∈ Fin )
29 fipreima ⊢ ( ( 𝐹 Fn 𝐼 ∧ 𝑤 ⊆ ran 𝐹 ∧ 𝑤 ∈ Fin ) → ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ( 𝐹 “ 𝑣 ) = 𝑤 )
30 21 25 28 29 syl3anc ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) ) → ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ( 𝐹 “ 𝑣 ) = 𝑤 )
31 eqcom ⊢ ( ( 𝐹 “ 𝑣 ) = 𝑤 ↔ 𝑤 = ( 𝐹 “ 𝑣 ) )
32 31 rexbii ⊢ ( ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ( 𝐹 “ 𝑣 ) = 𝑤 ↔ ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝑤 = ( 𝐹 “ 𝑣 ) )
33 30 32 sylib ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) ) → ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝑤 = ( 𝐹 “ 𝑣 ) )
34 inteq ⊢ ( 𝑤 = ( 𝐹 “ 𝑣 ) → ∩ 𝑤 = ∩ ( 𝐹 “ 𝑣 ) )
35 34 ineq2d ⊢ ( 𝑤 = ( 𝐹 “ 𝑣 ) → ( 𝐵 ∩ ∩ 𝑤 ) = ( 𝐵 ∩ ∩ ( 𝐹 “ 𝑣 ) ) )
36 35 eqeq2d ⊢ ( 𝑤 = ( 𝐹 “ 𝑣 ) → ( 𝐴 = ( 𝐵 ∩ ∩ 𝑤 ) ↔ 𝐴 = ( 𝐵 ∩ ∩ ( 𝐹 “ 𝑣 ) ) ) )
37 36 adantl ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑤 = ( 𝐹 “ 𝑣 ) ) → ( 𝐴 = ( 𝐵 ∩ ∩ 𝑤 ) ↔ 𝐴 = ( 𝐵 ∩ ∩ ( 𝐹 “ 𝑣 ) ) ) )
38 19 33 37 rexxfrd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) → ( ∃ 𝑤 ∈ ( 𝒫 ran 𝐹 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑤 ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ ( 𝐹 “ 𝑣 ) ) ) )
39 20 ad2antlr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → 𝐹 Fn 𝐼 )
40 inss1 ⊢ ( 𝒫 𝐼 ∩ Fin ) ⊆ 𝒫 𝐼
41 40 sseli ⊢ ( 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) → 𝑣 ∈ 𝒫 𝐼 )
42 41 elpwid ⊢ ( 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) → 𝑣 ⊆ 𝐼 )
43 42 adantl ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → 𝑣 ⊆ 𝐼 )
44 imaiinfv ⊢ ( ( 𝐹 Fn 𝐼 ∧ 𝑣 ⊆ 𝐼 ) → ∩ 𝑦 ∈ 𝑣 ( 𝐹 ‘ 𝑦 ) = ∩ ( 𝐹 “ 𝑣 ) )
45 39 43 44 syl2anc ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → ∩ 𝑦 ∈ 𝑣 ( 𝐹 ‘ 𝑦 ) = ∩ ( 𝐹 “ 𝑣 ) )
46 45 eqcomd ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → ∩ ( 𝐹 “ 𝑣 ) = ∩ 𝑦 ∈ 𝑣 ( 𝐹 ‘ 𝑦 ) )
47 46 ineq2d ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → ( 𝐵 ∩ ∩ ( 𝐹 “ 𝑣 ) ) = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 ( 𝐹 ‘ 𝑦 ) ) )
48 47 eqeq2d ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) ∧ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) ) → ( 𝐴 = ( 𝐵 ∩ ∩ ( 𝐹 “ 𝑣 ) ) ↔ 𝐴 = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )
49 48 rexbidva ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ ( 𝐹 “ 𝑣 ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )
50 3 38 49 3bitrd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝒫 𝐵 ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ ran 𝐹 ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐼 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑦 ∈ 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) )