cvmsiota

Description: Identify the unique element of T containing A . (Contributed by Mario Carneiro, 14-Feb-2015)

	Ref	Expression
Hypotheses	cvmcov.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
	cvmseu.1	$⊢ B = ⋃ C$
	cvmsiota.2	$⊢ W = (ι x \in T \| A \in x)$
Assertion	cvmsiota	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to (W \in T \land A \in W)$

Step	Hyp	Ref	Expression
1		cvmcov.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
2		cvmseu.1	$⊢ B = ⋃ C$
3		cvmsiota.2	$⊢ W = (ι x \in T \| A \in x)$
4	1 2	cvmseu	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to \exists! x \in T A \in x$
5		riotacl2	$⊢ \exists! x \in T A \in x \to (ι x \in T \| A \in x) \in \{x \in T \| A \in x\}$
6	4 5	syl	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to (ι x \in T \| A \in x) \in \{x \in T \| A \in x\}$
7	3 6	eqeltrid	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to W \in \{x \in T \| A \in x\}$
8		eleq2	$⊢ v = W \to (A \in v \leftrightarrow A \in W)$
9		eleq2	$⊢ x = v \to (A \in x \leftrightarrow A \in v)$
10	9	cbvrabv	$⊢ \{x \in T \| A \in x\} = \{v \in T \| A \in v\}$
11	8 10	elrab2	$⊢ W \in \{x \in T \| A \in x\} \leftrightarrow (W \in T \land A \in W)$
12	7 11	sylib	$⊢ (F \in (C CovMap J) \land (T \in S (U) \land A \in B \land F (A) \in U)) \to (W \in T \land A \in W)$

Metamath Proof Explorer