txcmplem2

	Ref	Expression
Hypotheses	txcmp.x	$⊢ X = ⋃ R$
	txcmp.y	$⊢ Y = ⋃ S$
	txcmp.r	$⊢ φ \to R \in Comp$
	txcmp.s	$⊢ φ \to S \in Comp$
	txcmp.w	$⊢ φ \to W \subseteq R \times_{t} S$
	txcmp.u	$⊢ φ \to X \times Y = ⋃ W$
Assertion	txcmplem2	$⊢ φ \to \exists v \in (𝒫 W \cap Fin) X \times Y = ⋃ v$

Proof

Step	Hyp	Ref	Expression
1		txcmp.x	$⊢ X = ⋃ R$
2		txcmp.y	$⊢ Y = ⋃ S$
3		txcmp.r	$⊢ φ \to R \in Comp$
4		txcmp.s	$⊢ φ \to S \in Comp$
5		txcmp.w	$⊢ φ \to W \subseteq R \times_{t} S$
6		txcmp.u	$⊢ φ \to X \times Y = ⋃ W$
7	3	adantr	$⊢ (φ \land x \in Y) \to R \in Comp$
8	4	adantr	$⊢ (φ \land x \in Y) \to S \in Comp$
9	5	adantr	$⊢ (φ \land x \in Y) \to W \subseteq R \times_{t} S$
10	6	adantr	$⊢ (φ \land x \in Y) \to X \times Y = ⋃ W$
11		simpr	$⊢ (φ \land x \in Y) \to x \in Y$
12	1 2 7 8 9 10 11	txcmplem1	$⊢ (φ \land x \in Y) \to \exists u \in S (x \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v)$
13	12	ralrimiva	$⊢ φ \to \forall x \in Y \exists u \in S (x \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v)$
14		unieq	$⊢ v = f (u) \to ⋃ v = ⋃ f (u)$
15	14	sseq2d	$⊢ v = f (u) \to (X \times u \subseteq ⋃ v \leftrightarrow X \times u \subseteq ⋃ f (u))$
16	2 15	cmpcovf	$⊢ (S \in Comp \land \forall x \in Y \exists u \in S (x \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v)) \to \exists w \in (𝒫 S \cap Fin) (Y = ⋃ w \land \exists f (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))$
17	4 13 16	syl2anc	$⊢ φ \to \exists w \in (𝒫 S \cap Fin) (Y = ⋃ w \land \exists f (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))$
18		simprrl	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to f : w ⟶ 𝒫 W \cap Fin$
19		ffn	$⊢ f : w ⟶ 𝒫 W \cap Fin \to f Fn w$
20		fniunfv	$⊢ f Fn w \to ⋃_{z \in w} f (z) = ⋃ ran f$
21	18 19 20	3syl	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to ⋃_{z \in w} f (z) = ⋃ ran f$
22	18	frnd	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to ran f \subseteq 𝒫 W \cap Fin$
23		inss1	$⊢ 𝒫 W \cap Fin \subseteq 𝒫 W$
24	22 23	sstrdi	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to ran f \subseteq 𝒫 W$
25		sspwuni	$⊢ ran f \subseteq 𝒫 W \leftrightarrow ⋃ ran f \subseteq W$
26	24 25	sylib	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to ⋃ ran f \subseteq W$
27	21 26	eqsstrd	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to ⋃_{z \in w} f (z) \subseteq W$
28		vex	$⊢ w \in V$
29		fvex	$⊢ f (z) \in V$
30	28 29	iunex	$⊢ ⋃_{z \in w} f (z) \in V$
31	30	elpw	$⊢ ⋃_{z \in w} f (z) \in 𝒫 W \leftrightarrow ⋃_{z \in w} f (z) \subseteq W$
32	27 31	sylibr	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to ⋃_{z \in w} f (z) \in 𝒫 W$
33		inss2	$⊢ 𝒫 S \cap Fin \subseteq Fin$
34		simplr	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to w \in (𝒫 S \cap Fin)$
35	33 34	sselid	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to w \in Fin$
36		inss2	$⊢ 𝒫 W \cap Fin \subseteq Fin$
37		fss	$⊢ (f : w ⟶ 𝒫 W \cap Fin \land 𝒫 W \cap Fin \subseteq Fin) \to f : w ⟶ Fin$
38	18 36 37	sylancl	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to f : w ⟶ Fin$
39		ffvelcdm	$⊢ (f : w ⟶ Fin \land z \in w) \to f (z) \in Fin$
40	39	ralrimiva	$⊢ f : w ⟶ Fin \to \forall z \in w f (z) \in Fin$
41	38 40	syl	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to \forall z \in w f (z) \in Fin$
42		iunfi	$⊢ (w \in Fin \land \forall z \in w f (z) \in Fin) \to ⋃_{z \in w} f (z) \in Fin$
43	35 41 42	syl2anc	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to ⋃_{z \in w} f (z) \in Fin$
44	32 43	elind	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to ⋃_{z \in w} f (z) \in (𝒫 W \cap Fin)$
45		simprl	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to Y = ⋃ w$
46		uniiun	$⊢ ⋃ w = ⋃_{z \in w} z$
47	45 46	eqtrdi	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to Y = ⋃_{z \in w} z$
48	47	xpeq2d	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to X \times Y = X \times ⋃_{z \in w} z$
49		xpiundi	$⊢ X \times ⋃_{z \in w} z = ⋃_{z \in w} (X \times z)$
50	48 49	eqtrdi	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to X \times Y = ⋃_{z \in w} (X \times z)$
51		simprrr	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to \forall u \in w X \times u \subseteq ⋃ f (u)$
52		xpeq2	$⊢ u = z \to X \times u = X \times z$
53		fveq2	$⊢ u = z \to f (u) = f (z)$
54	53	unieqd	$⊢ u = z \to ⋃ f (u) = ⋃ f (z)$
55	52 54	sseq12d	$⊢ u = z \to (X \times u \subseteq ⋃ f (u) \leftrightarrow X \times z \subseteq ⋃ f (z))$
56	55	cbvralvw	$⊢ \forall u \in w X \times u \subseteq ⋃ f (u) \leftrightarrow \forall z \in w X \times z \subseteq ⋃ f (z)$
57	51 56	sylib	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to \forall z \in w X \times z \subseteq ⋃ f (z)$
58		ss2iun	$⊢ \forall z \in w X \times z \subseteq ⋃ f (z) \to ⋃_{z \in w} (X \times z) \subseteq ⋃_{z \in w} ⋃ f (z)$
59	57 58	syl	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to ⋃_{z \in w} (X \times z) \subseteq ⋃_{z \in w} ⋃ f (z)$
60	50 59	eqsstrd	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to X \times Y \subseteq ⋃_{z \in w} ⋃ f (z)$
61	18	ffvelcdmda	$⊢ (((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \land z \in w) \to f (z) \in (𝒫 W \cap Fin)$
62	23 61	sselid	$⊢ (((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \land z \in w) \to f (z) \in 𝒫 W$
63		elpwi	$⊢ f (z) \in 𝒫 W \to f (z) \subseteq W$
64		uniss	$⊢ f (z) \subseteq W \to ⋃ f (z) \subseteq ⋃ W$
65	62 63 64	3syl	$⊢ (((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \land z \in w) \to ⋃ f (z) \subseteq ⋃ W$
66	6	ad3antrrr	$⊢ (((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \land z \in w) \to X \times Y = ⋃ W$
67	65 66	sseqtrrd	$⊢ (((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \land z \in w) \to ⋃ f (z) \subseteq X \times Y$
68	67	ralrimiva	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to \forall z \in w ⋃ f (z) \subseteq X \times Y$
69		iunss	$⊢ ⋃_{z \in w} ⋃ f (z) \subseteq X \times Y \leftrightarrow \forall z \in w ⋃ f (z) \subseteq X \times Y$
70	68 69	sylibr	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to ⋃_{z \in w} ⋃ f (z) \subseteq X \times Y$
71	60 70	eqssd	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to X \times Y = ⋃_{z \in w} ⋃ f (z)$
72		iuncom4	$⊢ ⋃_{z \in w} ⋃ f (z) = ⋃ ⋃_{z \in w} f (z)$
73	71 72	eqtrdi	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to X \times Y = ⋃ ⋃_{z \in w} f (z)$
74		unieq	$⊢ v = ⋃_{z \in w} f (z) \to ⋃ v = ⋃ ⋃_{z \in w} f (z)$
75	74	rspceeqv	$⊢ (⋃_{z \in w} f (z) \in (𝒫 W \cap Fin) \land X \times Y = ⋃ ⋃_{z \in w} f (z)) \to \exists v \in (𝒫 W \cap Fin) X \times Y = ⋃ v$
76	44 73 75	syl2anc	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land (Y = ⋃ w \land (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)))) \to \exists v \in (𝒫 W \cap Fin) X \times Y = ⋃ v$
77	76	expr	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land Y = ⋃ w) \to ((f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)) \to \exists v \in (𝒫 W \cap Fin) X \times Y = ⋃ v)$
78	77	exlimdv	$⊢ ((φ \land w \in (𝒫 S \cap Fin)) \land Y = ⋃ w) \to (\exists f (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u)) \to \exists v \in (𝒫 W \cap Fin) X \times Y = ⋃ v)$
79	78	expimpd	$⊢ (φ \land w \in (𝒫 S \cap Fin)) \to ((Y = ⋃ w \land \exists f (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u))) \to \exists v \in (𝒫 W \cap Fin) X \times Y = ⋃ v)$
80	79	rexlimdva	$⊢ φ \to (\exists w \in (𝒫 S \cap Fin) (Y = ⋃ w \land \exists f (f : w ⟶ 𝒫 W \cap Fin \land \forall u \in w X \times u \subseteq ⋃ f (u))) \to \exists v \in (𝒫 W \cap Fin) X \times Y = ⋃ v)$
81	17 80	mpd	$⊢ φ \to \exists v \in (𝒫 W \cap Fin) X \times Y = ⋃ v$

Metamath Proof Explorer

Theorem txcmplem2

Proof