Theorem cmpsub 22005

Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman's Beginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)

Hypothesis

Ref	Expression
cmpsub.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
cmpsub	⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))

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

Proof of Theorem cmpsub

Dummy variables 𝑥 𝑦 𝑓 𝑠 𝑡 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2798	. . . 4 ⊢ ∪ (𝐽 ↾t 𝑆) = ∪ (𝐽 ↾t 𝑆)
2	1	iscmp 21993	. . 3 ⊢ ((𝐽 ↾t 𝑆) ∈ Comp ↔ ((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
3		id 22	. . . . . 6 ⊢ (𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋)
4		cmpsub.1	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐽
5	4	topopn 21511	. . . . . 6 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
6		ssexg 5191	. . . . . 6 ⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑆 ∈ V)
7	3, 5, 6	syl2anr 599	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V)
8		resttop 21765	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽 ↾t 𝑆) ∈ Top)
9	7, 8	syldan 594	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐽 ↾t 𝑆) ∈ Top)
10		ibar 532	. . . . 5 ⊢ ((𝐽 ↾t 𝑆) ∈ Top → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) ↔ ((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))))
11	10	bicomd 226	. . . 4 ⊢ ((𝐽 ↾t 𝑆) ∈ Top → (((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
12	9, 11	syl 17	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
13	2, 12	syl5bb 286	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
14		vex 3444	. . . . . . . . . . 11 ⊢ 𝑡 ∈ V
15		eqeq1 2802	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑦 ∩ 𝑆) ↔ 𝑡 = (𝑦 ∩ 𝑆)))
16	15	rexbidv 3256	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆) ↔ ∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆)))
17	14, 16	elab 3615	. . . . . . . . . 10 ⊢ (𝑡 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆))
18		velpw 4502	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽)
19		ssel2 3910	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐) → 𝑦 ∈ 𝐽)
20		ineq1 4131	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑦 → (𝑑 ∩ 𝑆) = (𝑦 ∩ 𝑆))
21	20	rspceeqv 3586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝐽 ∧ 𝑡 = (𝑦 ∩ 𝑆)) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))
22	21	ex 416	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐽 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
23	19, 22	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐) → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
24	23	ex 416	. . . . . . . . . . . . . 14 ⊢ (𝑐 ⊆ 𝐽 → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))))
25	18, 24	sylbi 220	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ 𝒫 𝐽 → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))))
26	25	adantl 485	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))))
27	26	rexlimdv 3242	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
28		simpll 766	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝐽 ∈ Top)
29	4	sseq2i 3944	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽)
30		uniexg 7446	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
31		ssexg 5191	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ∈ V) → 𝑆 ∈ V)
32	30, 31	sylan2 595	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ∪ 𝐽 ∧ 𝐽 ∈ Top) → 𝑆 ∈ V)
33	32	ancoms 462	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → 𝑆 ∈ V)
34	29, 33	sylan2b 596	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V)
35	34	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝑆 ∈ V)
36		elrest 16693	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑡 ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
37	28, 35, 36	syl2anc 587	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
38	27, 37	sylibrd 262	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆) → 𝑡 ∈ (𝐽 ↾t 𝑆)))
39	17, 38	syl5bi 245	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → 𝑡 ∈ (𝐽 ↾t 𝑆)))
40	39	ssrdv 3921	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ⊆ (𝐽 ↾t 𝑆))
41		vex 3444	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
42	41	abrexex 7645	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ V
43	42	elpw 4501	. . . . . . . 8 ⊢ ({𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆) ↔ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ⊆ (𝐽 ↾t 𝑆))
44	40, 43	sylibr 237	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆))
45		unieq 4811	. . . . . . . . . 10 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∪ 𝑠 = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
46	45	eqeq2d 2809	. . . . . . . . 9 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 ↔ ∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}))
47		pweq 4513	. . . . . . . . . . 11 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → 𝒫 𝑠 = 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
48	47	ineq1d 4138	. . . . . . . . . 10 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (𝒫 𝑠 ∩ Fin) = (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin))
49	48	rexeqdv 3365	. . . . . . . . 9 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
50	46, 49	imbi12d 348	. . . . . . . 8 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ((∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) ↔ (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
51	50	rspcva 3569	. . . . . . 7 ⊢ (({𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆) ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)) → (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
52	44, 51	sylan 583	. . . . . 6 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)) → (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
53	52	ex 416	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) → (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
54	4	restuni 21767	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾t 𝑆))
55	54	ad2antrr 725	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → 𝑆 = ∪ (𝐽 ↾t 𝑆))
56		vex 3444	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
57	56	inex1 5185	. . . . . . . . . . . . 13 ⊢ (𝑦 ∩ 𝑆) ∈ V
58	57	dfiun2 4920	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 ∈ 𝑐 (𝑦 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}
59		incom 4128	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ 𝑆) = (𝑆 ∩ 𝑦)
60	59	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ 𝑦 ∈ 𝑐) → (𝑦 ∩ 𝑆) = (𝑆 ∩ 𝑦))
61	60	iuneq2dv 4905	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 (𝑦 ∩ 𝑆) = ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦))
62	58, 61	syl5eqr 2847	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} = ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦))
63		iunin2 4956	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦) = (𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦)
64		uniiun 4945	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑐 = ∪ 𝑦 ∈ 𝑐 𝑦
65	64	eqcomi 2807	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐
66	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐)
67	66	ineq2d 4139	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦) = (𝑆 ∩ ∪ 𝑐))
68		incom 4128	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∩ ∪ 𝑐) = (∪ 𝑐 ∩ 𝑆)
69		sseqin2 4142	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ ∪ 𝑐 ↔ (∪ 𝑐 ∩ 𝑆) = 𝑆)
70	69	biimpi 219	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ ∪ 𝑐 → (∪ 𝑐 ∩ 𝑆) = 𝑆)
71	68, 70	syl5eq 2845	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ ∪ 𝑐 → (𝑆 ∩ ∪ 𝑐) = 𝑆)
72	71	adantl 485	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑐) = 𝑆)
73	67, 72	eqtrd 2833	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦) = 𝑆)
74	63, 73	syl5eq 2845	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦) = 𝑆)
75	62, 74	eqtr2d 2834	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → 𝑆 = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
76	55, 75	eqeq12d 2814	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 = 𝑆 ↔ ∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}))
77	55	eqeq1d 2800	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 = ∪ 𝑡 ↔ ∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
78	77	rexbidv 3256	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
79	76, 78	imbi12d 348	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡) ↔ (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
80		eqid 2798	. . . . . . . . . 10 ⊢ 𝑆 = 𝑆
81	80	a1bi 366	. . . . . . . . 9 ⊢ (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 ↔ (𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡))
82		elin 3897	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin) ↔ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∧ 𝑡 ∈ Fin))
83		velpw 4502	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ 𝑡 ⊆ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
84		dfss3 3903	. . . . . . . . . . . . . 14 ⊢ (𝑡 ⊆ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
85		vex 3444	. . . . . . . . . . . . . . . 16 ⊢ 𝑠 ∈ V
86		eqeq1 2802	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑠 → (𝑥 = (𝑦 ∩ 𝑆) ↔ 𝑠 = (𝑦 ∩ 𝑆)))
87	86	rexbidv 3256	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑠 → (∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆) ↔ ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)))
88	85, 87	elab 3615	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆))
89	88	ralbii 3133	. . . . . . . . . . . . . 14 ⊢ (∀𝑠 ∈ 𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆))
90	83, 84, 89	3bitri 300	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆))
91	90	anbi1i 626	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∧ 𝑡 ∈ Fin) ↔ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin))
92	82, 91	bitri 278	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin) ↔ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin))
93		ineq1 4131	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑓‘𝑠) → (𝑦 ∩ 𝑆) = ((𝑓‘𝑠) ∩ 𝑆))
94	93	eqeq2d 2809	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑓‘𝑠) → (𝑠 = (𝑦 ∩ 𝑆) ↔ 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)))
95	94	ac6sfi 8746	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)))
96	95	ancoms 462	. . . . . . . . . . . . 13 ⊢ ((∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)))
97	96	adantl 485	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)))
98		frn 6493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑡⟶𝑐 → ran 𝑓 ⊆ 𝑐)
99	98	ad2antrl 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ⊆ 𝑐)
100		vex 3444	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑓 ∈ V
101	100	rnex 7599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran 𝑓 ∈ V
102	101	elpw 4501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐)
103	99, 102	sylibr 237	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ 𝒫 𝑐)
104		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → 𝑡 ∈ Fin)
105	104	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → 𝑡 ∈ Fin)
106		ffn 6487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:𝑡⟶𝑐 → 𝑓 Fn 𝑡)
107		dffn4 6571	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 Fn 𝑡 ↔ 𝑓:𝑡–onto→ran 𝑓)
108	106, 107	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:𝑡⟶𝑐 → 𝑓:𝑡–onto→ran 𝑓)
109		fodomfi 8781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ Fin ∧ 𝑓:𝑡–onto→ran 𝑓) → ran 𝑓 ≼ 𝑡)
110	108, 109	sylan2 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ Fin ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡)
111	110	adantll 713	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin) ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡)
112	111	adantll 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡)
113	112	ad2ant2r 746	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ≼ 𝑡)
114		domfi 8723	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ Fin ∧ ran 𝑓 ≼ 𝑡) → ran 𝑓 ∈ Fin)
115	105, 113, 114	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ Fin)
116	103, 115	elind 4121	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
117		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑢 → 𝑠 = 𝑢)
118		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = 𝑢 → (𝑓‘𝑠) = (𝑓‘𝑢))
119	118	ineq1d 4138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑢 → ((𝑓‘𝑠) ∩ 𝑆) = ((𝑓‘𝑢) ∩ 𝑆))
120	117, 119	eqeq12d 2814	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑢 → (𝑠 = ((𝑓‘𝑠) ∩ 𝑆) ↔ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)))
121	120	rspccv 3568	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆) → (𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)))
122		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)))
123		inss1 4155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓‘𝑢) ∩ 𝑆) ⊆ (𝑓‘𝑢)
124		sseq1 3940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑢 ⊆ (𝑓‘𝑢) ↔ ((𝑓‘𝑢) ∩ 𝑆) ⊆ (𝑓‘𝑢)))
125	123, 124	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → 𝑢 ⊆ (𝑓‘𝑢))
126		ssel 3908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑢 ⊆ (𝑓‘𝑢) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (𝑓‘𝑢)))
127	126	a1dd 50	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑢 ⊆ (𝑓‘𝑢) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢))))
128	125, 127	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢))))
129	128	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑢 ∈ 𝑡 → (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢)))))
130	129	3imp 1108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢)))
131		fnfvelrn 6825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡) → (𝑓‘𝑢) ∈ ran 𝑓)
132	131	expcom 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑢 ∈ 𝑡 → (𝑓 Fn 𝑡 → (𝑓‘𝑢) ∈ ran 𝑓))
133	132	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓 Fn 𝑡 → (𝑓‘𝑢) ∈ ran 𝑓))
134	106, 133	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → (𝑓‘𝑢) ∈ ran 𝑓))
135	130, 134	jcad 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))
136	135	3exp 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 ∈ 𝑡 → (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))))
137	122, 136	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))))
138	137	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ 𝑢 → (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))))
139	138	imp 410	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))))
140	139	com3l 89	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))))
141	140	impcom 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:𝑡⟶𝑐 ∧ (𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆))) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))
142	121, 141	sylan2 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))
143		fvex 6658	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓‘𝑢) ∈ V
144		eleq2 2878	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ (𝑓‘𝑢)))
145		eleq1 2877	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑣 ∈ ran 𝑓 ↔ (𝑓‘𝑢) ∈ ran 𝑓))
146	144, 145	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = (𝑓‘𝑢) → ((𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓) ↔ (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))
147	143, 146	spcev 3555	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓))
148	142, 147	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓)))
149	148	exlimdv 1934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (∃𝑢(𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓)))
150		eluni 4803	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ∪ 𝑡 ↔ ∃𝑢(𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡))
151		eluni 4803	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ∪ ran 𝑓 ↔ ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓))
152	149, 150, 151	3imtr4g 299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑤 ∈ ∪ 𝑡 → 𝑤 ∈ ∪ ran 𝑓))
153	152	ssrdv 3921	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∪ 𝑡 ⊆ ∪ ran 𝑓)
154	153	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ∪ 𝑡 ⊆ ∪ ran 𝑓)
155		sseq1 3940	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 = ∪ 𝑡 → (𝑆 ⊆ ∪ ran 𝑓 ↔ ∪ 𝑡 ⊆ ∪ ran 𝑓))
156	155	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → (𝑆 ⊆ ∪ ran 𝑓 ↔ ∪ 𝑡 ⊆ ∪ ran 𝑓))
157	154, 156	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → 𝑆 ⊆ ∪ ran 𝑓)
158	116, 157	jca 515	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓))
159	158	ex 416	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) → ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓)))
160	159	eximdv 1918	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓)))
161	160	ex 416	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = ∪ 𝑡 → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓))))
162	161	com23 86	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑆 = ∪ 𝑡 → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓))))
163		unieq 4811	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ran 𝑓 → ∪ 𝑑 = ∪ ran 𝑓)
164	163	sseq2d 3947	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ran 𝑓 → (𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 ⊆ ∪ ran 𝑓))
165	164	rspcev 3571	. . . . . . . . . . . . . 14 ⊢ ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)
166	165	exlimiv 1931	. . . . . . . . . . . . 13 ⊢ (∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)
167	162, 166	syl8 76	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
168	97, 167	mpd 15	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))
169	92, 168	sylan2b 596	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ 𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))
170	169	rexlimdva 3243	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))
171	81, 170	syl5bir 246	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))
172	79, 171	sylbird 263	. . . . . . 7 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))
173	172	ex 416	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑆 ⊆ ∪ 𝑐 → ((∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
174	173	com23 86	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → ((∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) → (𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
175	53, 174	syld 47	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) → (𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
176	175	ralrimdva 3154	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) → ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
177	4	cmpsublem 22004	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
178	176, 177	impbid 215	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
179	13, 178	bitrd 282	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881  𝒫 cpw 4497  ∪ cuni 4800  ∪ ciun 4881   class class class wbr 5030  ran crn 5520   Fn wfn 6319  ⟶wf 6320  –onto→wfo 6322  ‘cfv 6324  (class class class)co 7135   ≼ cdom 8490  Fincfn 8492   ↾_t crest 16686  Topctop 21498  Compccmp 21991

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-en 8493  df-dom 8494  df-fin 8496  df-fi 8859  df-rest 16688  df-topgen 16709  df-top 21499  df-topon 21516  df-bases 21551  df-cmp 21992

This theorem is referenced by:  cmpcld  22007  uncmp  22008  hauscmplem  22011  1stckgenlem  22158  icccmp  23430  bndth  23563  ovolicc2  24126  stoweidlem50  42692  stoweidlem57  42699