cmpcovf

Description: Combine cmpcov with ac6sfi to show the existence of a function that indexes the elements that are generating the open cover. (Contributed by Mario Carneiro, 14-Sep-2014)

	Ref	Expression
Hypotheses	iscmp.1	$⊢ X = ⋃ J$
	cmpcovf.2	$⊢ z = f (y) \to (φ \leftrightarrow ψ)$
Assertion	cmpcovf	$⊢ (J \in Comp \land \forall x \in X \exists y \in J (x \in y \land \exists z \in A φ)) \to \exists s \in (𝒫 J \cap Fin) (X = ⋃ s \land \exists f (f : s ⟶ A \land \forall y \in s ψ))$

Proof

Step	Hyp	Ref	Expression
1		iscmp.1	$⊢ X = ⋃ J$
2		cmpcovf.2	$⊢ z = f (y) \to (φ \leftrightarrow ψ)$
3		simpl	$⊢ (J \in Comp \land \forall x \in X \exists y \in J (x \in y \land \exists z \in A φ)) \to J \in Comp$
4	1	cmpcov2	$⊢ (J \in Comp \land \forall x \in X \exists y \in J (x \in y \land \exists z \in A φ)) \to \exists u \in (𝒫 J \cap Fin) (X = ⋃ u \land \forall y \in u \exists z \in A φ)$
5		elfpw	$⊢ u \in (𝒫 J \cap Fin) \leftrightarrow (u \subseteq J \land u \in Fin)$
6		simplrl	$⊢ ((J \in Comp \land (u \subseteq J \land u \in Fin)) \land (X = ⋃ u \land \forall y \in u \exists z \in A φ)) \to u \subseteq J$
7		velpw	$⊢ u \in 𝒫 J \leftrightarrow u \subseteq J$
8	6 7	sylibr	$⊢ ((J \in Comp \land (u \subseteq J \land u \in Fin)) \land (X = ⋃ u \land \forall y \in u \exists z \in A φ)) \to u \in 𝒫 J$
9		simplrr	$⊢ ((J \in Comp \land (u \subseteq J \land u \in Fin)) \land (X = ⋃ u \land \forall y \in u \exists z \in A φ)) \to u \in Fin$
10	8 9	elind	$⊢ ((J \in Comp \land (u \subseteq J \land u \in Fin)) \land (X = ⋃ u \land \forall y \in u \exists z \in A φ)) \to u \in (𝒫 J \cap Fin)$
11		simprl	$⊢ ((J \in Comp \land (u \subseteq J \land u \in Fin)) \land (X = ⋃ u \land \forall y \in u \exists z \in A φ)) \to X = ⋃ u$
12		simprr	$⊢ ((J \in Comp \land (u \subseteq J \land u \in Fin)) \land (X = ⋃ u \land \forall y \in u \exists z \in A φ)) \to \forall y \in u \exists z \in A φ$
13	2	ac6sfi	$⊢ (u \in Fin \land \forall y \in u \exists z \in A φ) \to \exists f (f : u ⟶ A \land \forall y \in u ψ)$
14	9 12 13	syl2anc	$⊢ ((J \in Comp \land (u \subseteq J \land u \in Fin)) \land (X = ⋃ u \land \forall y \in u \exists z \in A φ)) \to \exists f (f : u ⟶ A \land \forall y \in u ψ)$
15		unieq	$⊢ s = u \to ⋃ s = ⋃ u$
16	15	eqeq2d	$⊢ s = u \to (X = ⋃ s \leftrightarrow X = ⋃ u)$
17		feq2	$⊢ s = u \to (f : s ⟶ A \leftrightarrow f : u ⟶ A)$
18		raleq	$⊢ s = u \to (\forall y \in s ψ \leftrightarrow \forall y \in u ψ)$
19	17 18	anbi12d	$⊢ s = u \to ((f : s ⟶ A \land \forall y \in s ψ) \leftrightarrow (f : u ⟶ A \land \forall y \in u ψ))$
20	19	exbidv	$⊢ s = u \to (\exists f (f : s ⟶ A \land \forall y \in s ψ) \leftrightarrow \exists f (f : u ⟶ A \land \forall y \in u ψ))$
21	16 20	anbi12d	$⊢ s = u \to ((X = ⋃ s \land \exists f (f : s ⟶ A \land \forall y \in s ψ)) \leftrightarrow (X = ⋃ u \land \exists f (f : u ⟶ A \land \forall y \in u ψ)))$
22	21	rspcev	$⊢ (u \in (𝒫 J \cap Fin) \land (X = ⋃ u \land \exists f (f : u ⟶ A \land \forall y \in u ψ))) \to \exists s \in (𝒫 J \cap Fin) (X = ⋃ s \land \exists f (f : s ⟶ A \land \forall y \in s ψ))$
23	10 11 14 22	syl12anc	$⊢ ((J \in Comp \land (u \subseteq J \land u \in Fin)) \land (X = ⋃ u \land \forall y \in u \exists z \in A φ)) \to \exists s \in (𝒫 J \cap Fin) (X = ⋃ s \land \exists f (f : s ⟶ A \land \forall y \in s ψ))$
24	23	ex	$⊢ (J \in Comp \land (u \subseteq J \land u \in Fin)) \to ((X = ⋃ u \land \forall y \in u \exists z \in A φ) \to \exists s \in (𝒫 J \cap Fin) (X = ⋃ s \land \exists f (f : s ⟶ A \land \forall y \in s ψ)))$
25	5 24	sylan2b	$⊢ (J \in Comp \land u \in (𝒫 J \cap Fin)) \to ((X = ⋃ u \land \forall y \in u \exists z \in A φ) \to \exists s \in (𝒫 J \cap Fin) (X = ⋃ s \land \exists f (f : s ⟶ A \land \forall y \in s ψ)))$
26	25	rexlimdva	$⊢ J \in Comp \to (\exists u \in (𝒫 J \cap Fin) (X = ⋃ u \land \forall y \in u \exists z \in A φ) \to \exists s \in (𝒫 J \cap Fin) (X = ⋃ s \land \exists f (f : s ⟶ A \land \forall y \in s ψ)))$
27	3 4 26	sylc	$⊢ (J \in Comp \land \forall x \in X \exists y \in J (x \in y \land \exists z \in A φ)) \to \exists s \in (𝒫 J \cap Fin) (X = ⋃ s \land \exists f (f : s ⟶ A \land \forall y \in s ψ))$

Metamath Proof Explorer

Theorem cmpcovf

Proof