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 23364

Description: Lemma for cmpsub 23365. (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 5278	. . . . . . 7 ⊢ (𝐽 ∈ Top → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V)
2	1	ad2antrr 727	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V)
3		ssrab2 4020	. . . . . . 7 ⊢ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ⊆ 𝐽
4		elpwg 4544	. . . . . . 7 ⊢ ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V → ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽 ↔ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ⊆ 𝐽))
5	3, 4	mpbiri 258	. . . . . 6 ⊢ ({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ V → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽)
6	2, 5	syl 17	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽)
7		unieq 4861	. . . . . . . 8 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∪ 𝑐 = ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
8	7	sseq2d 3954	. . . . . . 7 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑆 ⊆ ∪ 𝑐 ↔ 𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
9		pweq 4555	. . . . . . . . 9 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → 𝒫 𝑐 = 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
10	9	ineq1d 4159	. . . . . . . 8 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝒫 𝑐 ∩ Fin) = (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin))
11	10	rexeqdv 3296	. . . . . . 7 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑 ↔ ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
12	8, 11	imbi12d 344	. . . . . 6 ⊢ (𝑐 = {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) ↔ (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
13	12	rspcva 3562	. . . . 5 ⊢ (({𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∈ 𝒫 𝐽 ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
14	6, 13	sylan 581	. . . 4 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
15	14	ex 412	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
16		cmpsub.1	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
17	16	restuni 23127	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
18	17	adantr 480	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
19	18	eqeq1d 2738	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (𝑆 = ∪ 𝑠 ↔ ∪ (𝐽 ↾_t 𝑆) = ∪ 𝑠))
20		velpw 4546	. . . . . . . . . . 11 ⊢ (𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆) ↔ 𝑠 ⊆ (𝐽 ↾_t 𝑆))
21		eleq2 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 ↔ 𝑡 ∈ ∪ 𝑠))
22		eluni 4853	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ∪ 𝑠 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠))
23	21, 22	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠)))
24	23	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ⊆ (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 ↔ ∃𝑢(𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠)))
25		ssel 3915	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ⊆ (𝐽 ↾_t 𝑆) → (𝑢 ∈ 𝑠 → 𝑢 ∈ (𝐽 ↾_t 𝑆)))
26	16	sseq2i 3951	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽)
27		uniexg 7694	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
28		ssexg 5264	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ∈ V) → 𝑆 ∈ V)
29	28	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∪ 𝐽 ∈ V ∧ 𝑆 ⊆ ∪ 𝐽) → 𝑆 ∈ V)
30	27, 29	sylan 581	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → 𝑆 ∈ V)
31	26, 30	sylan2b 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V)
32		elrest 17390	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑢 ∈ (𝐽 ↾_t 𝑆) ↔ ∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆)))
33	31, 32	syldan 592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑢 ∈ (𝐽 ↾_t 𝑆) ↔ ∃𝑤 ∈ 𝐽 𝑢 = (𝑤 ∩ 𝑆)))
34		inss1 4177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∩ 𝑆) ⊆ 𝑤
35		sseq1 3947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ⊆ 𝑤 ↔ (𝑤 ∩ 𝑆) ⊆ 𝑤))
36	34, 35	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = (𝑤 ∩ 𝑆) → 𝑢 ⊆ 𝑤)
37	36	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑢 = (𝑤 ∩ 𝑆) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤)
38	37	3ad2antl3 1189	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤)
39	38	3adant2 1132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ 𝑤)
40		ineq1 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑤 → (𝑦 ∩ 𝑆) = (𝑤 ∩ 𝑆))
41	40	eleq1d 2821	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑤 → ((𝑦 ∩ 𝑆) ∈ 𝑠 ↔ (𝑤 ∩ 𝑆) ∈ 𝑠))
42		simp12 1206	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑤 ∈ 𝐽)
43		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (𝑤 ∩ 𝑆) → (𝑢 ∈ 𝑠 ↔ (𝑤 ∩ 𝑆) ∈ 𝑠))
44	43	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 = (𝑤 ∩ 𝑆) ∧ 𝑢 ∈ 𝑠) → (𝑤 ∩ 𝑆) ∈ 𝑠)
45	44	3ad2antl3 1189	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠) → (𝑤 ∩ 𝑆) ∈ 𝑠)
46	45	3adant3 1133	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → (𝑤 ∩ 𝑆) ∈ 𝑠)
47	41, 42, 46	elrabd 3636	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
48		vex 3433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑤 ∈ V
49		eleq2 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → (𝑡 ∈ 𝑣 ↔ 𝑡 ∈ 𝑤))
50		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑣 = 𝑤 → (𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
51	49, 50	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑤 → ((𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) ↔ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
52	48, 51	spcev 3548	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
53	39, 47, 52	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢) → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
54	53	3exp 1120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = (𝑤 ∩ 𝑆)) → (𝑢 ∈ 𝑠 → (𝑡 ∈ 𝑢 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))
55	54	rexlimdv3a 3142	. . . . . . . . . . . . . . . . . . . . . 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 1935	. . . . . . . . . . . . . 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 595	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) → (𝑆 = ∪ 𝑠 → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))))
68	67	imp 406	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})))
69		eluni 4853	. . . . . . . . 9 ⊢ (𝑡 ∈ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ ∃𝑣(𝑡 ∈ 𝑣 ∧ 𝑣 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
70	68, 69	imbitrrdi 252	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑡 ∈ 𝑆 → 𝑡 ∈ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
71	70	ssrdv 3927	. . . . . . 7 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → 𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
72		pm2.27 42	. . . . . . . . 9 ⊢ (𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ((𝑆 ⊆ ∪ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∃𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin)𝑆 ⊆ ∪ 𝑑))
73		elin 3905	. . . . . . . . . . 11 ⊢ (𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin) ↔ (𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin))
74		vex 3433	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑡 ∈ V
75		eqeq1 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑧 ∩ 𝑆) ↔ 𝑡 = (𝑧 ∩ 𝑆)))
76	75	rexbidv 3161	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑡 → (∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆) ↔ ∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆)))
77	74, 76	elab 3622	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ↔ ∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆))
78		velpw 4546	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ 𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠})
79		ssel 3915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 ⊆ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} → (𝑧 ∈ 𝑑 → 𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠}))
80		ineq1 4153	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑧 → (𝑦 ∩ 𝑆) = (𝑧 ∩ 𝑆))
81	80	eleq1d 2821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑧 → ((𝑦 ∩ 𝑆) ∈ 𝑠 ↔ (𝑧 ∩ 𝑆) ∈ 𝑠))
82	81	elrab 3634	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ↔ (𝑧 ∈ 𝐽 ∧ (𝑧 ∩ 𝑆) ∈ 𝑠))
83		eleq1a 2831	. . . . . . . . . . . . . . . . . . . . . . . 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 582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))))
89	88	3imp 1111	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (𝑧 ∈ 𝑑 → (𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠)))
90	89	rexlimdv 3136	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (∃𝑧 ∈ 𝑑 𝑡 = (𝑧 ∩ 𝑆) → 𝑡 ∈ 𝑠))
91	77, 90	biimtrid 242	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → (𝑡 ∈ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} → 𝑡 ∈ 𝑠))
92	91	ssrdv 3927	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ⊆ 𝑠)
93		vex 3433	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
94	93	abrexex 7915	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ V
95	94	elpw 4545	. . . . . . . . . . . . . . 15 ⊢ ({𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ 𝒫 𝑠 ↔ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ⊆ 𝑠)
96	92, 95	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ 𝒫 𝑠)
97		abrexfi 9262	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ Fin → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin)
98	97	ad2antlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin)
99	98	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ Fin)
100	96, 99	elind 4140	. . . . . . . . . . . . 13 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ (𝒫 𝑠 ∩ Fin))
101		dfss 3908	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 = (𝑆 ∩ ∪ 𝑑))
102	101	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ ∪ 𝑑 → 𝑆 = (𝑆 ∩ ∪ 𝑑))
103		uniiun 5001	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑑 = ∪ 𝑧 ∈ 𝑑 𝑧
104	103	ineq2i 4157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∩ ∪ 𝑑) = (𝑆 ∩ ∪ 𝑧 ∈ 𝑑 𝑧)
105		iunin2 5013	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑧 ∈ 𝑑 (𝑆 ∩ 𝑧) = (𝑆 ∩ ∪ 𝑧 ∈ 𝑑 𝑧)
106		incom 4149	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∩ 𝑧) = (𝑧 ∩ 𝑆)
107	106	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑑 → (𝑆 ∩ 𝑧) = (𝑧 ∩ 𝑆))
108	107	iuneq2i 4955	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑧 ∈ 𝑑 (𝑆 ∩ 𝑧) = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆)
109	104, 105, 108	3eqtr2i 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∩ ∪ 𝑑) = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆)
110	102, 109	eqtrdi 2787	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ ∪ 𝑑 → 𝑆 = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆))
111	110	3ad2ant2 1135	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆))
112	18	ad2antrl 729	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
113	112	3adant1 1131	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → 𝑆 = ∪ (𝐽 ↾_t 𝑆))
114		vex 3433	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
115	114	inex1 5258	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∩ 𝑆) ∈ V
116	115	dfiun2 4974	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)}
117	116	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∪ 𝑧 ∈ 𝑑 (𝑧 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)})
118	111, 113, 117	3eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∪ (𝐽 ↾_t 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)})
119		unieq 4861	. . . . . . . . . . . . . 14 ⊢ (𝑡 = {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} → ∪ 𝑡 = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)})
120	119	rspceeqv 3587	. . . . . . . . . . . . 13 ⊢ (({𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)} ∈ (𝒫 𝑠 ∩ Fin) ∧ ∪ (𝐽 ↾_t 𝑆) = ∪ {𝑥 ∣ ∃𝑧 ∈ 𝑑 𝑥 = (𝑧 ∩ 𝑆)}) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)
121	100, 118, 120	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠)) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)
122	121	3exp 1120	. . . . . . . . . . 11 ⊢ ((𝑑 ∈ 𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∧ 𝑑 ∈ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
123	73, 122	sylbi 217	. . . . . . . . . 10 ⊢ (𝑑 ∈ (𝒫 {𝑦 ∈ 𝐽 ∣ (𝑦 ∩ 𝑆) ∈ 𝑠} ∩ Fin) → (𝑆 ⊆ ∪ 𝑑 → ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)) ∧ 𝑆 = ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))
124	123	rexlimiv 3131	. . . . . . . . 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 3137	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾_t 𝑆)(∪ (𝐽 ↾_t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾_t 𝑆) = ∪ 𝑡)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 {cab 2714 ∀wral 3051 ∃wrex 3061 {crab 3389 Vcvv 3429 ∩ cin 3888 ⊆ wss 3889 𝒫 cpw 4541 ∪ cuni 4850 ∪ ciun 4933 (class class class)co 7367 Fincfn 8893 ↾_t crest 17383 Topctop 22858

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-1o 8405 df-en 8894 df-dom 8895 df-fin 8897 df-fi 9324 df-rest 17385 df-topgen 17406 df-top 22859 df-topon 22876 df-bases 22911

This theorem is referenced by: cmpsub 23365

W3C validator