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 ⁡ A ⊆ 𝒫 ⋃ A

Proof

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