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

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