cmpsublem

		Ref	Expression
	Hypothesis	cmpsub.1	$⊢ X = ⋃ J$
	Assertion	cmpsublem	$⊢ (J \in Top \land S \subseteq X) \to (\forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d) \to \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$

Proof

Step	Hyp	Ref	Expression
1		cmpsub.1	$⊢ X = ⋃ J$
2		rabexg	$⊢ J \in Top \to \{y \in J \| y \cap S \in s\} \in V$
3	2	ad2antrr	$⊢ ((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \to \{y \in J \| y \cap S \in s\} \in V$
4		ssrab2	$⊢ \{y \in J \| y \cap S \in s\} \subseteq J$
5		elpwg	$⊢ \{y \in J \| y \cap S \in s\} \in V \to (\{y \in J \| y \cap S \in s\} \in 𝒫 J \leftrightarrow \{y \in J \| y \cap S \in s\} \subseteq J)$
6	4 5	mpbiri	$⊢ \{y \in J \| y \cap S \in s\} \in V \to \{y \in J \| y \cap S \in s\} \in 𝒫 J$
7	3 6	syl	$⊢ ((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \to \{y \in J \| y \cap S \in s\} \in 𝒫 J$
8		unieq	$⊢ c = \{y \in J \| y \cap S \in s\} \to ⋃ c = ⋃ \{y \in J \| y \cap S \in s\}$
9	8	sseq2d	$⊢ c = \{y \in J \| y \cap S \in s\} \to (S \subseteq ⋃ c \leftrightarrow S \subseteq ⋃ \{y \in J \| y \cap S \in s\})$
10		pweq	$⊢ c = \{y \in J \| y \cap S \in s\} \to 𝒫 c = 𝒫 \{y \in J \| y \cap S \in s\}$
11	10	ineq1d	$⊢ c = \{y \in J \| y \cap S \in s\} \to 𝒫 c \cap Fin = 𝒫 \{y \in J \| y \cap S \in s\} \cap Fin$
12	11	rexeqdv	$⊢ c = \{y \in J \| y \cap S \in s\} \to (\exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d \leftrightarrow \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d)$
13	9 12	imbi12d	$⊢ c = \{y \in J \| y \cap S \in s\} \to ((S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d) \leftrightarrow (S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d))$
14	13	rspcva	$⊢ (\{y \in J \| y \cap S \in s\} \in 𝒫 J \land \forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d)) \to (S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d)$
15	7 14	sylan	$⊢ (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land \forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d)) \to (S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d)$
16	15	ex	$⊢ ((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \to (\forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d) \to (S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d))$
17	1	restuni	$⊢ (J \in Top \land S \subseteq X) \to S = ⋃ (J ↾_{𝑡} S)$
18	17	adantr	$⊢ ((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \to S = ⋃ (J ↾_{𝑡} S)$
19	18	eqeq1d	$⊢ ((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \to (S = ⋃ s \leftrightarrow ⋃ (J ↾_{𝑡} S) = ⋃ s)$
20		velpw	$⊢ s \in 𝒫 (J ↾_{𝑡} S) \leftrightarrow s \subseteq J ↾_{𝑡} S$
21		eleq2	$⊢ S = ⋃ s \to (t \in S \leftrightarrow t \in ⋃ s)$
22		eluni	$⊢ t \in ⋃ s \leftrightarrow \exists u (t \in u \land u \in s)$
23	21 22	bitrdi	$⊢ S = ⋃ s \to (t \in S \leftrightarrow \exists u (t \in u \land u \in s))$
24	23	adantl	$⊢ (((J \in Top \land S \subseteq X) \land s \subseteq J ↾_{𝑡} S) \land S = ⋃ s) \to (t \in S \leftrightarrow \exists u (t \in u \land u \in s))$
25		ssel	$⊢ s \subseteq J ↾_{𝑡} S \to (u \in s \to u \in (J ↾_{𝑡} S))$
26	1	sseq2i	$⊢ S \subseteq X \leftrightarrow S \subseteq ⋃ J$
27		uniexg	$⊢ J \in Top \to ⋃ J \in V$
28		ssexg	$⊢ (S \subseteq ⋃ J \land ⋃ J \in V) \to S \in V$
29	28	ancoms	$⊢ (⋃ J \in V \land S \subseteq ⋃ J) \to S \in V$
30	27 29	sylan	$⊢ (J \in Top \land S \subseteq ⋃ J) \to S \in V$
31	26 30	sylan2b	$⊢ (J \in Top \land S \subseteq X) \to S \in V$
32		elrest	$⊢ (J \in Top \land S \in V) \to (u \in (J ↾_{𝑡} S) \leftrightarrow \exists w \in J u = w \cap S)$
33	31 32	syldan	$⊢ (J \in Top \land S \subseteq X) \to (u \in (J ↾_{𝑡} S) \leftrightarrow \exists w \in J u = w \cap S)$
34		inss1	$⊢ w \cap S \subseteq w$
35		sseq1	$⊢ u = w \cap S \to (u \subseteq w \leftrightarrow w \cap S \subseteq w)$
36	34 35	mpbiri	$⊢ u = w \cap S \to u \subseteq w$
37	36	sselda	$⊢ (u = w \cap S \land t \in u) \to t \in w$
38	37	3ad2antl3	$⊢ (((J \in Top \land S \subseteq X) \land w \in J \land u = w \cap S) \land t \in u) \to t \in w$
39	38	3adant2	$⊢ (((J \in Top \land S \subseteq X) \land w \in J \land u = w \cap S) \land u \in s \land t \in u) \to t \in w$
40		ineq1	$⊢ y = w \to y \cap S = w \cap S$
41	40	eleq1d	$⊢ y = w \to (y \cap S \in s \leftrightarrow w \cap S \in s)$
42		simp12	$⊢ (((J \in Top \land S \subseteq X) \land w \in J \land u = w \cap S) \land u \in s \land t \in u) \to w \in J$
43		eleq1	$⊢ u = w \cap S \to (u \in s \leftrightarrow w \cap S \in s)$
44	43	biimpa	$⊢ (u = w \cap S \land u \in s) \to w \cap S \in s$
45	44	3ad2antl3	$⊢ (((J \in Top \land S \subseteq X) \land w \in J \land u = w \cap S) \land u \in s) \to w \cap S \in s$
46	45	3adant3	$⊢ (((J \in Top \land S \subseteq X) \land w \in J \land u = w \cap S) \land u \in s \land t \in u) \to w \cap S \in s$
47	41 42 46	elrabd	$⊢ (((J \in Top \land S \subseteq X) \land w \in J \land u = w \cap S) \land u \in s \land t \in u) \to w \in \{y \in J \| y \cap S \in s\}$
48		vex	$⊢ w \in V$
49		eleq2	$⊢ v = w \to (t \in v \leftrightarrow t \in w)$
50		eleq1	$⊢ v = w \to (v \in \{y \in J \| y \cap S \in s\} \leftrightarrow w \in \{y \in J \| y \cap S \in s\})$
51	49 50	anbi12d	$⊢ v = w \to ((t \in v \land v \in \{y \in J \| y \cap S \in s\}) \leftrightarrow (t \in w \land w \in \{y \in J \| y \cap S \in s\}))$
52	48 51	spcev	$⊢ (t \in w \land w \in \{y \in J \| y \cap S \in s\}) \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\})$
53	39 47 52	syl2anc	$⊢ (((J \in Top \land S \subseteq X) \land w \in J \land u = w \cap S) \land u \in s \land t \in u) \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\})$
54	53	3exp	$⊢ ((J \in Top \land S \subseteq X) \land w \in J \land u = w \cap S) \to (u \in s \to (t \in u \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\})))$
55	54	rexlimdv3a	$⊢ (J \in Top \land S \subseteq X) \to (\exists w \in J u = w \cap S \to (u \in s \to (t \in u \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))))$
56	33 55	sylbid	$⊢ (J \in Top \land S \subseteq X) \to (u \in (J ↾_{𝑡} S) \to (u \in s \to (t \in u \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))))$
57	56	com23	$⊢ (J \in Top \land S \subseteq X) \to (u \in s \to (u \in (J ↾_{𝑡} S) \to (t \in u \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))))$
58	57	com4l	$⊢ u \in s \to (u \in (J ↾_{𝑡} S) \to (t \in u \to ((J \in Top \land S \subseteq X) \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))))$
59	25 58	sylcom	$⊢ s \subseteq J ↾_{𝑡} S \to (u \in s \to (t \in u \to ((J \in Top \land S \subseteq X) \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))))$
60	59	com24	$⊢ s \subseteq J ↾_{𝑡} S \to ((J \in Top \land S \subseteq X) \to (t \in u \to (u \in s \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))))$
61	60	impcom	$⊢ ((J \in Top \land S \subseteq X) \land s \subseteq J ↾_{𝑡} S) \to (t \in u \to (u \in s \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\})))$
62	61	impd	$⊢ ((J \in Top \land S \subseteq X) \land s \subseteq J ↾_{𝑡} S) \to ((t \in u \land u \in s) \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))$
63	62	exlimdv	$⊢ ((J \in Top \land S \subseteq X) \land s \subseteq J ↾_{𝑡} S) \to (\exists u (t \in u \land u \in s) \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))$
64	63	adantr	$⊢ (((J \in Top \land S \subseteq X) \land s \subseteq J ↾_{𝑡} S) \land S = ⋃ s) \to (\exists u (t \in u \land u \in s) \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))$
65	24 64	sylbid	$⊢ (((J \in Top \land S \subseteq X) \land s \subseteq J ↾_{𝑡} S) \land S = ⋃ s) \to (t \in S \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))$
66	65	ex	$⊢ ((J \in Top \land S \subseteq X) \land s \subseteq J ↾_{𝑡} S) \to (S = ⋃ s \to (t \in S \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\})))$
67	20 66	sylan2b	$⊢ ((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \to (S = ⋃ s \to (t \in S \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\})))$
68	67	imp	$⊢ (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to (t \in S \to \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\}))$
69		eluni	$⊢ t \in ⋃ \{y \in J \| y \cap S \in s\} \leftrightarrow \exists v (t \in v \land v \in \{y \in J \| y \cap S \in s\})$
70	68 69	imbitrrdi	$⊢ (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to (t \in S \to t \in ⋃ \{y \in J \| y \cap S \in s\})$
71	70	ssrdv	$⊢ (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to S \subseteq ⋃ \{y \in J \| y \cap S \in s\}$
72		pm2.27	$⊢ S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to ((S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d) \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d)$
73		elin	$⊢ d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) \leftrightarrow (d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin)$
74		vex	$⊢ t \in V$
75		eqeq1	$⊢ x = t \to (x = z \cap S \leftrightarrow t = z \cap S)$
76	75	rexbidv	$⊢ x = t \to (\exists z \in d x = z \cap S \leftrightarrow \exists z \in d t = z \cap S)$
77	74 76	elab	$⊢ t \in \{x \| \exists z \in d x = z \cap S\} \leftrightarrow \exists z \in d t = z \cap S$
78		velpw	$⊢ d \in 𝒫 \{y \in J \| y \cap S \in s\} \leftrightarrow d \subseteq \{y \in J \| y \cap S \in s\}$
79		ssel	$⊢ d \subseteq \{y \in J \| y \cap S \in s\} \to (z \in d \to z \in \{y \in J \| y \cap S \in s\})$
80		ineq1	$⊢ y = z \to y \cap S = z \cap S$
81	80	eleq1d	$⊢ y = z \to (y \cap S \in s \leftrightarrow z \cap S \in s)$
82	81	elrab	$⊢ z \in \{y \in J \| y \cap S \in s\} \leftrightarrow (z \in J \land z \cap S \in s)$
83		eleq1a	$⊢ z \cap S \in s \to (t = z \cap S \to t \in s)$
84	82 83	simplbiim	$⊢ z \in \{y \in J \| y \cap S \in s\} \to (t = z \cap S \to t \in s)$
85	79 84	syl6	$⊢ d \subseteq \{y \in J \| y \cap S \in s\} \to (z \in d \to (t = z \cap S \to t \in s))$
86	85	2a1d	$⊢ d \subseteq \{y \in J \| y \cap S \in s\} \to (S \subseteq ⋃ d \to ((((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to (z \in d \to (t = z \cap S \to t \in s))))$
87	86	adantr	$⊢ (d \subseteq \{y \in J \| y \cap S \in s\} \land d \in Fin) \to (S \subseteq ⋃ d \to ((((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to (z \in d \to (t = z \cap S \to t \in s))))$
88	78 87	sylanb	$⊢ (d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \to (S \subseteq ⋃ d \to ((((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to (z \in d \to (t = z \cap S \to t \in s))))$
89	88	3imp	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to (z \in d \to (t = z \cap S \to t \in s))$
90	89	rexlimdv	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to (\exists z \in d t = z \cap S \to t \in s)$
91	77 90	biimtrid	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to (t \in \{x \| \exists z \in d x = z \cap S\} \to t \in s)$
92	91	ssrdv	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to \{x \| \exists z \in d x = z \cap S\} \subseteq s$
93		vex	$⊢ d \in V$
94	93	abrexex	$⊢ \{x \| \exists z \in d x = z \cap S\} \in V$
95	94	elpw	$⊢ \{x \| \exists z \in d x = z \cap S\} \in 𝒫 s \leftrightarrow \{x \| \exists z \in d x = z \cap S\} \subseteq s$
96	92 95	sylibr	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to \{x \| \exists z \in d x = z \cap S\} \in 𝒫 s$
97		abrexfi	$⊢ d \in Fin \to \{x \| \exists z \in d x = z \cap S\} \in Fin$
98	97	ad2antlr	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d) \to \{x \| \exists z \in d x = z \cap S\} \in Fin$
99	98	3adant3	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to \{x \| \exists z \in d x = z \cap S\} \in Fin$
100	96 99	elind	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to \{x \| \exists z \in d x = z \cap S\} \in (𝒫 s \cap Fin)$
101		dfss	$⊢ S \subseteq ⋃ d \leftrightarrow S = S \cap ⋃ d$
102	101	biimpi	$⊢ S \subseteq ⋃ d \to S = S \cap ⋃ d$
103		uniiun	$⊢ ⋃ d = ⋃_{z \in d} z$
104	103	ineq2i	$⊢ S \cap ⋃ d = S \cap ⋃_{z \in d} z$
105		iunin2	$⊢ ⋃_{z \in d} (S \cap z) = S \cap ⋃_{z \in d} z$
106		incom	$⊢ S \cap z = z \cap S$
107	106	a1i	$⊢ z \in d \to S \cap z = z \cap S$
108	107	iuneq2i	$⊢ ⋃_{z \in d} (S \cap z) = ⋃_{z \in d} (z \cap S)$
109	104 105 108	3eqtr2i	$⊢ S \cap ⋃ d = ⋃_{z \in d} (z \cap S)$
110	102 109	eqtrdi	$⊢ S \subseteq ⋃ d \to S = ⋃_{z \in d} (z \cap S)$
111	110	3ad2ant2	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to S = ⋃_{z \in d} (z \cap S)$
112	18	ad2antrl	$⊢ (S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to S = ⋃ (J ↾_{𝑡} S)$
113	112	3adant1	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to S = ⋃ (J ↾_{𝑡} S)$
114		vex	$⊢ z \in V$
115	114	inex1	$⊢ z \cap S \in V$
116	115	dfiun2	$⊢ ⋃_{z \in d} (z \cap S) = ⋃ \{x \| \exists z \in d x = z \cap S\}$
117	116	a1i	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to ⋃_{z \in d} (z \cap S) = ⋃ \{x \| \exists z \in d x = z \cap S\}$
118	111 113 117	3eqtr3d	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to ⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists z \in d x = z \cap S\}$
119		unieq	$⊢ t = \{x \| \exists z \in d x = z \cap S\} \to ⋃ t = ⋃ \{x \| \exists z \in d x = z \cap S\}$
120	119	rspceeqv	$⊢ (\{x \| \exists z \in d x = z \cap S\} \in (𝒫 s \cap Fin) \land ⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists z \in d x = z \cap S\}) \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t$
121	100 118 120	syl2anc	$⊢ ((d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \land S \subseteq ⋃ d \land (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s)) \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t$
122	121	3exp	$⊢ (d \in 𝒫 \{y \in J \| y \cap S \in s\} \land d \in Fin) \to (S \subseteq ⋃ d \to ((((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
123	73 122	sylbi	$⊢ d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) \to (S \subseteq ⋃ d \to ((((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
124	123	rexlimiv	$⊢ \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d \to ((((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)$
125	72 124	syl6	$⊢ S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to ((S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d) \to ((((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
126	125	com3r	$⊢ (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to (S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to ((S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d) \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
127	71 126	mpd	$⊢ (((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \land S = ⋃ s) \to ((S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d) \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)$
128	127	ex	$⊢ ((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \to (S = ⋃ s \to ((S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d) \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
129	19 128	sylbird	$⊢ ((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \to (⋃ (J ↾_{𝑡} S) = ⋃ s \to ((S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d) \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
130	129	com23	$⊢ ((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \to ((S \subseteq ⋃ \{y \in J \| y \cap S \in s\} \to \exists d \in (𝒫 \{y \in J \| y \cap S \in s\} \cap Fin) S \subseteq ⋃ d) \to (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
131	16 130	syld	$⊢ ((J \in Top \land S \subseteq X) \land s \in 𝒫 (J ↾_{𝑡} S)) \to (\forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d) \to (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
132	131	ralrimdva	$⊢ (J \in Top \land S \subseteq X) \to (\forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d) \to \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$

Metamath Proof Explorer

Theorem cmpsublem

Proof