Theorem cmpsub 23316

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 2733	. . . 4 ⊢ ∪ (𝐽 ↾t 𝑆) = ∪ (𝐽 ↾t 𝑆)
2	1	iscmp 23304	. . 3 ⊢ ((𝐽 ↾t 𝑆) ∈ Comp ↔ ((𝐽 ↾t 𝑆) ∈ Top ∧ ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
3		id 22	. . . . . 6 ⊢ (𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋)
4		cmpsub.1	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐽
5	4	topopn 22822	. . . . . 6 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
6		ssexg 5263	. . . . . 6 ⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑆 ∈ V)
7	3, 5, 6	syl2anr 597	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V)
8		resttop 23076	. . . . 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 3441	. . . . . . . . . . 11 ⊢ 𝑡 ∈ V
15		eqeq1 2737	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑥 = (𝑦 ∩ 𝑆) ↔ 𝑡 = (𝑦 ∩ 𝑆)))
16	15	rexbidv 3157	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆) ↔ ∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆)))
17	14, 16	elab 3631	. . . . . . . . . 10 ⊢ (𝑡 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆))
18		velpw 4554	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽)
19		ssel2 3925	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐) → 𝑦 ∈ 𝐽)
20		ineq1 4162	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑦 → (𝑑 ∩ 𝑆) = (𝑦 ∩ 𝑆))
21	20	rspceeqv 3596	. . . . . . . . . . . . . . . . 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 3132	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → (∃𝑦 ∈ 𝑐 𝑡 = (𝑦 ∩ 𝑆) → ∃𝑑 ∈ 𝐽 𝑡 = (𝑑 ∩ 𝑆)))
28		simpll 766	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → 𝐽 ∈ Top)
29	4	sseq2i 3960	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽)
30		uniexg 7679	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
31		ssexg 5263	. . . . . . . . . . . . . . . 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 17333	. . . . . . . . . . . 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 3936	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ⊆ (𝐽 ↾t 𝑆))
41		vex 3441	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
42	41	abrexex 7900	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ V
43	42	elpw 4553	. . . . . . . 8 ⊢ ({𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆) ↔ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ⊆ (𝐽 ↾t 𝑆))
44	40, 43	sylibr 234	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) → {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∈ 𝒫 (𝐽 ↾t 𝑆))
45		unieq 4869	. . . . . . . . . 10 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∪ 𝑠 = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
46	45	eqeq2d 2744	. . . . . . . . 9 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 ↔ ∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}))
47		pweq 4563	. . . . . . . . . . 11 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → 𝒫 𝑠 = 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
48	47	ineq1d 4168	. . . . . . . . . 10 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (𝒫 𝑠 ∩ Fin) = (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin))
49	48	rexeqdv 3294	. . . . . . . . 9 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → (∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
50	46, 49	imbi12d 344	. . . . . . . 8 ⊢ (𝑠 = {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ((∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) ↔ (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
51	50	rspcva 3571	. . . . . . 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 23078	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾t 𝑆))
55	54	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → 𝑆 = ∪ (𝐽 ↾t 𝑆))
56		vex 3441	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
57	56	inex1 5257	. . . . . . . . . . . . 13 ⊢ (𝑦 ∩ 𝑆) ∈ V
58	57	dfiun2 4982	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 ∈ 𝑐 (𝑦 ∩ 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}
59		incom 4158	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ 𝑆) = (𝑆 ∩ 𝑦)
60	59	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ 𝑦 ∈ 𝑐) → (𝑦 ∩ 𝑆) = (𝑆 ∩ 𝑦))
61	60	iuneq2dv 4966	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 (𝑦 ∩ 𝑆) = ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦))
62	58, 61	eqtr3id 2782	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} = ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦))
63		iunin2 5021	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦) = (𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦)
64		uniiun 5009	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑐 = ∪ 𝑦 ∈ 𝑐 𝑦
65	64	eqcomi 2742	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐
66	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐)
67	66	ineq2d 4169	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦) = (𝑆 ∩ ∪ 𝑐))
68		incom 4158	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∩ ∪ 𝑐) = (∪ 𝑐 ∩ 𝑆)
69		sseqin2 4172	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ ∪ 𝑐 ↔ (∪ 𝑐 ∩ 𝑆) = 𝑆)
70	69	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ ∪ 𝑐 → (∪ 𝑐 ∩ 𝑆) = 𝑆)
71	68, 70	eqtrid 2780	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ ∪ 𝑐 → (𝑆 ∩ ∪ 𝑐) = 𝑆)
72	71	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑐) = 𝑆)
73	67, 72	eqtrd 2768	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦) = 𝑆)
74	63, 73	eqtrid 2780	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ∪ 𝑦 ∈ 𝑐 (𝑆 ∩ 𝑦) = 𝑆)
75	62, 74	eqtr2d 2769	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → 𝑆 = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
76	55, 75	eqeq12d 2749	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 = 𝑆 ↔ ∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)}))
77	55	eqeq1d 2735	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (𝑆 = ∪ 𝑡 ↔ ∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
78	77	rexbidv 3157	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 ↔ ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))
79	76, 78	imbi12d 344	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) → ((𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡) ↔ (∪ (𝐽 ↾t 𝑆) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
80		eqid 2733	. . . . . . . . . 10 ⊢ 𝑆 = 𝑆
81	80	a1bi 362	. . . . . . . . 9 ⊢ (∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡 ↔ (𝑆 = 𝑆 → ∃𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)𝑆 = ∪ 𝑡))
82		elin 3914	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin) ↔ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∧ 𝑡 ∈ Fin))
83		velpw 4554	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ 𝑡 ⊆ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
84		dfss3 3919	. . . . . . . . . . . . . 14 ⊢ (𝑡 ⊆ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∀𝑠 ∈ 𝑡 𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)})
85		vex 3441	. . . . . . . . . . . . . . . 16 ⊢ 𝑠 ∈ V
86		eqeq1 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑠 → (𝑥 = (𝑦 ∩ 𝑆) ↔ 𝑠 = (𝑦 ∩ 𝑆)))
87	86	rexbidv 3157	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑠 → (∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆) ↔ ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆)))
88	85, 87	elab 3631	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ↔ ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆))
89	88	ralbii 3079	. . . . . . . . . . . . . 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 4162	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑓‘𝑠) → (𝑦 ∩ 𝑆) = ((𝑓‘𝑠) ∩ 𝑆))
94	93	eqeq2d 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑓‘𝑠) → (𝑠 = (𝑦 ∩ 𝑆) ↔ 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)))
95	94	ac6sfi 9175	. . . . . . . . . . . . . 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 3441	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑓 ∈ V
101	100	rnex 7846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran 𝑓 ∈ V
102	101	elpw 4553	. . . . . . . . . . . . . . . . . . . 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 9203	. . . . . . . . . . . . . . . . . . . . . . . 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 9105	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ Fin ∧ ran 𝑓 ≼ 𝑡) → ran 𝑓 ∈ Fin)
115	105, 113, 114	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ Fin)
116	103, 115	elind 4149	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin))
117		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑢 → 𝑠 = 𝑢)
118		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = 𝑢 → (𝑓‘𝑠) = (𝑓‘𝑢))
119	118	ineq1d 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑢 → ((𝑓‘𝑠) ∩ 𝑆) = ((𝑓‘𝑢) ∩ 𝑆))
120	117, 119	eqeq12d 2749	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑢 → (𝑠 = ((𝑓‘𝑠) ∩ 𝑆) ↔ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)))
121	120	rspccv 3570	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆) → (𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)))
122		pm2.27 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 ∈ 𝑡 → ((𝑢 ∈ 𝑡 → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)) → 𝑢 = ((𝑓‘𝑢) ∩ 𝑆)))
123		inss1 4186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓‘𝑢) ∩ 𝑆) ⊆ (𝑓‘𝑢)
124		sseq1 3956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑢 ⊆ (𝑓‘𝑢) ↔ ((𝑓‘𝑢) ∩ 𝑆) ⊆ (𝑓‘𝑢)))
125	123, 124	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → 𝑢 ⊆ (𝑓‘𝑢))
126		ssel 3924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑢 ⊆ (𝑓‘𝑢) → (𝑤 ∈ 𝑢 → 𝑤 ∈ (𝑓‘𝑢)))
127	126	a1dd 50	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑢 ⊆ (𝑓‘𝑢) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢))))
128	125, 127	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢))))
129	128	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑢 ∈ 𝑡 → (𝑢 = ((𝑓‘𝑢) ∩ 𝑆) → (𝑤 ∈ 𝑢 → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢)))))
130	129	3imp 1110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑢 ∈ 𝑡 ∧ 𝑢 = ((𝑓‘𝑢) ∩ 𝑆) ∧ 𝑤 ∈ 𝑢) → (𝑓:𝑡⟶𝑐 → 𝑤 ∈ (𝑓‘𝑢)))
131		fnfvelrn 7019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓‘𝑢) ∈ V
144		eleq2 2822	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ (𝑓‘𝑢)))
145		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑣 ∈ ran 𝑓 ↔ (𝑓‘𝑢) ∈ ran 𝑓))
146	144, 145	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = (𝑓‘𝑢) → ((𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓) ↔ (𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓)))
147	143, 146	spcev 3557	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑤 ∈ (𝑓‘𝑢) ∧ (𝑓‘𝑢) ∈ ran 𝑓) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓))
148	142, 147	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ((𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓)))
149	148	exlimdv 1934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (∃𝑢(𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡) → ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓)))
150		eluni 4861	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ∪ 𝑡 ↔ ∃𝑢(𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡))
151		eluni 4861	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ∪ ran 𝑓 ↔ ∃𝑣(𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓))
152	149, 150, 151	3imtr4g 296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → (𝑤 ∈ ∪ 𝑡 → 𝑤 ∈ ∪ ran 𝑓))
153	152	ssrdv 3936	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆)) → ∪ 𝑡 ⊆ ∪ ran 𝑓)
154	153	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ (∀𝑠 ∈ 𝑡 ∃𝑦 ∈ 𝑐 𝑠 = (𝑦 ∩ 𝑆) ∧ 𝑡 ∈ Fin)) ∧ 𝑆 = ∪ 𝑡) ∧ (𝑓:𝑡⟶𝑐 ∧ ∀𝑠 ∈ 𝑡 𝑠 = ((𝑓‘𝑠) ∩ 𝑆))) → ∪ 𝑡 ⊆ ∪ ran 𝑓)
155		sseq1 3956	. . . . . . . . . . . . . . . . . . . 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 1918	. . . . . . . . . . . . . . 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 4869	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ran 𝑓 → ∪ 𝑑 = ∪ ran 𝑓)
164	163	sseq2d 3963	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ran 𝑓 → (𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 ⊆ ∪ ran 𝑓))
165	164	rspcev 3573	. . . . . . . . . . . . . 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 594	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑐 ∈ 𝒫 𝐽) ∧ 𝑆 ⊆ ∪ 𝑐) ∧ 𝑡 ∈ (𝒫 {𝑥 ∣ ∃𝑦 ∈ 𝑐 𝑥 = (𝑦 ∩ 𝑆)} ∩ Fin)) → (𝑆 = ∪ 𝑡 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))
170	169	rexlimdva 3134	. . . . . . . . 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 3133	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡) → ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
177	4	cmpsublem 23315	. . 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 1541  ∃wex 1780   ∈ wcel 2113  {cab 2711  ∀wral 3048  ∃wrex 3057  Vcvv 3437   ∩ cin 3897   ⊆ wss 3898  𝒫 cpw 4549  ∪ cuni 4858  ∪ ciun 4941   class class class wbr 5093  ran crn 5620   Fn wfn 6481  ⟶wf 6482  –onto→wfo 6484  ‘cfv 6486  (class class class)co 7352   ≼ cdom 8873  Fincfn 8875   ↾_t crest 17326  Topctop 22809  Compccmp 23302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-int 4898  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  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 7355  df-oprab 7356  df-mpo 7357  df-om 7803  df-1st 7927  df-2nd 7928  df-1o 8391  df-en 8876  df-dom 8877  df-fin 8879  df-fi 9302  df-rest 17328  df-topgen 17349  df-top 22810  df-topon 22827  df-bases 22862  df-cmp 23303

This theorem is referenced by:  cmpcld  23318  uncmp  23319  hauscmplem  23322  1stckgenlem  23469  icccmp  24742  bndth  24885  ovolicc2  25451  stoweidlem50  46173  stoweidlem57  46180