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