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 23293

Description: Lemma for cmpsub 23294. (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 5295	. . . . . . 7 ⊢ (𝐽 ∈ Top → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V)
2	1	ad2antrr 726	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V)
3		ssrab2 4046	. . . . . . 7 ⊢ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ⊆ 𝐽
4		elpwg 4569	. . . . . . 7 ⊢ ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V → ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽 ↔ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ⊆ 𝐽))
5	3, 4	mpbiri 258	. . . . . 6 ⊢ ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽)
6	2, 5	syl 17	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽)
7		unieq 4885	. . . . . . . 8 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∪ 𝑐 = ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
8	7	sseq2d 3982	. . . . . . 7 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑆 ⊆ ∪ 𝑐 ↔ 𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
9		pweq 4580	. . . . . . . . 9 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → 𝒫 𝑐 = 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
10	9	ineq1d 4185	. . . . . . . 8 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝒫 𝑐 ∩ Fin) = (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin))
11	10	rexeqdv 3302	. . . . . . 7 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑 ↔ ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
12	8, 11	imbi12d 344	. . . . . 6 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) ↔ (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
13	12	rspcva 3589	. . . . 5 ⊢ (({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽 ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
14	6, 13	sylan 580	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
15	14	ex 412	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
16		cmpsub.1	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
17	16	restuni 23056	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
18	17	adantr 480	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
19	18	eqeq1d 2732	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (𝑆 = ∪ 𝑠 ↔ ∪ (𝐽 ↾_t 𝑆) = ∪ 𝑠))
20		velpw 4571	. . . . . . . . . . 11 ⊢ (𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆) ↔ 𝑠 ⊆ (𝐽 ↾_t 𝑆))
21		eleq2 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 ↔ 𝑡 ∈ ∪ 𝑠))
22		eluni 4877	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ∪ 𝑠 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠))
23	21, 22	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠)))
24	23	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠)))
25		ssel 3943	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ⊆ (𝐽 ↾_t 𝑆) → (𝑢 ∈ 𝑠 → 𝑢 ∈ (𝐽 ↾_t 𝑆)))
26	16	sseq2i 3979	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽)
27		uniexg 7719	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
28		ssexg 5281	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ∈ V) → 𝑆 ∈ V)
29	28	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∪ 𝐽 ∈ V ∧ 𝑆 ⊆ ∪ 𝐽) → 𝑆 ∈ V)
30	27, 29	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → 𝑆 ∈ V)
31	26, 30	sylan2b 594	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V)
32		elrest 17397	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑢 ∈ (𝐽 ↾_t 𝑆) ↔ ∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆)))
33	31, 32	syldan 591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑢 ∈ (𝐽 ↾_t 𝑆) ↔ ∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆)))
34		inss1 4203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∩ 𝑆) ⊆ 𝑤
35		sseq1 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ⊆ 𝑤 ↔ (𝑤 ∩ 𝑆) ⊆ 𝑤))
36	34, 35	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = (𝑤 ∩ 𝑆) → 𝑢 ⊆ 𝑤)
37	36	sselda 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑢 = (𝑤 ∩ 𝑆) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤)
38	37	3ad2antl3 1188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤)
39	38	3adant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤)
40		ineq1 4179	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑤 → (𝑦 ∩ 𝑆) = (𝑤 ∩ 𝑆))
41	40	eleq1d 2814	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑤 → ((𝑦 ∩ 𝑆) ∈ 𝑠 ↔ (𝑤 ∩ 𝑆) ∈ 𝑠))
42		simp12 1205	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑤 ∈ 𝐽)
43		eleq1 2817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ∈ 𝑠 ↔ (𝑤 ∩ 𝑆) ∈ 𝑠))
44	43	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 = (𝑤 ∩ 𝑆) ∧ 𝑢 ∈ 𝑠) → (𝑤 ∩ 𝑆) ∈ 𝑠)
45	44	3ad2antl3 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠) → (𝑤 ∩ 𝑆) ∈ 𝑠)
46	45	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → (𝑤 ∩ 𝑆) ∈ 𝑠)
47	41, 42, 46	elrabd 3664	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
48		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑤 ∈ V
49		eleq2 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → (𝑡 ∈ 𝑣 ↔ 𝑡 ∈ 𝑤))
50		eleq1 2817	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → (𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
51	49, 50	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑤 → ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) ↔ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
52	48, 51	spcev 3575	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
53	39, 47, 52	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
54	53	3exp 1119	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))
55	54	rexlimdv3a 3139	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))))
56	33, 55	sylbid 240	. . . . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) → (𝑡 ∈ 𝑢 → (𝑢 ∈ 𝑠 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))
62	61	impd 410	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) → ((𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
63	62	exlimdv 1933	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) → (∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
64	63	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
65	24, 64	sylbid 240	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
66	65	ex 412	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) → (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))
67	20, 66	sylan2b 594	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))
68	67	imp 406	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
69		eluni 4877	. . . . . . . . 9 ⊢ (𝑡 ∈ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
70	68, 69	imbitrrdi 252	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → 𝑡 ∈ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
71	70	ssrdv 3955	. . . . . . 7 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → 𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
72		pm2.27 42	. . . . . . . . 9 ⊢ (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
73		elin 3933	. . . . . . . . . . 11 ⊢ (𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin) ↔ (𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin))
74		vex 3454	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑡 ∈ V
75		eqeq1 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑧 ∩ 𝑆) ↔ 𝑡 = (𝑧 ∩ 𝑆)))
76	75	rexbidv 3158	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → (∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆) ↔ ∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆)))
77	74, 76	elab 3649	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ↔ ∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆))
78		velpw 4571	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ 𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
79		ssel 3943	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑧 ∈ 𝑑 → 𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
80		ineq1 4179	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑧 → (𝑦 ∩ 𝑆) = (𝑧 ∩ 𝑆))
81	80	eleq1d 2814	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → ((𝑦 ∩ 𝑆) ∈ 𝑠 ↔ (𝑧 ∩ 𝑆) ∈ 𝑠))
82	81	elrab 3662	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ (𝑧 ∈ 𝐽 ∧ (𝑧 ∩ 𝑆) ∈ 𝑠))
83		eleq1a 2824	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∩ 𝑆) ∈ 𝑠 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))
84	82, 83	simplbiim 504	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))
85	79, 84	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))
86	85	2a1d 26	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))))
87	86	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))))
88	78, 87	sylanb 581	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))))
89	88	3imp 1110	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))
90	89	rexlimdv 3133	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))
91	77, 90	biimtrid 242	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (𝑡 ∈ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} → 𝑡 ∈ 𝑠))
92	91	ssrdv 3955	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ⊆ 𝑠)
93		vex 3454	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
94	93	abrexex 7944	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ V
95	94	elpw 4570	. . . . . . . . . . . . . . 15 ⊢ ({𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ 𝒫 𝑠 ↔ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ⊆ 𝑠)
96	92, 95	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ 𝒫 𝑠)
97		abrexfi 9310	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ Fin → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin)
98	97	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin)
99	98	3adant3 1132	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin)
100	96, 99	elind 4166	. . . . . . . . . . . . 13 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ (𝒫 𝑠 ∩ Fin))
101		dfss 3936	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 = (𝑆 ∩ ∪ 𝑑))
102	101	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ ∪ 𝑑 → 𝑆 = (𝑆 ∩ ∪ 𝑑))
103		uniiun 5025	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑑 = ∪ 𝑧 ∈ 𝑑 𝑧
104	103	ineq2i 4183	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ ∪ 𝑑) = (𝑆 ∩ ∪ 𝑧 ∈ 𝑑 𝑧)
105		iunin2 5038	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑧 ∈ 𝑑 (𝑆 ∩ 𝑧) = (𝑆 ∩ ∪ 𝑧 ∈ 𝑑 𝑧)
106		incom 4175	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∩ 𝑧) = (𝑧 ∩ 𝑆)
107	106	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑑 → (𝑆 ∩ 𝑧) = (𝑧 ∩ 𝑆))
108	107	iuneq2i 4980	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑧 ∈ 𝑑 (𝑆 ∩ 𝑧) = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆)
109	104, 105, 108	3eqtr2i 2759	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∩ ∪ 𝑑) = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆)
110	102, 109	eqtrdi 2781	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ ∪ 𝑑 → 𝑆 = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆))
111	110	3ad2ant2 1134	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆))
112	18	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
113	112	3adant1 1130	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
114		vex 3454	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
115	114	inex1 5275	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∩ 𝑆) ∈ V
116	115	dfiun2 5000	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)}
117	116	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)})
118	111, 113, 117	3eqtr3d 2773	. . . . . . . . . . . . 13 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∪ (𝐽 ↾_t 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)})
119		unieq 4885	. . . . . . . . . . . . . 14 ⊢ (𝑡 = {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} → ∪ 𝑡 = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)})
120	119	rspceeqv 3614	. . . . . . . . . . . . 13 ⊢ (({𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ (𝒫 𝑠 ∩ Fin) ∧ ∪ (𝐽 ↾_t 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)}) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)
121	100, 118, 120	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)
122	121	3exp 1119	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
123	73, 122	sylbi 217	. . . . . . . . . 10 ⊢ (𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
124	123	rexlimiv 3128	. . . . . . . . 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 412	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (𝑆 = ∪ 𝑠 → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
129	19, 128	sylbird 260	. . . 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 3134	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)(∪ (𝐽 ↾_t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2109 {cab 2708 ∀wral 3045 ∃wrex 3054 {crab 3408 Vcvv 3450 ∩ cin 3916 ⊆ wss 3917 𝒫 cpw 4566 ∪ cuni 4874 ∪ ciun 4958 (class class class)co 7390 Fincfn 8921 ↾_t crest 17390 Topctop 22787

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-1o 8437 df-en 8922 df-dom 8923 df-fin 8925 df-fi 9369 df-rest 17392 df-topgen 17413 df-top 22788 df-topon 22805 df-bases 22840

This theorem is referenced by: cmpsub 23294

W3C validator