Theorem hauscmplem 23435

Description: Lemma for hauscmp 23436. (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 23360	. . . . . . 7 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
4	3	ad3antrrr 738	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝐽 ∈ Top)
5		hauscmp.1	. . . . . 6 ⊢ 𝑋 = ∪ 𝐽
6	5	topopn 22935	. . . . 5 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
7	4, 6	syl 17	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑋 ∈ 𝐽)
8		hauscmplem.6	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆))
9	8	eldifad 3907	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
10	9	ad3antrrr 738	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝐴 ∈ 𝑋)
11	5	clstop 23098	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
12	4, 11	syl 17	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = 𝑋)
13		simplr 776	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∪ 𝑥)
14		unieq 4866	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∪ ∅)
15		uni0 4884	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
16	14, 15	eqtrdi 2803	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∅)
17	16	adantl 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ∪ 𝑥 = ∅)
18	13, 17	sseqtrd 3963	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∅)
19		ss0 4346	. . . . . . . . 9 ⊢ (𝑆 ⊆ ∅ → 𝑆 = ∅)
20	18, 19	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 = ∅)
21	20	difeq2d 4071	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → (𝑋 ∖ 𝑆) = (𝑋 ∖ ∅))
22		dif0 4321	. . . . . . 7 ⊢ (𝑋 ∖ ∅) = 𝑋
23	21, 22	eqtrdi 2803	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → (𝑋 ∖ 𝑆) = 𝑋)
24	12, 23	eqtr4d 2790	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = (𝑋 ∖ 𝑆))
25		eqimss 3985	. . . . 5 ⊢ (((cls‘𝐽)‘𝑋) = (𝑋 ∖ 𝑆) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))
26	24, 25	syl 17	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))
27		eleq2 2841	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋))
28		fveq2 6852	. . . . . . 7 ⊢ (𝑧 = 𝑋 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘𝑋))
29	28	sseq1d 3958	. . . . . 6 ⊢ (𝑧 = 𝑋 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆) ↔ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆)))
30	27, 29	anbi12d 640	. . . . 5 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)) ↔ (𝐴 ∈ 𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))))
31	30	rspcev 3572	. . . 4 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝐴 ∈ 𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
32	7, 10, 26, 31	syl12anc 845	. . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
33		elin 3911	. . . . . . 7 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin))
34		id 22	. . . . . . . 8 ⊢ (𝑥 ∈ Fin → 𝑥 ∈ Fin)
35		elpwi 4552	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝑂 → 𝑥 ⊆ 𝑂)
36	35	sseld 3926	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝒫 𝑂 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑂))
37		difeq2 4065	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑧))
38	37	sseq2d 3959	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦) ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
39	38	anbi2d 638	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → ((𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) ↔ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
40	39	rexbidv 3176	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) ↔ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
41		hauscmplem.2	. . . . . . . . . . . 12 ⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}
42	40, 41	elrab2 3644	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑂 ↔ (𝑧 ∈ 𝐽 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
43	42	simprbi 500	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑂 → ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
44	36, 43	syl6 35	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝑂 → (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
45	44	ralrimiv 3143	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝑂 → ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
46		eleq2 2841	. . . . . . . . . 10 ⊢ (𝑤 = (𝑓‘𝑧) → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ (𝑓‘𝑧)))
47		fveq2 6852	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑓‘𝑧) → ((cls‘𝐽)‘𝑤) = ((cls‘𝐽)‘(𝑓‘𝑧)))
48	47	sseq1d 3958	. . . . . . . . . 10 ⊢ (𝑤 = (𝑓‘𝑧) → (((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧) ↔ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))
49	46, 48	anbi12d 640	. . . . . . . . 9 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)) ↔ (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
50	49	ac6sfi 9213	. . . . . . . 8 ⊢ ((𝑥 ∈ Fin ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
51	34, 45, 50	syl2anr 605	. . . . . . 7 ⊢ ((𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
52	33, 51	sylbi 219	. . . . . 6 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
53	52	ad2antlr 735	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
54	3	ad3antrrr 738	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐽 ∈ Top)
55		frn 6684	. . . . . . . 8 ⊢ (𝑓:𝑥⟶𝐽 → ran 𝑓 ⊆ 𝐽)
56	55	ad2antrl 736	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ⊆ 𝐽)
57		simprr 780	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → 𝑥 ≠ ∅)
58		simpl 485	. . . . . . . 8 ⊢ ((𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) → 𝑓:𝑥⟶𝐽)
59		fdm 6686	. . . . . . . . . . . 12 ⊢ (𝑓:𝑥⟶𝐽 → dom 𝑓 = 𝑥)
60	59	eqeq1d 2754	. . . . . . . . . . 11 ⊢ (𝑓:𝑥⟶𝐽 → (dom 𝑓 = ∅ ↔ 𝑥 = ∅))
61		dm0rn0 5889	. . . . . . . . . . 11 ⊢ (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
62	60, 61	bitr3di 288	. . . . . . . . . 10 ⊢ (𝑓:𝑥⟶𝐽 → (𝑥 = ∅ ↔ ran 𝑓 = ∅))
63	62	necon3bid 2991	. . . . . . . . 9 ⊢ (𝑓:𝑥⟶𝐽 → (𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅))
64	63	biimpac 481	. . . . . . . 8 ⊢ ((𝑥 ≠ ∅ ∧ 𝑓:𝑥⟶𝐽) → ran 𝑓 ≠ ∅)
65	57, 58, 64	syl2an 604	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ≠ ∅)
66	33	simprbi 500	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → 𝑥 ∈ Fin)
67	66	ad2antlr 735	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ Fin)
68		ffn 6676	. . . . . . . . . 10 ⊢ (𝑓:𝑥⟶𝐽 → 𝑓 Fn 𝑥)
69		dffn4 6769	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ 𝑓:𝑥–onto→ran 𝑓)
70	68, 69	sylib 220	. . . . . . . . 9 ⊢ (𝑓:𝑥⟶𝐽 → 𝑓:𝑥–onto→ran 𝑓)
71	70	adantr 483	. . . . . . . 8 ⊢ ((𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) → 𝑓:𝑥–onto→ran 𝑓)
72		fofi 9242	. . . . . . . 8 ⊢ ((𝑥 ∈ Fin ∧ 𝑓:𝑥–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
73	67, 71, 72	syl2an 604	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ∈ Fin)
74		fiinopn 22930	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ∩ ran 𝑓 ∈ 𝐽))
75	74	imp 409	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ∩ ran 𝑓 ∈ 𝐽)
76	54, 56, 65, 73, 75	syl13anc 1383	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 ∈ 𝐽)
77		simpl 485	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → 𝐴 ∈ (𝑓‘𝑧))
78	77	ralimi 3089	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧))
79	78	ad2antll 737	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧))
80	8	ad3antrrr 738	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ (𝑋 ∖ 𝑆))
81		eliin 4944	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑋 ∖ 𝑆) → (𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧)))
82	80, 81	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → (𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧)))
83	79, 82	mpbird 259	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
84	68	ad2antrl 736	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑓 Fn 𝑥)
85		fnrnfv 6911	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 → ran 𝑓 = {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)})
86	85	inteqd 4900	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑥 → ∩ ran 𝑓 = ∩ {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)})
87		fvex 6865	. . . . . . . . . 10 ⊢ (𝑓‘𝑧) ∈ V
88	87	dfiin2 4980	. . . . . . . . 9 ⊢ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) = ∩ {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)}
89	86, 88	eqtr4di 2805	. . . . . . . 8 ⊢ (𝑓 Fn 𝑥 → ∩ ran 𝑓 = ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
90	84, 89	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 = ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
91	83, 90	eleqtrrd 2855	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ ∩ ran 𝑓)
92	57	adantr 483	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑥 ≠ ∅)
93	3	ad4antr 740	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → 𝐽 ∈ Top)
94		ffvelcdm 7047	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:𝑥⟶𝐽 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ 𝐽)
95	94	adantll 722	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ 𝐽)
96		elssuni 4887	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑧) ∈ 𝐽 → (𝑓‘𝑧) ⊆ ∪ 𝐽)
97	95, 96	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ ∪ 𝐽)
98	97, 5	sseqtrrdi 3968	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ 𝑋)
99	5	clscld 23076	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ (𝑓‘𝑧) ⊆ 𝑋) → ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
100	93, 98, 99	syl2anc 592	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
101	100	ralrimiva 3144	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
102	101	adantrr 725	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
103		iincld 23068	. . . . . . . . 9 ⊢ ((𝑥 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
104	92, 102, 103	syl2anc 592	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
105	5	sscls 23085	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (𝑓‘𝑧) ⊆ 𝑋) → (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
106	93, 98, 105	syl2anc 592	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
107	106	ralrimiva 3144	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
108		ssel 3921	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (𝑦 ∈ (𝑓‘𝑧) → 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
109	108	ral2imi 3091	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧) → ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
110		eliin 4944	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧)))
111	110	elv 3449	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧))
112		eliin 4944	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
113	112	elv 3449	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)))
114	109, 111, 113	3imtr4g 298	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) → 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))))
115	114	ssrdv 3933	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
116	107, 115	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
117	116	adantrr 725	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
118	90, 117	eqsstrd 3961	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
119	5	clsss2 23101	. . . . . . . 8 ⊢ ((∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽) ∧ ∩ ran 𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
120	104, 118, 119	syl2anc 592	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
121		ssel 3921	. . . . . . . . . . . . 13 ⊢ (((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ (𝑋 ∖ 𝑧)))
122	121	adantl 484	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ (𝑋 ∖ 𝑧)))
123	122	ral2imi 3091	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧)))
124		eliin 4944	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧)))
125	124	elv 3449	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧))
126	123, 113, 125	3imtr4g 298	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧)))
127	126	ssrdv 3933	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧))
128	127	ad2antll 737	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧))
129		iindif2 5024	. . . . . . . . . 10 ⊢ (𝑥 ≠ ∅ → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) = (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧))
130	92, 129	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) = (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧))
131		simplrl 784	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑆 ⊆ ∪ 𝑥)
132		uniiun 5006	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 = ∪ 𝑧 ∈ 𝑥 𝑧
133	132	sseq2i 3956	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ ∪ 𝑥 ↔ 𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧)
134		sscon 4087	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧 → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
135	133, 134	sylbi 219	. . . . . . . . . 10 ⊢ (𝑆 ⊆ ∪ 𝑥 → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
136	131, 135	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
137	130, 136	eqsstrd 3961	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑆))
138	128, 137	sstrd 3937	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑆))
139	120, 138	sstrd 3937	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))
140		eleq2 2841	. . . . . . . 8 ⊢ (𝑧 = ∩ ran 𝑓 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ ∩ ran 𝑓))
141		fveq2 6852	. . . . . . . . 9 ⊢ (𝑧 = ∩ ran 𝑓 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘∩ ran 𝑓))
142	141	sseq1d 3958	. . . . . . . 8 ⊢ (𝑧 = ∩ ran 𝑓 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆) ↔ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆)))
143	140, 142	anbi12d 640	. . . . . . 7 ⊢ (𝑧 = ∩ ran 𝑓 → ((𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)) ↔ (𝐴 ∈ ∩ ran 𝑓 ∧ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))))
144	143	rspcev 3572	. . . . . 6 ⊢ ((∩ ran 𝑓 ∈ 𝐽 ∧ (𝐴 ∈ ∩ ran 𝑓 ∧ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
145	76, 91, 139, 144	syl12anc 845	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
146	53, 145	exlimddv 1945	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
147	146	anassrs 470	. . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
148	32, 147	pm2.61dane 3034	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
149	1	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ Haus)
150		hauscmplem.4	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⊆ 𝑋)
151	150	sselda 3927	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑋)
152	9	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑋)
153		id 22	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ 𝑆)
154	8	eldifbd 3908	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝑆)
155		nelne2 3045	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑆 ∧ ¬ 𝐴 ∈ 𝑆) → 𝑥 ≠ 𝐴)
156	153, 154, 155	syl2anr 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≠ 𝐴)
157	5	hausnei 23357	. . . . . . . 8 ⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ≠ 𝐴)) → ∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅))
158	149, 151, 152, 156, 157	syl13anc 1383	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅))
159		3anass 1103	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) ↔ (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)))
160		elssuni 4887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽)
161	160, 5	sseqtrrdi 3968	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑋)
162	161	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → 𝑤 ⊆ 𝑋)
163		incom 4152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∩ 𝑤) = (𝑤 ∩ 𝑦)
164	163	eqeq1i 2757	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∩ 𝑤) = ∅ ↔ (𝑤 ∩ 𝑦) = ∅)
165		reldisj 4397	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ⊆ 𝑋 → ((𝑤 ∩ 𝑦) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
166	164, 165	bitrid 285	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ⊆ 𝑋 → ((𝑦 ∩ 𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
167	162, 166	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑦 ∩ 𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
168	149, 2	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ Top)
169	5	opncld 23062	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
170	168, 169	sylan 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
171	170	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
172	5	clsss2 23101	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽) ∧ 𝑤 ⊆ (𝑋 ∖ 𝑦)) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))
173	172	ex 415	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽) → (𝑤 ⊆ (𝑋 ∖ 𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
174	171, 173	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑤 ⊆ (𝑋 ∖ 𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
175	167, 174	sylbid 242	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑦 ∩ 𝑤) = ∅ → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
176	175	anim2d 620	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
177	176	anim2d 620	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)) → (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
178	159, 177	biimtrid 244	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
179	178	reximdva 3165	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
180		r19.42v 3184	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
181	179, 180	imbitrdi 253	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
182	181	reximdva 3165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
183	158, 182	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
184	41	unieqi 4867	. . . . . . . 8 ⊢ ∪ 𝑂 = ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}
185	184	eleq2i 2844	. . . . . . 7 ⊢ (𝑥 ∈ ∪ 𝑂 ↔ 𝑥 ∈ ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))})
186		elunirab 4870	. . . . . . 7 ⊢ (𝑥 ∈ ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))} ↔ ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
187	185, 186	bitri 277	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑂 ↔ ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
188	183, 187	sylibr 236	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ∪ 𝑂)
189	188	ex 415	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑂))
190	189	ssrdv 3933	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝑂)
191		unieq 4866	. . . . . 6 ⊢ (𝑧 = 𝑂 → ∪ 𝑧 = ∪ 𝑂)
192	191	sseq2d 3959	. . . . 5 ⊢ (𝑧 = 𝑂 → (𝑆 ⊆ ∪ 𝑧 ↔ 𝑆 ⊆ ∪ 𝑂))
193		pweq 4559	. . . . . . 7 ⊢ (𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂)
194	193	ineq1d 4162	. . . . . 6 ⊢ (𝑧 = 𝑂 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑂 ∩ Fin))
195	194	rexeqdv 3311	. . . . 5 ⊢ (𝑧 = 𝑂 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
196	192, 195	imbi12d 346	. . . 4 ⊢ (𝑧 = 𝑂 → ((𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥) ↔ (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥)))
197		hauscmplem.5	. . . . 5 ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp)
198	5	cmpsub 23429	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥)))
199	198	biimp3a 1480	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ (𝐽 ↾t 𝑆) ∈ Comp) → ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
200	3, 150, 197, 199	syl3anc 1382	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
201	41	ssrab3 4026	. . . . 5 ⊢ 𝑂 ⊆ 𝐽
202		elpw2g 5279	. . . . . 6 ⊢ (𝐽 ∈ Haus → (𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽))
203	1, 202	syl 17	. . . . 5 ⊢ (𝜑 → (𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽))
204	201, 203	mpbiri 260	. . . 4 ⊢ (𝜑 → 𝑂 ∈ 𝒫 𝐽)
205	196, 200, 204	rspcdva 3573	. . 3 ⊢ (𝜑 → (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
206	190, 205	mpd 15	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥)
207	148, 206	r19.29a 3160	1 ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1095   = wceq 1550  ∃wex 1789   ∈ wcel 2132  {cab 2730   ≠ wne 2947  ∀wral 3066  ∃wrex 3076  {crab 3404  Vcvv 3444   ∖ cdif 3892   ∩ cin 3894   ⊆ wss 3895  ∅c0 4276  𝒫 cpw 4545  ∪ cuni 4855  ∩ cint 4895  ∪ ciun 4939  ∩ ciin 4940  dom cdm 5636  ran crn 5637   Fn wfn 6501  ⟶wf 6502  –onto→wfo 6504  ‘cfv 6506  (class class class)co 7381  Fincfn 8912   ↾_t crest 17421  Topctop 22922  Clsdccld 23045  clsccl 23047  Hauscha 23337  Compccmp 23415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-rep 5217  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-reu 3358  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-pss 3915  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-int 4896  df-iun 4941  df-iin 4942  df-br 5091  df-opab 5153  df-mpt 5172  df-tr 5198  df-id 5531  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5589  df-we 5591  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-ord 6334  df-on 6335  df-lim 6336  df-suc 6337  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-ov 7384  df-oprab 7385  df-mpo 7386  df-om 7832  df-1st 7955  df-2nd 7956  df-1o 8421  df-2o 8422  df-en 8913  df-dom 8914  df-fin 8916  df-fi 9343  df-rest 17423  df-topgen 17444  df-top 22923  df-topon 22940  df-bases 22975  df-cld 23048  df-cls 23050  df-haus 23344  df-cmp 23416

This theorem is referenced by:  hauscmp  23436  hausllycmp  23523