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 ‘ 𝐴 ) ⊆ 𝒫 𝑋 )