Metamath Proof Explorer


Theorem fipwuni

Description: The set of finite intersections of a set is contained in the powerset of the union of the elements of A . (Contributed by Mario Carneiro, 24-Nov-2013) (Proof shortened by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion fipwuni ( fi ‘ 𝐴 ) ⊆ 𝒫 𝐴

Proof

Step Hyp Ref Expression
1 uniexg ( 𝐴 ∈ V → 𝐴 ∈ V )
2 1 pwexd ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V )
3 pwuni 𝐴 ⊆ 𝒫 𝐴
4 fiss ( ( 𝒫 𝐴 ∈ V ∧ 𝐴 ⊆ 𝒫 𝐴 ) → ( fi ‘ 𝐴 ) ⊆ ( fi ‘ 𝒫 𝐴 ) )
5 2 3 4 sylancl ( 𝐴 ∈ V → ( fi ‘ 𝐴 ) ⊆ ( fi ‘ 𝒫 𝐴 ) )
6 ssinss1 ( 𝑥 𝐴 → ( 𝑥𝑦 ) ⊆ 𝐴 )
7 vex 𝑥 ∈ V
8 7 elpw ( 𝑥 ∈ 𝒫 𝐴𝑥 𝐴 )
9 7 inex1 ( 𝑥𝑦 ) ∈ V
10 9 elpw ( ( 𝑥𝑦 ) ∈ 𝒫 𝐴 ↔ ( 𝑥𝑦 ) ⊆ 𝐴 )
11 6 8 10 3imtr4i ( 𝑥 ∈ 𝒫 𝐴 → ( 𝑥𝑦 ) ∈ 𝒫 𝐴 )
12 11 adantr ( ( 𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴 ) → ( 𝑥𝑦 ) ∈ 𝒫 𝐴 )
13 12 rgen2 𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴 ( 𝑥𝑦 ) ∈ 𝒫 𝐴
14 inficl ( 𝒫 𝐴 ∈ V → ( ∀ 𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴 ( 𝑥𝑦 ) ∈ 𝒫 𝐴 ↔ ( fi ‘ 𝒫 𝐴 ) = 𝒫 𝐴 ) )
15 2 14 syl ( 𝐴 ∈ V → ( ∀ 𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴 ( 𝑥𝑦 ) ∈ 𝒫 𝐴 ↔ ( fi ‘ 𝒫 𝐴 ) = 𝒫 𝐴 ) )
16 13 15 mpbii ( 𝐴 ∈ V → ( fi ‘ 𝒫 𝐴 ) = 𝒫 𝐴 )
17 5 16 sseqtrd ( 𝐴 ∈ V → ( fi ‘ 𝐴 ) ⊆ 𝒫 𝐴 )
18 fvprc ( ¬ 𝐴 ∈ V → ( fi ‘ 𝐴 ) = ∅ )
19 0ss ∅ ⊆ 𝒫 𝐴
20 18 19 eqsstrdi ( ¬ 𝐴 ∈ V → ( fi ‘ 𝐴 ) ⊆ 𝒫 𝐴 )
21 17 20 pm2.61i ( fi ‘ 𝐴 ) ⊆ 𝒫 𝐴