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

Metamath Proof Explorer

Theorem fipwss

Description: If a set is a family of subsets of some base set, then so is its finite intersection. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fipwss ( 𝐴 ⊆ 𝒫 𝑋 → ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 )

Proof

Step Hyp Ref Expression
1 fiuni ⊢ ( 𝐴 ∈ V → ∪ 𝐴 = ∪ ( fi ‘ 𝐴 ) )
2 1 sseq1d ⊢ ( 𝐴 ∈ V → ( ∪ 𝐴 ⊆ 𝑋 ↔ ∪ ( fi ‘ 𝐴 ) ⊆ 𝑋 ) )
3 sspwuni ⊢ ( 𝐴 ⊆ 𝒫 𝑋 ↔ ∪ 𝐴 ⊆ 𝑋 )
4 sspwuni ⊢ ( ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 ↔ ∪ ( fi ‘ 𝐴 ) ⊆ 𝑋 )
5 2 3 4 3bitr4g ⊢ ( 𝐴 ∈ V → ( 𝐴 ⊆ 𝒫 𝑋 ↔ ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 ) )
6 5 biimpa ⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ⊆ 𝒫 𝑋 ) → ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 )
7 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( fi ‘ 𝐴 ) = ∅ )
8 0ss ⊢ ∅ ⊆ 𝒫 𝑋
9 7 8 eqsstrdi ⊢ ( ¬ 𝐴 ∈ V → ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 )
10 9 adantr ⊢ ( ( ¬ 𝐴 ∈ V ∧ 𝐴 ⊆ 𝒫 𝑋 ) → ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 )
11 6 10 pm2.61ian ⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( fi ‘ 𝐴 ) ⊆ 𝒫 𝑋 )