Theorem cmpsub 23303

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 2729	. . . 4 ⊢ ∪ (𝐽 ↾t 𝑆) = ∪ (𝐽 ↾t 𝑆)
2	1	iscmp 23291	. . 3 ⊢ ((𝐽 ↾t 𝑆) ∈ Comp ↔ ((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
3		id 22	. . . . . 6 ⊢ (𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋)
4		cmpsub.1	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐽
5	4	topopn 22809	. . . . . 6 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
6		ssexg 5265	. . . . . 6 ⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑆 ∈ V)
7	3, 5, 6	syl2anr 597	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V)
8		resttop 23063	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽 ↾t 𝑆) ∈ Top)
9	7, 8	syldan 591	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐽 ↾t 𝑆) ∈ Top)
10		ibar 528	. . . . 5 ⊢ ((𝐽 ↾t 𝑆) ∈ Top → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) ↔ ((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))))
11	10	bicomd 223	. . . 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	bitrid 283	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
14		vex 3442	. . . . . . . . . . 11 ⊢ 𝑡 ∈ V
15		eqeq1 2733	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑦 ∩ 𝑆) ↔ 𝑡 = (𝑦 ∩ 𝑆)))
16	15	rexbidv 3153	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆) ↔ ∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆)))
17	14, 16	elab 3637	. . . . . . . . . 10 ⊢ (𝑡 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆))
18		velpw 4558	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽)
19		ssel2 3932	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐) → 𝑦 ∈ 𝐽)
20		ineq1 4166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑦 → (𝑑 ∩ 𝑆) = (𝑦 ∩ 𝑆))
21	20	rspceeqv 3602	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝐽 ∧ 𝑡 = (𝑦 ∩ 𝑆)) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))
22	21	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐽 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
23	19, 22	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐) → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
24	23	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝑐 ⊆ 𝐽 → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))))
25	18, 24	sylbi 217	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ 𝒫 𝐽 → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))))
26	25	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑦 ∈ 𝑐 → (𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆))))
27	26	rexlimdv 3128	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
28		simpll 766	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝐽 ∈ Top)
29	4	sseq2i 3967	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽)
30		uniexg 7680	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
31		ssexg 5265	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ∈ V) → 𝑆 ∈ V)
32	30, 31	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ ∪ 𝐽 ∧ 𝐽 ∈ Top) → 𝑆 ∈ V)
33	32	ancoms 458	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → 𝑆 ∈ V)
34	29, 33	sylan2b 594	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V)
35	34	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝑆 ∈ V)
36		elrest 17349	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝑡 ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
37	28, 35, 36	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
38	27, 37	sylibrd 259	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆) → 𝑡 ∈ (𝐽 ↾t 𝑆)))
39	17, 38	biimtrid 242	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (𝑡 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → 𝑡 ∈ (𝐽 ↾t 𝑆)))
40	39	ssrdv 3943	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ⊆ (𝐽 ↾t 𝑆))
41		vex 3442	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
42	41	abrexex 7904	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ V
43	42	elpw 4557	. . . . . . . 8 ⊢ ({𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆) ↔ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ⊆ (𝐽 ↾t 𝑆))
44	40, 43	sylibr 234	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆))
45		unieq 4872	. . . . . . . . . 10 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∪ 𝑠 = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
46	45	eqeq2d 2740	. . . . . . . . 9 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 ↔ ∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}))
47		pweq 4567	. . . . . . . . . . 11 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → 𝒫 𝑠 = 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
48	47	ineq1d 4172	. . . . . . . . . 10 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (𝒫 𝑠 ∩ Fin) = (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin))
49	48	rexeqdv 3291	. . . . . . . . 9 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
50	46, 49	imbi12d 344	. . . . . . . 8 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ((∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) ↔ (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
51	50	rspcva 3577	. . . . . . 7 ⊢ (({𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆) ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)) → (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
52	44, 51	sylan 580	. . . . . 6 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)) → (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
53	52	ex 412	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) → (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
54	4	restuni 23065	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾t 𝑆))
55	54	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → 𝑆 = ∪ (𝐽 ↾t 𝑆))
56		vex 3442	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
57	56	inex1 5259	. . . . . . . . . . . . 13 ⊢ (𝑦 ∩ 𝑆) ∈ V
58	57	dfiun2 4985	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 ∈ 𝑐 (𝑦 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}
59		incom 4162	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ 𝑆) = (𝑆 ∩ 𝑦)
60	59	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ 𝑦 ∈ 𝑐) → (𝑦 ∩ 𝑆) = (𝑆 ∩ 𝑦))
61	60	iuneq2dv 4969	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 (𝑦 ∩ 𝑆) = ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦))
62	58, 61	eqtr3id 2778	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} = ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦))
63		iunin2 5023	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦) = (𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦)
64		uniiun 5010	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑐 = ∪ 𝑦 ∈ 𝑐 𝑦
65	64	eqcomi 2738	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐
66	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐)
67	66	ineq2d 4173	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦) = (𝑆 ∩ ∪ 𝑐))
68		incom 4162	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∩ ∪ 𝑐) = (∪ 𝑐 ∩ 𝑆)
69		sseqin2 4176	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ ∪ 𝑐 ↔ (∪ 𝑐 ∩ 𝑆) = 𝑆)
70	69	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ ∪ 𝑐 → (∪ 𝑐 ∩ 𝑆) = 𝑆)
71	68, 70	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ ∪ 𝑐 → (𝑆 ∩ ∪ 𝑐) = 𝑆)
72	71	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑐) = 𝑆)
73	67, 72	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦) = 𝑆)
74	63, 73	eqtrid 2776	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦) = 𝑆)
75	62, 74	eqtr2d 2765	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → 𝑆 = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
76	55, 75	eqeq12d 2745	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 = 𝑆 ↔ ∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}))
77	55	eqeq1d 2731	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 = ∪ 𝑡 ↔ ∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
78	77	rexbidv 3153	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
79	76, 78	imbi12d 344	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡) ↔ (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
80		eqid 2729	. . . . . . . . . 10 ⊢ 𝑆 = 𝑆
81	80	a1bi 362	. . . . . . . . 9 ⊢ (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 ↔ (𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡))
82		elin 3921	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin) ↔ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∧ 𝑡 ∈ Fin))
83		velpw 4558	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ 𝑡 ⊆ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
84		dfss3 3926	. . . . . . . . . . . . . 14 ⊢ (𝑡 ⊆ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
85		vex 3442	. . . . . . . . . . . . . . . 16 ⊢ 𝑠 ∈ V
86		eqeq1 2733	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑠 → (𝑥 = (𝑦 ∩ 𝑆) ↔ 𝑠 = (𝑦 ∩ 𝑆)))
87	86	rexbidv 3153	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑠 → (∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆) ↔ ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)))
88	85, 87	elab 3637	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆))
89	88	ralbii 3075	. . . . . . . . . . . . . 14 ⊢ (∀𝑠 ∈ 𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆))
90	83, 84, 89	3bitri 297	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆))
91	90	anbi1i 624	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∧ 𝑡 ∈ Fin) ↔ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin))
92	82, 91	bitri 275	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin) ↔ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin))
93		ineq1 4166	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑓‘𝑠) → (𝑦 ∩ 𝑆) = ((𝑓‘𝑠) ∩ 𝑆))
94	93	eqeq2d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑓‘𝑠) → (𝑠 = (𝑦 ∩ 𝑆) ↔ 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)))
95	94	ac6sfi 9189	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ Fin ∧ ∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)))
96	95	ancoms 458	. . . . . . . . . . . . 13 ⊢ ((∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)))
97	96	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → ∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)))
98		frn 6663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑡⟶𝑐 → ran 𝑓 ⊆ 𝑐)
99	98	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ⊆ 𝑐)
100		vex 3442	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑓 ∈ V
101	100	rnex 7850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran 𝑓 ∈ V
102	101	elpw 4557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐)
103	99, 102	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ 𝒫 𝑐)
104		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → 𝑡 ∈ Fin)
105	104	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → 𝑡 ∈ Fin)
106		ffn 6656	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓:𝑡⟶𝑐 → 𝑓 Fn 𝑡)
107		dffn4 6746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 Fn 𝑡 ↔ 𝑓:𝑡–onto→ran 𝑓)
108	106, 107	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:𝑡⟶𝑐 → 𝑓:𝑡–onto→ran 𝑓)
109		fodomfi 9219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 ∈ Fin ∧ 𝑓:𝑡–onto→ran 𝑓) → ran 𝑓 ≼ 𝑡)
110	108, 109	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ Fin ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡)
111	110	adantll 714	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin) ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡)
112	111	adantll 714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑓:𝑡⟶𝑐) → ran 𝑓 ≼ 𝑡)
113	112	ad2ant2r 747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ≼ 𝑡)
114		domfi 9113	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ Fin ∧ ran 𝑓 ≼ 𝑡) → ran 𝑓 ∈ Fin)
115	105, 113, 114	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ Fin)
116	103, 115	elind 4153	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
117		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑢 → 𝑠 = 𝑢)
118		fveq2 6826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = 𝑢 → (𝑓‘𝑠) = (𝑓‘𝑢))
119	118	ineq1d 4172	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑢 → ((𝑓‘𝑠) ∩ 𝑆) = ((𝑓‘𝑢) ∩ 𝑆))
120	117, 119	eqeq12d 2745	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑢 → (𝑠 = ((𝑓‘𝑠) ∩ 𝑆) ↔ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)))
121	120	rspccv 3576	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆) → (𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)))
122		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)))
123		inss1 4190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓‘𝑢) ∩ 𝑆) ⊆ (𝑓‘𝑢)
124		sseq1 3963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑢 ⊆ (𝑓‘𝑢) ↔ ((𝑓‘𝑢) ∩ 𝑆) ⊆ (𝑓‘𝑢)))
125	123, 124	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → 𝑢 ⊆ (𝑓‘𝑢))
126		ssel 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑢 ⊆ (𝑓‘𝑢) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (𝑓‘𝑢)))
127	126	a1dd 50	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑢 ⊆ (𝑓‘𝑢) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢))))
128	125, 127	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢))))
129	128	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑢 ∈ 𝑡 → (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢)))))
130	129	3imp 1110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢)))
131		fnfvelrn 7018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡) → (𝑓‘𝑢) ∈ ran 𝑓)
132	131	expcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑢 ∈ 𝑡 → (𝑓 Fn 𝑡 → (𝑓‘𝑢) ∈ ran 𝑓))
133	132	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓 Fn 𝑡 → (𝑓‘𝑢) ∈ ran 𝑓))
134	106, 133	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → (𝑓‘𝑢) ∈ ran 𝑓))
135	130, 134	jcad 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))
136	135	3exp 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 ∈ 𝑡 → (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))))
137	122, 136	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))))
138	137	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ 𝑢 → (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))))
139	138	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))))
140	139	com3l 89	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → (𝑓:𝑡⟶𝑐 → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓))))
141	140	impcom 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:𝑡⟶𝑐 ∧ (𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆))) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))
142	121, 141	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))
143		fvex 6839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓‘𝑢) ∈ V
144		eleq2 2817	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ (𝑓‘𝑢)))
145		eleq1 2816	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑣 ∈ ran 𝑓 ↔ (𝑓‘𝑢) ∈ ran 𝑓))
146	144, 145	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = (𝑓‘𝑢) → ((𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓) ↔ (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))
147	143, 146	spcev 3563	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓))
148	142, 147	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓)))
149	148	exlimdv 1933	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (∃𝑢(𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓)))
150		eluni 4864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ∪ 𝑡 ↔ ∃𝑢(𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡))
151		eluni 4864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ∪ ran 𝑓 ↔ ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓))
152	149, 150, 151	3imtr4g 296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑤 ∈ ∪ 𝑡 → 𝑤 ∈ ∪ ran 𝑓))
153	152	ssrdv 3943	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∪ 𝑡 ⊆ ∪ ran 𝑓)
154	153	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ∪ 𝑡 ⊆ ∪ ran 𝑓)
155		sseq1 3963	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 = ∪ 𝑡 → (𝑆 ⊆ ∪ ran 𝑓 ↔ ∪ 𝑡 ⊆ ∪ ran 𝑓))
156	155	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → (𝑆 ⊆ ∪ ran 𝑓 ↔ ∪ 𝑡 ⊆ ∪ ran 𝑓))
157	154, 156	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → 𝑆 ⊆ ∪ ran 𝑓)
158	116, 157	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓))
159	158	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) → ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓)))
160	159	eximdv 1917	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓)))
161	160	ex 412	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (𝑆 = ∪ 𝑡 → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓))))
162	161	com23 86	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) → (∃𝑓(𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑆 = ∪ 𝑡 → ∃𝑓(ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓))))
163		unieq 4872	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ran 𝑓 → ∪ 𝑑 = ∪ ran 𝑓)
164	163	sseq2d 3970	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ran 𝑓 → (𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 ⊆ ∪ ran 𝑓))
165	164	rspcev 3579	. . . . . . . . . . . . . 14 ⊢ ((ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑆 ⊆ ∪ ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)
166	165	exlimiv 1930	. . . . . . . . . . . . 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 594	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ 𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))
170	169	rexlimdva 3130	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))
171	81, 170	biimtrrid 243	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))
172	79, 171	sylbird 260	. . . . . . 7 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))
173	172	ex 412	. . . . . 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 3129	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) → ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
177	4	cmpsublem 23302	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
178	176, 177	impbid 212	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
179	13, 178	bitrd 279	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707  ∀wral 3044  ∃wrex 3053  Vcvv 3438   ∩ cin 3904   ⊆ wss 3905  𝒫 cpw 4553  ∪ cuni 4861  ∪ ciun 4944   class class class wbr 5095  ran crn 5624   Fn wfn 6481  ⟶wf 6482  –onto→wfo 6484  ‘cfv 6486  (class class class)co 7353   ≼ cdom 8877  Fincfn 8879   ↾_t crest 17342  Topctop 22796  Compccmp 23289

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 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-1st 7931  df-2nd 7932  df-1o 8395  df-en 8880  df-dom 8881  df-fin 8883  df-fi 9320  df-rest 17344  df-topgen 17365  df-top 22797  df-topon 22814  df-bases 22849  df-cmp 23290

This theorem is referenced by:  cmpcld  23305  uncmp  23306  hauscmplem  23309  1stckgenlem  23456  icccmp  24730  bndth  24873  ovolicc2  25439  stoweidlem50  46035  stoweidlem57  46042