Metamath Proof Explorer

Theorem elfir

Description: Sufficient condition for an element of ( fiB ) . (Contributed by Mario Carneiro, 24-Nov-2013)

		Ref	Expression
	Assertion	elfir	$⊢ (B \in V \land (A \subseteq B \land A \neq \emptyset \land A \in Fin)) \to ⋂ A \in fi (B)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \subseteq B \land A \neq \emptyset \land A \in Fin) \to A \subseteq B$
2		elpw2g	$⊢ B \in V \to (A \in 𝒫 B \leftrightarrow A \subseteq B)$
3	1 2	imbitrrid	$⊢ B \in V \to ((A \subseteq B \land A \neq \emptyset \land A \in Fin) \to A \in 𝒫 B)$
4	3	imp	$⊢ (B \in V \land (A \subseteq B \land A \neq \emptyset \land A \in Fin)) \to A \in 𝒫 B$
5		simpr3	$⊢ (B \in V \land (A \subseteq B \land A \neq \emptyset \land A \in Fin)) \to A \in Fin$
6	4 5	elind	$⊢ (B \in V \land (A \subseteq B \land A \neq \emptyset \land A \in Fin)) \to A \in (𝒫 B \cap Fin)$
7		eqid	$⊢ ⋂ A = ⋂ A$
8		inteq	$⊢ x = A \to ⋂ x = ⋂ A$
9	8	rspceeqv	$⊢ (A \in (𝒫 B \cap Fin) \land ⋂ A = ⋂ A) \to \exists x \in (𝒫 B \cap Fin) ⋂ A = ⋂ x$
10	6 7 9	sylancl	$⊢ (B \in V \land (A \subseteq B \land A \neq \emptyset \land A \in Fin)) \to \exists x \in (𝒫 B \cap Fin) ⋂ A = ⋂ x$
11		simp2	$⊢ (A \subseteq B \land A \neq \emptyset \land A \in Fin) \to A \neq \emptyset$
12		intex	$⊢ A \neq \emptyset \leftrightarrow ⋂ A \in V$
13	11 12	sylib	$⊢ (A \subseteq B \land A \neq \emptyset \land A \in Fin) \to ⋂ A \in V$
14		id	$⊢ B \in V \to B \in V$
15		elfi	$⊢ (⋂ A \in V \land B \in V) \to (⋂ A \in fi (B) \leftrightarrow \exists x \in (𝒫 B \cap Fin) ⋂ A = ⋂ x)$
16	13 14 15	syl2anr	$⊢ (B \in V \land (A \subseteq B \land A \neq \emptyset \land A \in Fin)) \to (⋂ A \in fi (B) \leftrightarrow \exists x \in (𝒫 B \cap Fin) ⋂ A = ⋂ x)$
17	10 16	mpbird	$⊢ (B \in V \land (A \subseteq B \land A \neq \emptyset \land A \in Fin)) \to ⋂ A \in fi (B)$