Theorem hauscmplem 21209

Description: Lemma for hauscmp 21210. (Contributed by Mario Carneiro, 27-Nov-2013.)

Hypotheses

Ref	Expression
hauscmp.1	⊢ 𝑋 = ∪ 𝐽
hauscmplem.2	⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}
hauscmplem.3	⊢ (𝜑 → 𝐽 ∈ Haus)
hauscmplem.4	⊢ (𝜑 → 𝑆 ⊆ 𝑋)
hauscmplem.5	⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp)
hauscmplem.6	⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆))

Assertion

Ref	Expression
hauscmplem	⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))

Distinct variable groups:   𝑦,𝑤,𝑧,𝐴   𝑤,𝐽,𝑦,𝑧   𝜑,𝑤,𝑦,𝑧   𝑤,𝑆,𝑦,𝑧   𝑧,𝑂   𝑤,𝑋,𝑦,𝑧

Allowed substitution hints:   𝑂(𝑦,𝑤)

Proof of Theorem hauscmplem

Dummy variables 𝑓 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hauscmplem.3	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Haus)
2		haustop 21135	. . . . . . 7 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
4	3	ad3antrrr 766	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝐽 ∈ Top)
5		hauscmp.1	. . . . . 6 ⊢ 𝑋 = ∪ 𝐽
6	5	topopn 20711	. . . . 5 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
7	4, 6	syl 17	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑋 ∈ 𝐽)
8		hauscmplem.6	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆))
9	8	eldifad 3586	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
10	9	ad3antrrr 766	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝐴 ∈ 𝑋)
11	5	clstop 20873	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
12	4, 11	syl 17	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = 𝑋)
13		simplr 792	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∪ 𝑥)
14		unieq 4444	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∪ ∅)
15		uni0 4465	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
16	14, 15	syl6eq 2672	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∅)
17	16	adantl 482	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ∪ 𝑥 = ∅)
18	13, 17	sseqtrd 3641	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∅)
19		ss0 3974	. . . . . . . . 9 ⊢ (𝑆 ⊆ ∅ → 𝑆 = ∅)
20	18, 19	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 = ∅)
21	20	difeq2d 3728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → (𝑋 ∖ 𝑆) = (𝑋 ∖ ∅))
22		dif0 3950	. . . . . . 7 ⊢ (𝑋 ∖ ∅) = 𝑋
23	21, 22	syl6eq 2672	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → (𝑋 ∖ 𝑆) = 𝑋)
24	12, 23	eqtr4d 2659	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = (𝑋 ∖ 𝑆))
25		eqimss 3657	. . . . 5 ⊢ (((cls‘𝐽)‘𝑋) = (𝑋 ∖ 𝑆) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))
26	24, 25	syl 17	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))
27		eleq2 2690	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋))
28		fveq2 6191	. . . . . . 7 ⊢ (𝑧 = 𝑋 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘𝑋))
29	28	sseq1d 3632	. . . . . 6 ⊢ (𝑧 = 𝑋 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆) ↔ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆)))
30	27, 29	anbi12d 747	. . . . 5 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)) ↔ (𝐴 ∈ 𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))))
31	30	rspcev 3309	. . . 4 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝐴 ∈ 𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
32	7, 10, 26, 31	syl12anc 1324	. . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
33		elin 3796	. . . . . . 7 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin))
34		id 22	. . . . . . . 8 ⊢ (𝑥 ∈ Fin → 𝑥 ∈ Fin)
35		elpwi 4168	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝑂 → 𝑥 ⊆ 𝑂)
36	35	sseld 3602	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝒫 𝑂 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑂))
37		difeq2 3722	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑧))
38	37	sseq2d 3633	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦) ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
39	38	anbi2d 740	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → ((𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) ↔ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
40	39	rexbidv 3052	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) ↔ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
41		hauscmplem.2	. . . . . . . . . . . 12 ⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}
42	40, 41	elrab2 3366	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑂 ↔ (𝑧 ∈ 𝐽 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
43	42	simprbi 480	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑂 → ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
44	36, 43	syl6 35	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝑂 → (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
45	44	ralrimiv 2965	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝑂 → ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
46		eleq2 2690	. . . . . . . . . 10 ⊢ (𝑤 = (𝑓‘𝑧) → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ (𝑓‘𝑧)))
47		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑓‘𝑧) → ((cls‘𝐽)‘𝑤) = ((cls‘𝐽)‘(𝑓‘𝑧)))
48	47	sseq1d 3632	. . . . . . . . . 10 ⊢ (𝑤 = (𝑓‘𝑧) → (((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧) ↔ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))
49	46, 48	anbi12d 747	. . . . . . . . 9 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)) ↔ (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
50	49	ac6sfi 8204	. . . . . . . 8 ⊢ ((𝑥 ∈ Fin ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
51	34, 45, 50	syl2anr 495	. . . . . . 7 ⊢ ((𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
52	33, 51	sylbi 207	. . . . . 6 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
53	52	ad2antlr 763	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
54	3	ad3antrrr 766	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐽 ∈ Top)
55		frn 6053	. . . . . . . 8 ⊢ (𝑓:𝑥⟶𝐽 → ran 𝑓 ⊆ 𝐽)
56	55	ad2antrl 764	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ⊆ 𝐽)
57		simprr 796	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → 𝑥 ≠ ∅)
58		simpl 473	. . . . . . . 8 ⊢ ((𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) → 𝑓:𝑥⟶𝐽)
59		dm0rn0 5342	. . . . . . . . . . 11 ⊢ (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
60		fdm 6051	. . . . . . . . . . . 12 ⊢ (𝑓:𝑥⟶𝐽 → dom 𝑓 = 𝑥)
61	60	eqeq1d 2624	. . . . . . . . . . 11 ⊢ (𝑓:𝑥⟶𝐽 → (dom 𝑓 = ∅ ↔ 𝑥 = ∅))
62	59, 61	syl5rbbr 275	. . . . . . . . . 10 ⊢ (𝑓:𝑥⟶𝐽 → (𝑥 = ∅ ↔ ran 𝑓 = ∅))
63	62	necon3bid 2838	. . . . . . . . 9 ⊢ (𝑓:𝑥⟶𝐽 → (𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅))
64	63	biimpac 503	. . . . . . . 8 ⊢ ((𝑥 ≠ ∅ ∧ 𝑓:𝑥⟶𝐽) → ran 𝑓 ≠ ∅)
65	57, 58, 64	syl2an 494	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ≠ ∅)
66	33	simprbi 480	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → 𝑥 ∈ Fin)
67	66	ad2antlr 763	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ Fin)
68		ffn 6045	. . . . . . . . . 10 ⊢ (𝑓:𝑥⟶𝐽 → 𝑓 Fn 𝑥)
69		dffn4 6121	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ 𝑓:𝑥–onto→ran 𝑓)
70	68, 69	sylib 208	. . . . . . . . 9 ⊢ (𝑓:𝑥⟶𝐽 → 𝑓:𝑥–onto→ran 𝑓)
71	70	adantr 481	. . . . . . . 8 ⊢ ((𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) → 𝑓:𝑥–onto→ran 𝑓)
72		fofi 8252	. . . . . . . 8 ⊢ ((𝑥 ∈ Fin ∧ 𝑓:𝑥–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
73	67, 71, 72	syl2an 494	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ∈ Fin)
74		fiinopn 20706	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ∩ ran 𝑓 ∈ 𝐽))
75	74	imp 445	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ∩ ran 𝑓 ∈ 𝐽)
76	54, 56, 65, 73, 75	syl13anc 1328	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 ∈ 𝐽)
77		simpl 473	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → 𝐴 ∈ (𝑓‘𝑧))
78	77	ralimi 2952	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧))
79	78	ad2antll 765	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧))
80	8	ad3antrrr 766	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ (𝑋 ∖ 𝑆))
81		eliin 4525	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑋 ∖ 𝑆) → (𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧)))
82	80, 81	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → (𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧)))
83	79, 82	mpbird 247	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
84	68	ad2antrl 764	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑓 Fn 𝑥)
85		fnrnfv 6242	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 → ran 𝑓 = {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)})
86	85	inteqd 4480	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑥 → ∩ ran 𝑓 = ∩ {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)})
87		fvex 6201	. . . . . . . . . 10 ⊢ (𝑓‘𝑧) ∈ V
88	87	dfiin2 4555	. . . . . . . . 9 ⊢ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) = ∩ {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)}
89	86, 88	syl6eqr 2674	. . . . . . . 8 ⊢ (𝑓 Fn 𝑥 → ∩ ran 𝑓 = ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
90	84, 89	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 = ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
91	83, 90	eleqtrrd 2704	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ ∩ ran 𝑓)
92	57	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑥 ≠ ∅)
93	3	ad4antr 768	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → 𝐽 ∈ Top)
94		ffvelrn 6357	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:𝑥⟶𝐽 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ 𝐽)
95	94	adantll 750	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ 𝐽)
96		elssuni 4467	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑧) ∈ 𝐽 → (𝑓‘𝑧) ⊆ ∪ 𝐽)
97	95, 96	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ ∪ 𝐽)
98	97, 5	syl6sseqr 3652	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ 𝑋)
99	5	clscld 20851	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ (𝑓‘𝑧) ⊆ 𝑋) → ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
100	93, 98, 99	syl2anc 693	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
101	100	ralrimiva 2966	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
102	101	adantrr 753	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
103		iincld 20843	. . . . . . . . 9 ⊢ ((𝑥 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
104	92, 102, 103	syl2anc 693	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
105	5	sscls 20860	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (𝑓‘𝑧) ⊆ 𝑋) → (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
106	93, 98, 105	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
107	106	ralrimiva 2966	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
108		ssel 3597	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (𝑦 ∈ (𝑓‘𝑧) → 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
109	108	ral2imi 2947	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧) → ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
110		vex 3203	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
111		eliin 4525	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧)))
112	110, 111	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧))
113		eliin 4525	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
114	110, 113	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)))
115	109, 112, 114	3imtr4g 285	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) → 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))))
116	115	ssrdv 3609	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
117	107, 116	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
118	117	adantrr 753	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
119	90, 118	eqsstrd 3639	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
120	5	clsss2 20876	. . . . . . . 8 ⊢ ((∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽) ∧ ∩ ran 𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
121	104, 119, 120	syl2anc 693	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
122		ssel 3597	. . . . . . . . . . . . 13 ⊢ (((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ (𝑋 ∖ 𝑧)))
123	122	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ (𝑋 ∖ 𝑧)))
124	123	ral2imi 2947	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧)))
125		eliin 4525	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧)))
126	110, 125	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧))
127	124, 114, 126	3imtr4g 285	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧)))
128	127	ssrdv 3609	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧))
129	128	ad2antll 765	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧))
130		iindif2 4589	. . . . . . . . . 10 ⊢ (𝑥 ≠ ∅ → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) = (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧))
131	92, 130	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) = (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧))
132		simplrl 800	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑆 ⊆ ∪ 𝑥)
133		uniiun 4573	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 = ∪ 𝑧 ∈ 𝑥 𝑧
134	133	sseq2i 3630	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ ∪ 𝑥 ↔ 𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧)
135		sscon 3744	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧 → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
136	134, 135	sylbi 207	. . . . . . . . . 10 ⊢ (𝑆 ⊆ ∪ 𝑥 → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
137	132, 136	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
138	131, 137	eqsstrd 3639	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑆))
139	129, 138	sstrd 3613	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑆))
140	121, 139	sstrd 3613	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))
141		eleq2 2690	. . . . . . . 8 ⊢ (𝑧 = ∩ ran 𝑓 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ ∩ ran 𝑓))
142		fveq2 6191	. . . . . . . . 9 ⊢ (𝑧 = ∩ ran 𝑓 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘∩ ran 𝑓))
143	142	sseq1d 3632	. . . . . . . 8 ⊢ (𝑧 = ∩ ran 𝑓 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆) ↔ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆)))
144	141, 143	anbi12d 747	. . . . . . 7 ⊢ (𝑧 = ∩ ran 𝑓 → ((𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)) ↔ (𝐴 ∈ ∩ ran 𝑓 ∧ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))))
145	144	rspcev 3309	. . . . . 6 ⊢ ((∩ ran 𝑓 ∈ 𝐽 ∧ (𝐴 ∈ ∩ ran 𝑓 ∧ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
146	76, 91, 140, 145	syl12anc 1324	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
147	53, 146	exlimddv 1863	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
148	147	anassrs 680	. . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
149	32, 148	pm2.61dane 2881	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
150	1	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ Haus)
151		hauscmplem.4	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⊆ 𝑋)
152	151	sselda 3603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑋)
153	9	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑋)
154		id 22	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ 𝑆)
155	8	eldifbd 3587	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝑆)
156		nelne2 2891	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑆 ∧ ¬ 𝐴 ∈ 𝑆) → 𝑥 ≠ 𝐴)
157	154, 155, 156	syl2anr 495	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≠ 𝐴)
158	5	hausnei 21132	. . . . . . . 8 ⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ≠ 𝐴)) → ∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅))
159	150, 152, 153, 157, 158	syl13anc 1328	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅))
160		3anass 1042	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) ↔ (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)))
161		elssuni 4467	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽)
162	161, 5	syl6sseqr 3652	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑋)
163	162	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → 𝑤 ⊆ 𝑋)
164		incom 3805	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∩ 𝑤) = (𝑤 ∩ 𝑦)
165	164	eqeq1i 2627	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∩ 𝑤) = ∅ ↔ (𝑤 ∩ 𝑦) = ∅)
166		reldisj 4020	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ⊆ 𝑋 → ((𝑤 ∩ 𝑦) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
167	165, 166	syl5bb 272	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ⊆ 𝑋 → ((𝑦 ∩ 𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
168	163, 167	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑦 ∩ 𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
169	150, 2	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ Top)
170	5	opncld 20837	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
171	169, 170	sylan 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
172	171	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
173	5	clsss2 20876	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽) ∧ 𝑤 ⊆ (𝑋 ∖ 𝑦)) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))
174	173	ex 450	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽) → (𝑤 ⊆ (𝑋 ∖ 𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
175	172, 174	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑤 ⊆ (𝑋 ∖ 𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
176	168, 175	sylbid 230	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑦 ∩ 𝑤) = ∅ → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
177	176	anim2d 589	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
178	177	anim2d 589	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)) → (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
179	160, 178	syl5bi 232	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
180	179	reximdva 3017	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
181		r19.42v 3092	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
182	180, 181	syl6ib 241	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
183	182	reximdva 3017	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
184	159, 183	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
185	41	unieqi 4445	. . . . . . . 8 ⊢ ∪ 𝑂 = ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}
186	185	eleq2i 2693	. . . . . . 7 ⊢ (𝑥 ∈ ∪ 𝑂 ↔ 𝑥 ∈ ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))})
187		elunirab 4448	. . . . . . 7 ⊢ (𝑥 ∈ ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))} ↔ ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
188	186, 187	bitri 264	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑂 ↔ ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
189	184, 188	sylibr 224	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ∪ 𝑂)
190	189	ex 450	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑂))
191	190	ssrdv 3609	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝑂)
192		ssrab2 3687	. . . . . 6 ⊢ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))} ⊆ 𝐽
193	41, 192	eqsstri 3635	. . . . 5 ⊢ 𝑂 ⊆ 𝐽
194		elpw2g 4827	. . . . . 6 ⊢ (𝐽 ∈ Haus → (𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽))
195	1, 194	syl 17	. . . . 5 ⊢ (𝜑 → (𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽))
196	193, 195	mpbiri 248	. . . 4 ⊢ (𝜑 → 𝑂 ∈ 𝒫 𝐽)
197		hauscmplem.5	. . . . 5 ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp)
198	5	cmpsub 21203	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥)))
199	198	biimp3a 1432	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ (𝐽 ↾t 𝑆) ∈ Comp) → ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
200	3, 151, 197, 199	syl3anc 1326	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
201		unieq 4444	. . . . . . 7 ⊢ (𝑧 = 𝑂 → ∪ 𝑧 = ∪ 𝑂)
202	201	sseq2d 3633	. . . . . 6 ⊢ (𝑧 = 𝑂 → (𝑆 ⊆ ∪ 𝑧 ↔ 𝑆 ⊆ ∪ 𝑂))
203		pweq 4161	. . . . . . . 8 ⊢ (𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂)
204	203	ineq1d 3813	. . . . . . 7 ⊢ (𝑧 = 𝑂 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑂 ∩ Fin))
205	204	rexeqdv 3145	. . . . . 6 ⊢ (𝑧 = 𝑂 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
206	202, 205	imbi12d 334	. . . . 5 ⊢ (𝑧 = 𝑂 → ((𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥) ↔ (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥)))
207	206	rspcva 3307	. . . 4 ⊢ ((𝑂 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥)) → (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
208	196, 200, 207	syl2anc 693	. . 3 ⊢ (𝜑 → (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
209	191, 208	mpd 15	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥)
210	149, 209	r19.29a 3078	1 ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483  ∃wex 1704   ∈ wcel 1990  {cab 2608   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200   ∖ cdif 3571   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  𝒫 cpw 4158  ∪ cuni 4436  ∩ cint 4475  ∪ ciun 4520  ∩ ciin 4521  dom cdm 5114  ran crn 5115   Fn wfn 5883  ⟶wf 5884  –onto→wfo 5886  ‘cfv 5888  (class class class)co 6650  Fincfn 7955   ↾_t crest 16081  Topctop 20698  Clsdccld 20820  clsccl 20822  Hauscha 21112  Compccmp 21189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-fin 7959  df-fi 8317  df-rest 16083  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-cls 20825  df-haus 21119  df-cmp 21190

This theorem is referenced by:  hauscmp  21210  hausllycmp  21297