cmpsublem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cmpsublem		Structured version Visualization version GIF version

Theorem cmpsublem 23347

Description: Lemma for cmpsub 23348. (Contributed by Jeff Hankins, 28-Jun-2009.)

**Hypothesis**
Ref	Expression
cmpsub.1	⊢ 𝑋 = ∪ 𝐽

**Assertion**
Ref	Expression
cmpsublem	⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)(∪ (𝐽 ↾_t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))

Distinct variable groups: 𝑐,𝑑,𝑠,𝑡,𝐽 𝑆,𝑐,𝑑,𝑠,𝑡 𝑋,𝑐,𝑑,𝑠,𝑡

Proof of Theorem cmpsublem Dummy variables 𝑥 𝑦 𝑢 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabexg 5334	. . . . . . 7 ⊢ (𝐽 ∈ Top → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V)
2	1	ad2antrr 724	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V)
3		ssrab2 4073	. . . . . . 7 ⊢ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ⊆ 𝐽
4		elpwg 4607	. . . . . . 7 ⊢ ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V → ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽 ↔ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ⊆ 𝐽))
5	3, 4	mpbiri 257	. . . . . 6 ⊢ ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽)
6	2, 5	syl 17	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽)
7		unieq 4920	. . . . . . . 8 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∪ 𝑐 = ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
8	7	sseq2d 4009	. . . . . . 7 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑆 ⊆ ∪ 𝑐 ↔ 𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
9		pweq 4618	. . . . . . . . 9 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → 𝒫 𝑐 = 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
10	9	ineq1d 4209	. . . . . . . 8 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝒫 𝑐 ∩ Fin) = (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin))
11	10	rexeqdv 3315	. . . . . . 7 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑 ↔ ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
12	8, 11	imbi12d 343	. . . . . 6 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) ↔ (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
13	12	rspcva 3604	. . . . 5 ⊢ (({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽 ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
14	6, 13	sylan 578	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
15	14	ex 411	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
16		cmpsub.1	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
17	16	restuni 23110	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
18	17	adantr 479	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
19	18	eqeq1d 2727	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (𝑆 = ∪ 𝑠 ↔ ∪ (𝐽 ↾_t 𝑆) = ∪ 𝑠))
20		velpw 4609	. . . . . . . . . . 11 ⊢ (𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆) ↔ 𝑠 ⊆ (𝐽 ↾_t 𝑆))
21		eleq2 2814	. . . . . . . . . . . . . . 15 ⊢ (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 ↔ 𝑡 ∈ ∪ 𝑠))
22		eluni 4912	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ∪ 𝑠 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠))
23	21, 22	bitrdi 286	. . . . . . . . . . . . . 14 ⊢ (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠)))
24	23	adantl 480	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠)))
25		ssel 3970	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ⊆ (𝐽 ↾_t 𝑆) → (𝑢 ∈ 𝑠 → 𝑢 ∈ (𝐽 ↾_t 𝑆)))
26	16	sseq2i 4006	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽)
27		uniexg 7746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
28		ssexg 5324	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ∈ V) → 𝑆 ∈ V)
29	28	ancoms 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∪ 𝐽 ∈ V ∧ 𝑆 ⊆ ∪ 𝐽) → 𝑆 ∈ V)
30	27, 29	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → 𝑆 ∈ V)
31	26, 30	sylan2b 592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V)
32		elrest 17412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑢 ∈ (𝐽 ↾_t 𝑆) ↔ ∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆)))
33	31, 32	syldan 589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑢 ∈ (𝐽 ↾_t 𝑆) ↔ ∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆)))
34		inss1 4227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∩ 𝑆) ⊆ 𝑤
35		sseq1 4002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ⊆ 𝑤 ↔ (𝑤 ∩ 𝑆) ⊆ 𝑤))
36	34, 35	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = (𝑤 ∩ 𝑆) → 𝑢 ⊆ 𝑤)
37	36	sselda 3976	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑢 = (𝑤 ∩ 𝑆) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤)
38	37	3ad2antl3 1184	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤)
39	38	3adant2 1128	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤)
40		ineq1 4203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑤 → (𝑦 ∩ 𝑆) = (𝑤 ∩ 𝑆))
41	40	eleq1d 2810	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑤 → ((𝑦 ∩ 𝑆) ∈ 𝑠 ↔ (𝑤 ∩ 𝑆) ∈ 𝑠))
42		simp12 1201	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑤 ∈ 𝐽)
43		eleq1 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ∈ 𝑠 ↔ (𝑤 ∩ 𝑆) ∈ 𝑠))
44	43	biimpa 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 = (𝑤 ∩ 𝑆) ∧ 𝑢 ∈ 𝑠) → (𝑤 ∩ 𝑆) ∈ 𝑠)
45	44	3ad2antl3 1184	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠) → (𝑤 ∩ 𝑆) ∈ 𝑠)
46	45	3adant3 1129	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → (𝑤 ∩ 𝑆) ∈ 𝑠)
47	41, 42, 46	elrabd 3681	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
48		vex 3465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑤 ∈ V
49		eleq2 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → (𝑡 ∈ 𝑣 ↔ 𝑡 ∈ 𝑤))
50		eleq1 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → (𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
51	49, 50	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑤 → ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) ↔ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
52	48, 51	spcev 3590	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
53	39, 47, 52	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
54	53	3exp 1116	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))
55	54	rexlimdv3a 3148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))))
56	33, 55	sylbid 239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑢 ∈ (𝐽 ↾_t 𝑆) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))))
57	56	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑢 ∈ 𝑠 → (𝑢 ∈ (𝐽 ↾_t 𝑆) → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))))
58	57	com4l 92	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ 𝑠 → (𝑢 ∈ (𝐽 ↾_t 𝑆) → (𝑡 ∈ 𝑢 → ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))))
59	25, 58	sylcom 30	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ⊆ (𝐽 ↾_t 𝑆) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))))
60	59	com24 95	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ⊆ (𝐽 ↾_t 𝑆) → ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑡 ∈ 𝑢 → (𝑢 ∈ 𝑠 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))))
61	60	impcom 406	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) → (𝑡 ∈ 𝑢 → (𝑢 ∈ 𝑠 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))
62	61	impd 409	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) → ((𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
63	62	exlimdv 1928	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) → (∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
64	63	adantr 479	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
65	24, 64	sylbid 239	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
66	65	ex 411	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) → (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))
67	20, 66	sylan2b 592	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))
68	67	imp 405	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
69		eluni 4912	. . . . . . . . 9 ⊢ (𝑡 ∈ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
70	68, 69	imbitrrdi 251	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → 𝑡 ∈ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
71	70	ssrdv 3982	. . . . . . 7 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → 𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
72		pm2.27 42	. . . . . . . . 9 ⊢ (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
73		elin 3960	. . . . . . . . . . 11 ⊢ (𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin) ↔ (𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin))
74		vex 3465	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑡 ∈ V
75		eqeq1 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑧 ∩ 𝑆) ↔ 𝑡 = (𝑧 ∩ 𝑆)))
76	75	rexbidv 3168	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → (∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆) ↔ ∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆)))
77	74, 76	elab 3664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ↔ ∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆))
78		velpw 4609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ 𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
79		ssel 3970	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑧 ∈ 𝑑 → 𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
80		ineq1 4203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑧 → (𝑦 ∩ 𝑆) = (𝑧 ∩ 𝑆))
81	80	eleq1d 2810	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → ((𝑦 ∩ 𝑆) ∈ 𝑠 ↔ (𝑧 ∩ 𝑆) ∈ 𝑠))
82	81	elrab 3679	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ (𝑧 ∈ 𝐽 ∧ (𝑧 ∩ 𝑆) ∈ 𝑠))
83		eleq1a 2820	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∩ 𝑆) ∈ 𝑠 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))
84	82, 83	simplbiim 503	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))
85	79, 84	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))
86	85	2a1d 26	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))))
87	86	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))))
88	78, 87	sylanb 579	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))))
89	88	3imp 1108	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))
90	89	rexlimdv 3142	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))
91	77, 90	biimtrid 241	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (𝑡 ∈ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} → 𝑡 ∈ 𝑠))
92	91	ssrdv 3982	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ⊆ 𝑠)
93		vex 3465	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
94	93	abrexex 7967	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ V
95	94	elpw 4608	. . . . . . . . . . . . . . 15 ⊢ ({𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ 𝒫 𝑠 ↔ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ⊆ 𝑠)
96	92, 95	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ 𝒫 𝑠)
97		abrexfi 9378	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ Fin → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin)
98	97	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin)
99	98	3adant3 1129	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin)
100	96, 99	elind 4192	. . . . . . . . . . . . 13 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ (𝒫 𝑠 ∩ Fin))
101		dfss 3963	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 = (𝑆 ∩ ∪ 𝑑))
102	101	biimpi 215	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ ∪ 𝑑 → 𝑆 = (𝑆 ∩ ∪ 𝑑))
103		uniiun 5062	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑑 = ∪ 𝑧 ∈ 𝑑 𝑧
104	103	ineq2i 4207	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ ∪ 𝑑) = (𝑆 ∩ ∪ 𝑧 ∈ 𝑑 𝑧)
105		iunin2 5075	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑧 ∈ 𝑑 (𝑆 ∩ 𝑧) = (𝑆 ∩ ∪ 𝑧 ∈ 𝑑 𝑧)
106		incom 4199	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∩ 𝑧) = (𝑧 ∩ 𝑆)
107	106	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑑 → (𝑆 ∩ 𝑧) = (𝑧 ∩ 𝑆))
108	107	iuneq2i 5018	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑧 ∈ 𝑑 (𝑆 ∩ 𝑧) = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆)
109	104, 105, 108	3eqtr2i 2759	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∩ ∪ 𝑑) = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆)
110	102, 109	eqtrdi 2781	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ ∪ 𝑑 → 𝑆 = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆))
111	110	3ad2ant2 1131	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆))
112	18	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
113	112	3adant1 1127	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
114		vex 3465	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
115	114	inex1 5318	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∩ 𝑆) ∈ V
116	115	dfiun2 5037	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)}
117	116	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)})
118	111, 113, 117	3eqtr3d 2773	. . . . . . . . . . . . 13 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∪ (𝐽 ↾_t 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)})
119		unieq 4920	. . . . . . . . . . . . . 14 ⊢ (𝑡 = {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} → ∪ 𝑡 = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)})
120	119	rspceeqv 3628	. . . . . . . . . . . . 13 ⊢ (({𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ (𝒫 𝑠 ∩ Fin) ∧ ∪ (𝐽 ↾_t 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)}) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)
121	100, 118, 120	syl2anc 582	. . . . . . . . . . . 12 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)
122	121	3exp 1116	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
123	73, 122	sylbi 216	. . . . . . . . . 10 ⊢ (𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
124	123	rexlimiv 3137	. . . . . . . . 9 ⊢ (∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡))
125	72, 124	syl6 35	. . . . . . . 8 ⊢ (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
126	125	com3r 87	. . . . . . 7 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
127	71, 126	mpd 15	. . . . . 6 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡))
128	127	ex 411	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (𝑆 = ∪ 𝑠 → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
129	19, 128	sylbird 259	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (∪ (𝐽 ↾_t 𝑆) = ∪ 𝑠 → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
130	129	com23 86	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → (∪ (𝐽 ↾_t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
131	15, 130	syld 47	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → (∪ (𝐽 ↾_t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
132	131	ralrimdva 3143	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)(∪ (𝐽 ↾_t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∃wex 1773 ∈ wcel 2098 {cab 2702 ∀wral 3050 ∃wrex 3059 {crab 3418 Vcvv 3461 ∩ cin 3943 ⊆ wss 3944 𝒫 cpw 4604 ∪ cuni 4909 ∪ ciun 4997 (class class class)co 7419 Fincfn 8964 ↾_t crest 17405 Topctop 22839

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-int 4951 df-iun 4999 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-ord 6374 df-on 6375 df-lim 6376 df-suc 6377 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7872 df-1st 7994 df-2nd 7995 df-1o 8487 df-er 8725 df-en 8965 df-dom 8966 df-fin 8968 df-fi 9436 df-rest 17407 df-topgen 17428 df-top 22840 df-topon 22857 df-bases 22893

This theorem is referenced by: cmpsub 23348

W3C validator