rintn0

Description: Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015) (Revised by Mario Carneiro, 5-Jun-2015)

		Ref	Expression
	Assertion	rintn0	$⊢ (X \subseteq 𝒫 A \land X \neq \emptyset) \to A \cap ⋂ X = ⋂ X$

Step	Hyp	Ref	Expression
1		intssuni2	$⊢ (X \subseteq 𝒫 A \land X \neq \emptyset) \to ⋂ X \subseteq ⋃ 𝒫 A$
2		ssid	$⊢ 𝒫 A \subseteq 𝒫 A$
3		sspwuni	$⊢ 𝒫 A \subseteq 𝒫 A \leftrightarrow ⋃ 𝒫 A \subseteq A$
4	2 3	mpbi	$⊢ ⋃ 𝒫 A \subseteq A$
5	1 4	sstrdi	$⊢ (X \subseteq 𝒫 A \land X \neq \emptyset) \to ⋂ X \subseteq A$
6		sseqin2	$⊢ ⋂ X \subseteq A \leftrightarrow A \cap ⋂ X = ⋂ X$
7	5 6	sylib	$⊢ (X \subseteq 𝒫 A \land X \neq \emptyset) \to A \cap ⋂ X = ⋂ X$

Metamath Proof Explorer