cmpcov2

Description: Rewrite cmpcov for the cover { y e. J | ph } . (Contributed by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Hypothesis	iscmp.1	$⊢ X = ⋃ J$
	Assertion	cmpcov2	$⊢ (J \in Comp \land \forall x \in X \exists y \in J (x \in y \land φ)) \to \exists s \in (𝒫 J \cap Fin) (X = ⋃ s \land \forall y \in s φ)$

Proof

Step	Hyp	Ref	Expression
1		iscmp.1	$⊢ X = ⋃ J$
2		dfss3	$⊢ X \subseteq ⋃ \{y \in J \| φ\} \leftrightarrow \forall x \in X x \in ⋃ \{y \in J \| φ\}$
3		elunirab	$⊢ x \in ⋃ \{y \in J \| φ\} \leftrightarrow \exists y \in J (x \in y \land φ)$
4	3	ralbii	$⊢ \forall x \in X x \in ⋃ \{y \in J \| φ\} \leftrightarrow \forall x \in X \exists y \in J (x \in y \land φ)$
5	2 4	sylbbr	$⊢ \forall x \in X \exists y \in J (x \in y \land φ) \to X \subseteq ⋃ \{y \in J \| φ\}$
6		ssrab2	$⊢ \{y \in J \| φ\} \subseteq J$
7	6	unissi	$⊢ ⋃ \{y \in J \| φ\} \subseteq ⋃ J$
8	7 1	sseqtrri	$⊢ ⋃ \{y \in J \| φ\} \subseteq X$
9	8	a1i	$⊢ \forall x \in X \exists y \in J (x \in y \land φ) \to ⋃ \{y \in J \| φ\} \subseteq X$
10	5 9	eqssd	$⊢ \forall x \in X \exists y \in J (x \in y \land φ) \to X = ⋃ \{y \in J \| φ\}$
11	1	cmpcov	$⊢ (J \in Comp \land \{y \in J \| φ\} \subseteq J \land X = ⋃ \{y \in J \| φ\}) \to \exists s \in (𝒫 \{y \in J \| φ\} \cap Fin) X = ⋃ s$
12	6 11	mp3an2	$⊢ (J \in Comp \land X = ⋃ \{y \in J \| φ\}) \to \exists s \in (𝒫 \{y \in J \| φ\} \cap Fin) X = ⋃ s$
13	10 12	sylan2	$⊢ (J \in Comp \land \forall x \in X \exists y \in J (x \in y \land φ)) \to \exists s \in (𝒫 \{y \in J \| φ\} \cap Fin) X = ⋃ s$
14		ssrab	$⊢ s \subseteq \{y \in J \| φ\} \leftrightarrow (s \subseteq J \land \forall y \in s φ)$
15	14	anbi1i	$⊢ (s \subseteq \{y \in J \| φ\} \land X = ⋃ s) \leftrightarrow ((s \subseteq J \land \forall y \in s φ) \land X = ⋃ s)$
16		an32	$⊢ ((s \subseteq J \land \forall y \in s φ) \land X = ⋃ s) \leftrightarrow ((s \subseteq J \land X = ⋃ s) \land \forall y \in s φ)$
17		anass	$⊢ ((s \subseteq J \land X = ⋃ s) \land \forall y \in s φ) \leftrightarrow (s \subseteq J \land (X = ⋃ s \land \forall y \in s φ))$
18	15 16 17	3bitri	$⊢ (s \subseteq \{y \in J \| φ\} \land X = ⋃ s) \leftrightarrow (s \subseteq J \land (X = ⋃ s \land \forall y \in s φ))$
19	18	anbi1i	$⊢ ((s \subseteq \{y \in J \| φ\} \land X = ⋃ s) \land s \in Fin) \leftrightarrow ((s \subseteq J \land (X = ⋃ s \land \forall y \in s φ)) \land s \in Fin)$
20		an32	$⊢ ((s \subseteq \{y \in J \| φ\} \land s \in Fin) \land X = ⋃ s) \leftrightarrow ((s \subseteq \{y \in J \| φ\} \land X = ⋃ s) \land s \in Fin)$
21		an32	$⊢ ((s \subseteq J \land s \in Fin) \land (X = ⋃ s \land \forall y \in s φ)) \leftrightarrow ((s \subseteq J \land (X = ⋃ s \land \forall y \in s φ)) \land s \in Fin)$
22	19 20 21	3bitr4i	$⊢ ((s \subseteq \{y \in J \| φ\} \land s \in Fin) \land X = ⋃ s) \leftrightarrow ((s \subseteq J \land s \in Fin) \land (X = ⋃ s \land \forall y \in s φ))$
23		elfpw	$⊢ s \in (𝒫 \{y \in J \| φ\} \cap Fin) \leftrightarrow (s \subseteq \{y \in J \| φ\} \land s \in Fin)$
24	23	anbi1i	$⊢ (s \in (𝒫 \{y \in J \| φ\} \cap Fin) \land X = ⋃ s) \leftrightarrow ((s \subseteq \{y \in J \| φ\} \land s \in Fin) \land X = ⋃ s)$
25		elfpw	$⊢ s \in (𝒫 J \cap Fin) \leftrightarrow (s \subseteq J \land s \in Fin)$
26	25	anbi1i	$⊢ (s \in (𝒫 J \cap Fin) \land (X = ⋃ s \land \forall y \in s φ)) \leftrightarrow ((s \subseteq J \land s \in Fin) \land (X = ⋃ s \land \forall y \in s φ))$
27	22 24 26	3bitr4i	$⊢ (s \in (𝒫 \{y \in J \| φ\} \cap Fin) \land X = ⋃ s) \leftrightarrow (s \in (𝒫 J \cap Fin) \land (X = ⋃ s \land \forall y \in s φ))$
28	27	rexbii2	$⊢ \exists s \in (𝒫 \{y \in J \| φ\} \cap Fin) X = ⋃ s \leftrightarrow \exists s \in (𝒫 J \cap Fin) (X = ⋃ s \land \forall y \in s φ)$
29	13 28	sylib	$⊢ (J \in Comp \land \forall x \in X \exists y \in J (x \in y \land φ)) \to \exists s \in (𝒫 J \cap Fin) (X = ⋃ s \land \forall y \in s φ)$

Metamath Proof Explorer

Theorem cmpcov2

Proof