txcmplem1

	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$
	txcmp.a	$⊢ φ \to A \in Y$
Assertion	txcmplem1	$⊢ φ \to \exists u \in S (A \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ 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		txcmp.a	$⊢ φ \to A \in Y$
8		id	$⊢ x \in X \to x \in X$
9		opelxpi	$⊢ (x \in X \land A \in Y) \to ⟨x, A⟩ \in (X \times Y)$
10	8 7 9	syl2anr	$⊢ (φ \land x \in X) \to ⟨x, A⟩ \in (X \times Y)$
11	6	adantr	$⊢ (φ \land x \in X) \to X \times Y = ⋃ W$
12	10 11	eleqtrd	$⊢ (φ \land x \in X) \to ⟨x, A⟩ \in ⋃ W$
13		eluni2	$⊢ ⟨x, A⟩ \in ⋃ W \leftrightarrow \exists k \in W ⟨x, A⟩ \in k$
14	12 13	sylib	$⊢ (φ \land x \in X) \to \exists k \in W ⟨x, A⟩ \in k$
15	5	adantr	$⊢ (φ \land x \in X) \to W \subseteq R \times_{t} S$
16	15	sselda	$⊢ ((φ \land x \in X) \land k \in W) \to k \in (R \times_{t} S)$
17		eltx	$⊢ (R \in Comp \land S \in Comp) \to (k \in (R \times_{t} S) \leftrightarrow \forall y \in k \exists r \in R \exists s \in S (y \in (r \times s) \land r \times s \subseteq k))$
18	3 4 17	syl2anc	$⊢ φ \to (k \in (R \times_{t} S) \leftrightarrow \forall y \in k \exists r \in R \exists s \in S (y \in (r \times s) \land r \times s \subseteq k))$
19	18	adantr	$⊢ (φ \land x \in X) \to (k \in (R \times_{t} S) \leftrightarrow \forall y \in k \exists r \in R \exists s \in S (y \in (r \times s) \land r \times s \subseteq k))$
20	19	biimpa	$⊢ ((φ \land x \in X) \land k \in (R \times_{t} S)) \to \forall y \in k \exists r \in R \exists s \in S (y \in (r \times s) \land r \times s \subseteq k)$
21	16 20	syldan	$⊢ ((φ \land x \in X) \land k \in W) \to \forall y \in k \exists r \in R \exists s \in S (y \in (r \times s) \land r \times s \subseteq k)$
22		eleq1	$⊢ y = ⟨x, A⟩ \to (y \in (r \times s) \leftrightarrow ⟨x, A⟩ \in (r \times s))$
23	22	anbi1d	$⊢ y = ⟨x, A⟩ \to ((y \in (r \times s) \land r \times s \subseteq k) \leftrightarrow (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k))$
24	23	2rexbidv	$⊢ y = ⟨x, A⟩ \to (\exists r \in R \exists s \in S (y \in (r \times s) \land r \times s \subseteq k) \leftrightarrow \exists r \in R \exists s \in S (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k))$
25	24	rspccv	$⊢ \forall y \in k \exists r \in R \exists s \in S (y \in (r \times s) \land r \times s \subseteq k) \to (⟨x, A⟩ \in k \to \exists r \in R \exists s \in S (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k))$
26	21 25	syl	$⊢ ((φ \land x \in X) \land k \in W) \to (⟨x, A⟩ \in k \to \exists r \in R \exists s \in S (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k))$
27		opelxp1	$⊢ ⟨x, A⟩ \in (r \times s) \to x \in r$
28	27	ad2antrl	$⊢ (((φ \land x \in X) \land k \in W) \land (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k)) \to x \in r$
29		opelxp2	$⊢ ⟨x, A⟩ \in (r \times s) \to A \in s$
30	29	ad2antrl	$⊢ (((φ \land x \in X) \land k \in W) \land (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k)) \to A \in s$
31	30	snssd	$⊢ (((φ \land x \in X) \land k \in W) \land (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k)) \to \{A\} \subseteq s$
32		xpss2	$⊢ \{A\} \subseteq s \to r \times \{A\} \subseteq r \times s$
33	31 32	syl	$⊢ (((φ \land x \in X) \land k \in W) \land (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k)) \to r \times \{A\} \subseteq r \times s$
34		simprr	$⊢ (((φ \land x \in X) \land k \in W) \land (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k)) \to r \times s \subseteq k$
35	33 34	sstrd	$⊢ (((φ \land x \in X) \land k \in W) \land (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k)) \to r \times \{A\} \subseteq k$
36	28 35	jca	$⊢ (((φ \land x \in X) \land k \in W) \land (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k)) \to (x \in r \land r \times \{A\} \subseteq k)$
37	36	ex	$⊢ ((φ \land x \in X) \land k \in W) \to ((⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k) \to (x \in r \land r \times \{A\} \subseteq k))$
38	37	rexlimdvw	$⊢ ((φ \land x \in X) \land k \in W) \to (\exists s \in S (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k) \to (x \in r \land r \times \{A\} \subseteq k))$
39	38	reximdv	$⊢ ((φ \land x \in X) \land k \in W) \to (\exists r \in R \exists s \in S (⟨x, A⟩ \in (r \times s) \land r \times s \subseteq k) \to \exists r \in R (x \in r \land r \times \{A\} \subseteq k))$
40	26 39	syld	$⊢ ((φ \land x \in X) \land k \in W) \to (⟨x, A⟩ \in k \to \exists r \in R (x \in r \land r \times \{A\} \subseteq k))$
41	40	reximdva	$⊢ (φ \land x \in X) \to (\exists k \in W ⟨x, A⟩ \in k \to \exists k \in W \exists r \in R (x \in r \land r \times \{A\} \subseteq k))$
42	14 41	mpd	$⊢ (φ \land x \in X) \to \exists k \in W \exists r \in R (x \in r \land r \times \{A\} \subseteq k)$
43		rexcom	$⊢ \exists k \in W \exists r \in R (x \in r \land r \times \{A\} \subseteq k) \leftrightarrow \exists r \in R \exists k \in W (x \in r \land r \times \{A\} \subseteq k)$
44		r19.42v	$⊢ \exists k \in W (x \in r \land r \times \{A\} \subseteq k) \leftrightarrow (x \in r \land \exists k \in W r \times \{A\} \subseteq k)$
45	44	rexbii	$⊢ \exists r \in R \exists k \in W (x \in r \land r \times \{A\} \subseteq k) \leftrightarrow \exists r \in R (x \in r \land \exists k \in W r \times \{A\} \subseteq k)$
46	43 45	bitri	$⊢ \exists k \in W \exists r \in R (x \in r \land r \times \{A\} \subseteq k) \leftrightarrow \exists r \in R (x \in r \land \exists k \in W r \times \{A\} \subseteq k)$
47	42 46	sylib	$⊢ (φ \land x \in X) \to \exists r \in R (x \in r \land \exists k \in W r \times \{A\} \subseteq k)$
48	47	ralrimiva	$⊢ φ \to \forall x \in X \exists r \in R (x \in r \land \exists k \in W r \times \{A\} \subseteq k)$
49		sseq2	$⊢ k = f (r) \to (r \times \{A\} \subseteq k \leftrightarrow r \times \{A\} \subseteq f (r))$
50	1 49	cmpcovf	$⊢ (R \in Comp \land \forall x \in X \exists r \in R (x \in r \land \exists k \in W r \times \{A\} \subseteq k)) \to \exists t \in (𝒫 R \cap Fin) (X = ⋃ t \land \exists f (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))$
51	3 48 50	syl2anc	$⊢ φ \to \exists t \in (𝒫 R \cap Fin) (X = ⋃ t \land \exists f (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))$
52	3	ad2antrr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to R \in Comp$
53		cmptop	$⊢ S \in Comp \to S \in Top$
54	4 53	syl	$⊢ φ \to S \in Top$
55	54	ad2antrr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to S \in Top$
56		cmptop	$⊢ R \in Comp \to R \in Top$
57	52 56	syl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to R \in Top$
58		txtop	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S \in Top$
59	57 55 58	syl2anc	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to R \times_{t} S \in Top$
60		simprrl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to f : t ⟶ W$
61	60	frnd	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to ran f \subseteq W$
62	5	ad2antrr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to W \subseteq R \times_{t} S$
63	61 62	sstrd	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to ran f \subseteq R \times_{t} S$
64		uniopn	$⊢ (R \times_{t} S \in Top \land ran f \subseteq R \times_{t} S) \to ⋃ ran f \in (R \times_{t} S)$
65	59 63 64	syl2anc	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to ⋃ ran f \in (R \times_{t} S)$
66		simprrr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to \forall r \in t r \times \{A\} \subseteq f (r)$
67		ss2iun	$⊢ \forall r \in t r \times \{A\} \subseteq f (r) \to ⋃_{r \in t} (r \times \{A\}) \subseteq ⋃_{r \in t} f (r)$
68	66 67	syl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to ⋃_{r \in t} (r \times \{A\}) \subseteq ⋃_{r \in t} f (r)$
69		simprl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to X = ⋃ t$
70		uniiun	$⊢ ⋃ t = ⋃_{r \in t} r$
71	69 70	eqtrdi	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to X = ⋃_{r \in t} r$
72	71	xpeq1d	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to X \times \{A\} = ⋃_{r \in t} r \times \{A\}$
73		xpiundir	$⊢ ⋃_{r \in t} r \times \{A\} = ⋃_{r \in t} (r \times \{A\})$
74	72 73	eqtr2di	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to ⋃_{r \in t} (r \times \{A\}) = X \times \{A\}$
75	60	ffnd	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to f Fn t$
76		fniunfv	$⊢ f Fn t \to ⋃_{r \in t} f (r) = ⋃ ran f$
77	75 76	syl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to ⋃_{r \in t} f (r) = ⋃ ran f$
78	68 74 77	3sstr3d	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to X \times \{A\} \subseteq ⋃ ran f$
79	7	ad2antrr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to A \in Y$
80	1 2 52 55 65 78 79	txtube	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to \exists u \in S (A \in u \land X \times u \subseteq ⋃ ran f)$
81		vex	$⊢ f \in V$
82	81	rnex	$⊢ ran f \in V$
83	82	elpw	$⊢ ran f \in 𝒫 W \leftrightarrow ran f \subseteq W$
84	61 83	sylibr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to ran f \in 𝒫 W$
85		simplr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to t \in (𝒫 R \cap Fin)$
86	85	elin2d	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to t \in Fin$
87		dffn4	$⊢ f Fn t \leftrightarrow f : t \underset{onto}{⟶} ran f$
88	75 87	sylib	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to f : t \underset{onto}{⟶} ran f$
89		fofi	$⊢ (t \in Fin \land f : t \underset{onto}{⟶} ran f) \to ran f \in Fin$
90	86 88 89	syl2anc	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to ran f \in Fin$
91	84 90	elind	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to ran f \in (𝒫 W \cap Fin)$
92		unieq	$⊢ v = ran f \to ⋃ v = ⋃ ran f$
93	92	sseq2d	$⊢ v = ran f \to (X \times u \subseteq ⋃ v \leftrightarrow X \times u \subseteq ⋃ ran f)$
94	93	rspcev	$⊢ (ran f \in (𝒫 W \cap Fin) \land X \times u \subseteq ⋃ ran f) \to \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v$
95	94	ex	$⊢ ran f \in (𝒫 W \cap Fin) \to (X \times u \subseteq ⋃ ran f \to \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v)$
96	91 95	syl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to (X \times u \subseteq ⋃ ran f \to \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v)$
97	96	anim2d	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to ((A \in u \land X \times u \subseteq ⋃ ran f) \to (A \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v))$
98	97	reximdv	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to (\exists u \in S (A \in u \land X \times u \subseteq ⋃ ran f) \to \exists u \in S (A \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v))$
99	80 98	mpd	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)))) \to \exists u \in S (A \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v)$
100	99	expr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land X = ⋃ t) \to ((f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)) \to \exists u \in S (A \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v))$
101	100	exlimdv	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land X = ⋃ t) \to (\exists f (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r)) \to \exists u \in S (A \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v))$
102	101	expimpd	$⊢ (φ \land t \in (𝒫 R \cap Fin)) \to ((X = ⋃ t \land \exists f (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r))) \to \exists u \in S (A \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v))$
103	102	rexlimdva	$⊢ φ \to (\exists t \in (𝒫 R \cap Fin) (X = ⋃ t \land \exists f (f : t ⟶ W \land \forall r \in t r \times \{A\} \subseteq f (r))) \to \exists u \in S (A \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v))$
104	51 103	mpd	$⊢ φ \to \exists u \in S (A \in u \land \exists v \in (𝒫 W \cap Fin) X \times u \subseteq ⋃ v)$

Metamath Proof Explorer

Theorem txcmplem1

Proof