This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ 𝐶 ) ) → 𝐴 ∈ V )
2 1 a1i ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ 𝐶 ) ) → 𝐴 ∈ V ) )
3 inex1g ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∩ ∩ 𝑣 ) ∈ V )
4 eleq1 ⊢ ( 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) → ( 𝐴 ∈ V ↔ ( 𝐵 ∩ ∩ 𝑣 ) ∈ V ) )
5 3 4 syl5ibrcom ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) → 𝐴 ∈ V ) )
6 5 rexlimdvw ⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) → 𝐴 ∈ V ) )
7 6 adantr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) → 𝐴 ∈ V ) )
8 simpr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) → 𝐴 ∈ V )
9 snex ⊢ { 𝐵 } ∈ V
10 pwexg ⊢ ( 𝐵 ∈ 𝑉 → 𝒫 𝐵 ∈ V )
11 10 ad2antrr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) → 𝒫 𝐵 ∈ V )
12 simplr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) → 𝐶 ⊆ 𝒫 𝐵 )
13 11 12 ssexd ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) → 𝐶 ∈ V )
14 unexg ⊢ ( ( { 𝐵 } ∈ V ∧ 𝐶 ∈ V ) → ( { 𝐵 } ∪ 𝐶 ) ∈ V )
15 9 13 14 sylancr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) → ( { 𝐵 } ∪ 𝐶 ) ∈ V )
16 elfi ⊢ ( ( 𝐴 ∈ V ∧ ( { 𝐵 } ∪ 𝐶 ) ∈ V ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ 𝐶 ) ) ↔ ∃ 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) 𝐴 = ∩ 𝑤 ) )
17 8 15 16 syl2anc ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ 𝐶 ) ) ↔ ∃ 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) 𝐴 = ∩ 𝑤 ) )
18 inss1 ⊢ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ⊆ 𝒫 ( { 𝐵 } ∪ 𝐶 )
19 uncom ⊢ ( { 𝐵 } ∪ 𝐶 ) = ( 𝐶 ∪ { 𝐵 } )
20 19 pweqi ⊢ 𝒫 ( { 𝐵 } ∪ 𝐶 ) = 𝒫 ( 𝐶 ∪ { 𝐵 } )
21 18 20 sseqtri ⊢ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ⊆ 𝒫 ( 𝐶 ∪ { 𝐵 } )
22 21 sseli ⊢ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) → 𝑤 ∈ 𝒫 ( 𝐶 ∪ { 𝐵 } ) )
23 9 elpwun ⊢ ( 𝑤 ∈ 𝒫 ( 𝐶 ∪ { 𝐵 } ) ↔ ( 𝑤 ∖ { 𝐵 } ) ∈ 𝒫 𝐶 )
24 22 23 sylib ⊢ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) → ( 𝑤 ∖ { 𝐵 } ) ∈ 𝒫 𝐶 )
25 24 ad2antrl ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ( 𝑤 ∖ { 𝐵 } ) ∈ 𝒫 𝐶 )
26 inss2 ⊢ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ⊆ Fin
27 26 sseli ⊢ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) → 𝑤 ∈ Fin )
28 diffi ⊢ ( 𝑤 ∈ Fin → ( 𝑤 ∖ { 𝐵 } ) ∈ Fin )
29 27 28 syl ⊢ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) → ( 𝑤 ∖ { 𝐵 } ) ∈ Fin )
30 29 ad2antrl ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ( 𝑤 ∖ { 𝐵 } ) ∈ Fin )
31 25 30 elind ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ( 𝑤 ∖ { 𝐵 } ) ∈ ( 𝒫 𝐶 ∩ Fin ) )
32 incom ⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 )
33 simprr ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝐴 = ∩ 𝑤 )
34 simplr ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝐴 ∈ V )
35 33 34 eqeltrrd ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ∩ 𝑤 ∈ V )
36 intex ⊢ ( 𝑤 ≠ ∅ ↔ ∩ 𝑤 ∈ V )
37 35 36 sylibr ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝑤 ≠ ∅ )
38 intssuni ⊢ ( 𝑤 ≠ ∅ → ∩ 𝑤 ⊆ ∪ 𝑤 )
39 37 38 syl ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ∩ 𝑤 ⊆ ∪ 𝑤 )
40 18 sseli ⊢ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) → 𝑤 ∈ 𝒫 ( { 𝐵 } ∪ 𝐶 ) )
41 40 elpwid ⊢ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) → 𝑤 ⊆ ( { 𝐵 } ∪ 𝐶 ) )
42 41 ad2antrl ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝑤 ⊆ ( { 𝐵 } ∪ 𝐶 ) )
43 pwidg ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵 )
44 43 snssd ⊢ ( 𝐵 ∈ 𝑉 → { 𝐵 } ⊆ 𝒫 𝐵 )
45 44 adantr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) → { 𝐵 } ⊆ 𝒫 𝐵 )
46 simpr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) → 𝐶 ⊆ 𝒫 𝐵 )
47 45 46 unssd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) → ( { 𝐵 } ∪ 𝐶 ) ⊆ 𝒫 𝐵 )
48 47 ad2antrr ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ( { 𝐵 } ∪ 𝐶 ) ⊆ 𝒫 𝐵 )
49 42 48 sstrd ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝑤 ⊆ 𝒫 𝐵 )
50 sspwuni ⊢ ( 𝑤 ⊆ 𝒫 𝐵 ↔ ∪ 𝑤 ⊆ 𝐵 )
51 49 50 sylib ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ∪ 𝑤 ⊆ 𝐵 )
52 39 51 sstrd ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ∩ 𝑤 ⊆ 𝐵 )
53 33 52 eqsstrd ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝐴 ⊆ 𝐵 )
54 dfss2 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
55 53 54 sylib ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ( 𝐴 ∩ 𝐵 ) = 𝐴 )
56 32 55 eqtr2id ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝐴 = ( 𝐵 ∩ 𝐴 ) )
57 ineq2 ⊢ ( 𝐴 = ∩ 𝑤 → ( 𝐵 ∩ 𝐴 ) = ( 𝐵 ∩ ∩ 𝑤 ) )
58 57 ad2antll ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ( 𝐵 ∩ 𝐴 ) = ( 𝐵 ∩ ∩ 𝑤 ) )
59 56 58 eqtrd ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝐴 = ( 𝐵 ∩ ∩ 𝑤 ) )
60 intun ⊢ ∩ ( { 𝐵 } ∪ 𝑤 ) = ( ∩ { 𝐵 } ∩ ∩ 𝑤 )
61 intsng ⊢ ( 𝐵 ∈ 𝑉 → ∩ { 𝐵 } = 𝐵 )
62 61 ineq1d ⊢ ( 𝐵 ∈ 𝑉 → ( ∩ { 𝐵 } ∩ ∩ 𝑤 ) = ( 𝐵 ∩ ∩ 𝑤 ) )
63 60 62 eqtr2id ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∩ ∩ 𝑤 ) = ∩ ( { 𝐵 } ∪ 𝑤 ) )
64 63 ad3antrrr ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ( 𝐵 ∩ ∩ 𝑤 ) = ∩ ( { 𝐵 } ∪ 𝑤 ) )
65 59 64 eqtrd ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝐴 = ∩ ( { 𝐵 } ∪ 𝑤 ) )
66 undif2 ⊢ ( { 𝐵 } ∪ ( 𝑤 ∖ { 𝐵 } ) ) = ( { 𝐵 } ∪ 𝑤 )
67 66 inteqi ⊢ ∩ ( { 𝐵 } ∪ ( 𝑤 ∖ { 𝐵 } ) ) = ∩ ( { 𝐵 } ∪ 𝑤 )
68 65 67 eqtr4di ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝐴 = ∩ ( { 𝐵 } ∪ ( 𝑤 ∖ { 𝐵 } ) ) )
69 intun ⊢ ∩ ( { 𝐵 } ∪ ( 𝑤 ∖ { 𝐵 } ) ) = ( ∩ { 𝐵 } ∩ ∩ ( 𝑤 ∖ { 𝐵 } ) )
70 61 ineq1d ⊢ ( 𝐵 ∈ 𝑉 → ( ∩ { 𝐵 } ∩ ∩ ( 𝑤 ∖ { 𝐵 } ) ) = ( 𝐵 ∩ ∩ ( 𝑤 ∖ { 𝐵 } ) ) )
71 69 70 eqtrid ⊢ ( 𝐵 ∈ 𝑉 → ∩ ( { 𝐵 } ∪ ( 𝑤 ∖ { 𝐵 } ) ) = ( 𝐵 ∩ ∩ ( 𝑤 ∖ { 𝐵 } ) ) )
72 71 ad3antrrr ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ∩ ( { 𝐵 } ∪ ( 𝑤 ∖ { 𝐵 } ) ) = ( 𝐵 ∩ ∩ ( 𝑤 ∖ { 𝐵 } ) ) )
73 68 72 eqtrd ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → 𝐴 = ( 𝐵 ∩ ∩ ( 𝑤 ∖ { 𝐵 } ) ) )
74 inteq ⊢ ( 𝑣 = ( 𝑤 ∖ { 𝐵 } ) → ∩ 𝑣 = ∩ ( 𝑤 ∖ { 𝐵 } ) )
75 74 ineq2d ⊢ ( 𝑣 = ( 𝑤 ∖ { 𝐵 } ) → ( 𝐵 ∩ ∩ 𝑣 ) = ( 𝐵 ∩ ∩ ( 𝑤 ∖ { 𝐵 } ) ) )
76 75 rspceeqv ⊢ ( ( ( 𝑤 ∖ { 𝐵 } ) ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ 𝐴 = ( 𝐵 ∩ ∩ ( 𝑤 ∖ { 𝐵 } ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) )
77 31 73 76 syl2anc ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ 𝐴 = ∩ 𝑤 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) )
78 77 rexlimdvaa ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) → ( ∃ 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) 𝐴 = ∩ 𝑤 → ∃ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) ) )
79 ssun1 ⊢ { 𝐵 } ⊆ ( { 𝐵 } ∪ 𝐶 )
80 79 a1i ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → { 𝐵 } ⊆ ( { 𝐵 } ∪ 𝐶 ) )
81 inss1 ⊢ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝒫 𝐶
82 81 sseli ⊢ ( 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑣 ∈ 𝒫 𝐶 )
83 elpwi ⊢ ( 𝑣 ∈ 𝒫 𝐶 → 𝑣 ⊆ 𝐶 )
84 ssun4 ⊢ ( 𝑣 ⊆ 𝐶 → 𝑣 ⊆ ( { 𝐵 } ∪ 𝐶 ) )
85 82 83 84 3syl ⊢ ( 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑣 ⊆ ( { 𝐵 } ∪ 𝐶 ) )
86 85 adantl ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑣 ⊆ ( { 𝐵 } ∪ 𝐶 ) )
87 80 86 unssd ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( { 𝐵 } ∪ 𝑣 ) ⊆ ( { 𝐵 } ∪ 𝐶 ) )
88 vex ⊢ 𝑣 ∈ V
89 9 88 unex ⊢ ( { 𝐵 } ∪ 𝑣 ) ∈ V
90 89 elpw ⊢ ( ( { 𝐵 } ∪ 𝑣 ) ∈ 𝒫 ( { 𝐵 } ∪ 𝐶 ) ↔ ( { 𝐵 } ∪ 𝑣 ) ⊆ ( { 𝐵 } ∪ 𝐶 ) )
91 87 90 sylibr ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( { 𝐵 } ∪ 𝑣 ) ∈ 𝒫 ( { 𝐵 } ∪ 𝐶 ) )
92 snfi ⊢ { 𝐵 } ∈ Fin
93 inss2 ⊢ ( 𝒫 𝐶 ∩ Fin ) ⊆ Fin
94 93 sseli ⊢ ( 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑣 ∈ Fin )
95 94 adantl ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑣 ∈ Fin )
96 unfi ⊢ ( ( { 𝐵 } ∈ Fin ∧ 𝑣 ∈ Fin ) → ( { 𝐵 } ∪ 𝑣 ) ∈ Fin )
97 92 95 96 sylancr ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( { 𝐵 } ∪ 𝑣 ) ∈ Fin )
98 91 97 elind ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( { 𝐵 } ∪ 𝑣 ) ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) )
99 61 eqcomd ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ∩ { 𝐵 } )
100 99 ineq1d ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∩ ∩ 𝑣 ) = ( ∩ { 𝐵 } ∩ ∩ 𝑣 ) )
101 intun ⊢ ∩ ( { 𝐵 } ∪ 𝑣 ) = ( ∩ { 𝐵 } ∩ ∩ 𝑣 )
102 100 101 eqtr4di ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∩ ∩ 𝑣 ) = ∩ ( { 𝐵 } ∪ 𝑣 ) )
103 102 ad3antrrr ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐵 ∩ ∩ 𝑣 ) = ∩ ( { 𝐵 } ∪ 𝑣 ) )
104 inteq ⊢ ( 𝑤 = ( { 𝐵 } ∪ 𝑣 ) → ∩ 𝑤 = ∩ ( { 𝐵 } ∪ 𝑣 ) )
105 104 rspceeqv ⊢ ( ( ( { 𝐵 } ∪ 𝑣 ) ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ∧ ( 𝐵 ∩ ∩ 𝑣 ) = ∩ ( { 𝐵 } ∪ 𝑣 ) ) → ∃ 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ( 𝐵 ∩ ∩ 𝑣 ) = ∩ 𝑤 )
106 98 103 105 syl2anc ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ∃ 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ( 𝐵 ∩ ∩ 𝑣 ) = ∩ 𝑤 )
107 eqeq1 ⊢ ( 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) → ( 𝐴 = ∩ 𝑤 ↔ ( 𝐵 ∩ ∩ 𝑣 ) = ∩ 𝑤 ) )
108 107 rexbidv ⊢ ( 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) → ( ∃ 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) 𝐴 = ∩ 𝑤 ↔ ∃ 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) ( 𝐵 ∩ ∩ 𝑣 ) = ∩ 𝑤 ) )
109 106 108 syl5ibrcom ⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) ∧ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) → ∃ 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) 𝐴 = ∩ 𝑤 ) )
110 109 rexlimdva ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) → ( ∃ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) → ∃ 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) 𝐴 = ∩ 𝑤 ) )
111 78 110 impbid ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) → ( ∃ 𝑤 ∈ ( 𝒫 ( { 𝐵 } ∪ 𝐶 ) ∩ Fin ) 𝐴 = ∩ 𝑤 ↔ ∃ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) ) )
112 17 111 bitrd ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) ∧ 𝐴 ∈ V ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ 𝐶 ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) ) )
113 112 ex ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) → ( 𝐴 ∈ V → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ 𝐶 ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) ) ) )
114 2 7 113 pm5.21ndd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝒫 𝐵 ) → ( 𝐴 ∈ ( fi ‘ ( { 𝐵 } ∪ 𝐶 ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝐶 ∩ Fin ) 𝐴 = ( 𝐵 ∩ ∩ 𝑣 ) ) )