Theorem hauscmplem 23415

Description: Lemma for hauscmp 23416. (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 23340	. . . . . . 7 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
4	3	ad3antrrr 730	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝐽 ∈ Top)
5		hauscmp.1	. . . . . 6 ⊢ 𝑋 = ∪ 𝐽
6	5	topopn 22913	. . . . 5 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
7	4, 6	syl 17	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑋 ∈ 𝐽)
8		hauscmplem.6	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆))
9	8	eldifad 3962	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
10	9	ad3antrrr 730	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝐴 ∈ 𝑋)
11	5	clstop 23078	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
12	4, 11	syl 17	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = 𝑋)
13		simplr 768	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∪ 𝑥)
14		unieq 4917	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∪ ∅)
15		uni0 4934	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
16	14, 15	eqtrdi 2792	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∅)
17	16	adantl 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ∪ 𝑥 = ∅)
18	13, 17	sseqtrd 4019	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∅)
19		ss0 4401	. . . . . . . . 9 ⊢ (𝑆 ⊆ ∅ → 𝑆 = ∅)
20	18, 19	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 = ∅)
21	20	difeq2d 4125	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → (𝑋 ∖ 𝑆) = (𝑋 ∖ ∅))
22		dif0 4377	. . . . . . 7 ⊢ (𝑋 ∖ ∅) = 𝑋
23	21, 22	eqtrdi 2792	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → (𝑋 ∖ 𝑆) = 𝑋)
24	12, 23	eqtr4d 2779	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = (𝑋 ∖ 𝑆))
25		eqimss 4041	. . . . 5 ⊢ (((cls‘𝐽)‘𝑋) = (𝑋 ∖ 𝑆) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))
26	24, 25	syl 17	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))
27		eleq2 2829	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋))
28		fveq2 6905	. . . . . . 7 ⊢ (𝑧 = 𝑋 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘𝑋))
29	28	sseq1d 4014	. . . . . 6 ⊢ (𝑧 = 𝑋 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆) ↔ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆)))
30	27, 29	anbi12d 632	. . . . 5 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)) ↔ (𝐴 ∈ 𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))))
31	30	rspcev 3621	. . . 4 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝐴 ∈ 𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
32	7, 10, 26, 31	syl12anc 836	. . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
33		elin 3966	. . . . . . 7 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin))
34		id 22	. . . . . . . 8 ⊢ (𝑥 ∈ Fin → 𝑥 ∈ Fin)
35		elpwi 4606	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝑂 → 𝑥 ⊆ 𝑂)
36	35	sseld 3981	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝒫 𝑂 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑂))
37		difeq2 4119	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑧))
38	37	sseq2d 4015	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦) ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
39	38	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → ((𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) ↔ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
40	39	rexbidv 3178	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) ↔ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
41		hauscmplem.2	. . . . . . . . . . . 12 ⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}
42	40, 41	elrab2 3694	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑂 ↔ (𝑧 ∈ 𝐽 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
43	42	simprbi 496	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑂 → ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
44	36, 43	syl6 35	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝑂 → (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
45	44	ralrimiv 3144	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝑂 → ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
46		eleq2 2829	. . . . . . . . . 10 ⊢ (𝑤 = (𝑓‘𝑧) → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ (𝑓‘𝑧)))
47		fveq2 6905	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑓‘𝑧) → ((cls‘𝐽)‘𝑤) = ((cls‘𝐽)‘(𝑓‘𝑧)))
48	47	sseq1d 4014	. . . . . . . . . 10 ⊢ (𝑤 = (𝑓‘𝑧) → (((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧) ↔ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))
49	46, 48	anbi12d 632	. . . . . . . . 9 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)) ↔ (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
50	49	ac6sfi 9321	. . . . . . . 8 ⊢ ((𝑥 ∈ Fin ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
51	34, 45, 50	syl2anr 597	. . . . . . 7 ⊢ ((𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
52	33, 51	sylbi 217	. . . . . 6 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
53	52	ad2antlr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
54	3	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐽 ∈ Top)
55		frn 6742	. . . . . . . 8 ⊢ (𝑓:𝑥⟶𝐽 → ran 𝑓 ⊆ 𝐽)
56	55	ad2antrl 728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ⊆ 𝐽)
57		simprr 772	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → 𝑥 ≠ ∅)
58		simpl 482	. . . . . . . 8 ⊢ ((𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) → 𝑓:𝑥⟶𝐽)
59		fdm 6744	. . . . . . . . . . . 12 ⊢ (𝑓:𝑥⟶𝐽 → dom 𝑓 = 𝑥)
60	59	eqeq1d 2738	. . . . . . . . . . 11 ⊢ (𝑓:𝑥⟶𝐽 → (dom 𝑓 = ∅ ↔ 𝑥 = ∅))
61		dm0rn0 5934	. . . . . . . . . . 11 ⊢ (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
62	60, 61	bitr3di 286	. . . . . . . . . 10 ⊢ (𝑓:𝑥⟶𝐽 → (𝑥 = ∅ ↔ ran 𝑓 = ∅))
63	62	necon3bid 2984	. . . . . . . . 9 ⊢ (𝑓:𝑥⟶𝐽 → (𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅))
64	63	biimpac 478	. . . . . . . 8 ⊢ ((𝑥 ≠ ∅ ∧ 𝑓:𝑥⟶𝐽) → ran 𝑓 ≠ ∅)
65	57, 58, 64	syl2an 596	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ≠ ∅)
66	33	simprbi 496	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → 𝑥 ∈ Fin)
67	66	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ Fin)
68		ffn 6735	. . . . . . . . . 10 ⊢ (𝑓:𝑥⟶𝐽 → 𝑓 Fn 𝑥)
69		dffn4 6825	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ 𝑓:𝑥–onto→ran 𝑓)
70	68, 69	sylib 218	. . . . . . . . 9 ⊢ (𝑓:𝑥⟶𝐽 → 𝑓:𝑥–onto→ran 𝑓)
71	70	adantr 480	. . . . . . . 8 ⊢ ((𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) → 𝑓:𝑥–onto→ran 𝑓)
72		fofi 9352	. . . . . . . 8 ⊢ ((𝑥 ∈ Fin ∧ 𝑓:𝑥–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
73	67, 71, 72	syl2an 596	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ∈ Fin)
74		fiinopn 22908	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ∩ ran 𝑓 ∈ 𝐽))
75	74	imp 406	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ∩ ran 𝑓 ∈ 𝐽)
76	54, 56, 65, 73, 75	syl13anc 1373	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 ∈ 𝐽)
77		simpl 482	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → 𝐴 ∈ (𝑓‘𝑧))
78	77	ralimi 3082	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧))
79	78	ad2antll 729	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧))
80	8	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ (𝑋 ∖ 𝑆))
81		eliin 4995	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑋 ∖ 𝑆) → (𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧)))
82	80, 81	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → (𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧)))
83	79, 82	mpbird 257	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
84	68	ad2antrl 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑓 Fn 𝑥)
85		fnrnfv 6967	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 → ran 𝑓 = {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)})
86	85	inteqd 4950	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑥 → ∩ ran 𝑓 = ∩ {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)})
87		fvex 6918	. . . . . . . . . 10 ⊢ (𝑓‘𝑧) ∈ V
88	87	dfiin2 5033	. . . . . . . . 9 ⊢ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) = ∩ {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)}
89	86, 88	eqtr4di 2794	. . . . . . . 8 ⊢ (𝑓 Fn 𝑥 → ∩ ran 𝑓 = ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
90	84, 89	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 = ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
91	83, 90	eleqtrrd 2843	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ ∩ ran 𝑓)
92	57	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑥 ≠ ∅)
93	3	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → 𝐽 ∈ Top)
94		ffvelcdm 7100	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:𝑥⟶𝐽 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ 𝐽)
95	94	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ 𝐽)
96		elssuni 4936	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑧) ∈ 𝐽 → (𝑓‘𝑧) ⊆ ∪ 𝐽)
97	95, 96	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ ∪ 𝐽)
98	97, 5	sseqtrrdi 4024	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ 𝑋)
99	5	clscld 23056	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ (𝑓‘𝑧) ⊆ 𝑋) → ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
100	93, 98, 99	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
101	100	ralrimiva 3145	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
102	101	adantrr 717	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
103		iincld 23048	. . . . . . . . 9 ⊢ ((𝑥 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
104	92, 102, 103	syl2anc 584	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
105	5	sscls 23065	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (𝑓‘𝑧) ⊆ 𝑋) → (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
106	93, 98, 105	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
107	106	ralrimiva 3145	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
108		ssel 3976	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (𝑦 ∈ (𝑓‘𝑧) → 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
109	108	ral2imi 3084	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧) → ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
110		eliin 4995	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧)))
111	110	elv 3484	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧))
112		eliin 4995	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
113	112	elv 3484	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)))
114	109, 111, 113	3imtr4g 296	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) → 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))))
115	114	ssrdv 3988	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
116	107, 115	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
117	116	adantrr 717	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
118	90, 117	eqsstrd 4017	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
119	5	clsss2 23081	. . . . . . . 8 ⊢ ((∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽) ∧ ∩ ran 𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
120	104, 118, 119	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
121		ssel 3976	. . . . . . . . . . . . 13 ⊢ (((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ (𝑋 ∖ 𝑧)))
122	121	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ (𝑋 ∖ 𝑧)))
123	122	ral2imi 3084	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧)))
124		eliin 4995	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧)))
125	124	elv 3484	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧))
126	123, 113, 125	3imtr4g 296	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧)))
127	126	ssrdv 3988	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧))
128	127	ad2antll 729	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧))
129		iindif2 5076	. . . . . . . . . 10 ⊢ (𝑥 ≠ ∅ → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) = (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧))
130	92, 129	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) = (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧))
131		simplrl 776	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑆 ⊆ ∪ 𝑥)
132		uniiun 5057	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 = ∪ 𝑧 ∈ 𝑥 𝑧
133	132	sseq2i 4012	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ ∪ 𝑥 ↔ 𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧)
134		sscon 4142	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧 → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
135	133, 134	sylbi 217	. . . . . . . . . 10 ⊢ (𝑆 ⊆ ∪ 𝑥 → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
136	131, 135	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
137	130, 136	eqsstrd 4017	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑆))
138	128, 137	sstrd 3993	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑆))
139	120, 138	sstrd 3993	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))
140		eleq2 2829	. . . . . . . 8 ⊢ (𝑧 = ∩ ran 𝑓 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ ∩ ran 𝑓))
141		fveq2 6905	. . . . . . . . 9 ⊢ (𝑧 = ∩ ran 𝑓 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘∩ ran 𝑓))
142	141	sseq1d 4014	. . . . . . . 8 ⊢ (𝑧 = ∩ ran 𝑓 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆) ↔ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆)))
143	140, 142	anbi12d 632	. . . . . . 7 ⊢ (𝑧 = ∩ ran 𝑓 → ((𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)) ↔ (𝐴 ∈ ∩ ran 𝑓 ∧ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))))
144	143	rspcev 3621	. . . . . 6 ⊢ ((∩ ran 𝑓 ∈ 𝐽 ∧ (𝐴 ∈ ∩ ran 𝑓 ∧ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
145	76, 91, 139, 144	syl12anc 836	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
146	53, 145	exlimddv 1934	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
147	146	anassrs 467	. . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
148	32, 147	pm2.61dane 3028	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
149	1	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ Haus)
150		hauscmplem.4	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⊆ 𝑋)
151	150	sselda 3982	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑋)
152	9	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑋)
153		id 22	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ 𝑆)
154	8	eldifbd 3963	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝑆)
155		nelne2 3039	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑆 ∧ ¬ 𝐴 ∈ 𝑆) → 𝑥 ≠ 𝐴)
156	153, 154, 155	syl2anr 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≠ 𝐴)
157	5	hausnei 23337	. . . . . . . 8 ⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ≠ 𝐴)) → ∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅))
158	149, 151, 152, 156, 157	syl13anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅))
159		3anass 1094	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) ↔ (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)))
160		elssuni 4936	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽)
161	160, 5	sseqtrrdi 4024	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑋)
162	161	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → 𝑤 ⊆ 𝑋)
163		incom 4208	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∩ 𝑤) = (𝑤 ∩ 𝑦)
164	163	eqeq1i 2741	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∩ 𝑤) = ∅ ↔ (𝑤 ∩ 𝑦) = ∅)
165		reldisj 4452	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ⊆ 𝑋 → ((𝑤 ∩ 𝑦) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
166	164, 165	bitrid 283	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ⊆ 𝑋 → ((𝑦 ∩ 𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
167	162, 166	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑦 ∩ 𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
168	149, 2	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ Top)
169	5	opncld 23042	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
170	168, 169	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
171	170	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
172	5	clsss2 23081	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽) ∧ 𝑤 ⊆ (𝑋 ∖ 𝑦)) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))
173	172	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽) → (𝑤 ⊆ (𝑋 ∖ 𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
174	171, 173	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑤 ⊆ (𝑋 ∖ 𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
175	167, 174	sylbid 240	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑦 ∩ 𝑤) = ∅ → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
176	175	anim2d 612	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
177	176	anim2d 612	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)) → (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
178	159, 177	biimtrid 242	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
179	178	reximdva 3167	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
180		r19.42v 3190	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
181	179, 180	imbitrdi 251	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
182	181	reximdva 3167	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
183	158, 182	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
184	41	unieqi 4918	. . . . . . . 8 ⊢ ∪ 𝑂 = ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}
185	184	eleq2i 2832	. . . . . . 7 ⊢ (𝑥 ∈ ∪ 𝑂 ↔ 𝑥 ∈ ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))})
186		elunirab 4921	. . . . . . 7 ⊢ (𝑥 ∈ ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))} ↔ ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
187	185, 186	bitri 275	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑂 ↔ ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
188	183, 187	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ∪ 𝑂)
189	188	ex 412	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑂))
190	189	ssrdv 3988	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝑂)
191		unieq 4917	. . . . . 6 ⊢ (𝑧 = 𝑂 → ∪ 𝑧 = ∪ 𝑂)
192	191	sseq2d 4015	. . . . 5 ⊢ (𝑧 = 𝑂 → (𝑆 ⊆ ∪ 𝑧 ↔ 𝑆 ⊆ ∪ 𝑂))
193		pweq 4613	. . . . . . 7 ⊢ (𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂)
194	193	ineq1d 4218	. . . . . 6 ⊢ (𝑧 = 𝑂 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑂 ∩ Fin))
195	194	rexeqdv 3326	. . . . 5 ⊢ (𝑧 = 𝑂 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
196	192, 195	imbi12d 344	. . . 4 ⊢ (𝑧 = 𝑂 → ((𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥) ↔ (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥)))
197		hauscmplem.5	. . . . 5 ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp)
198	5	cmpsub 23409	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥)))
199	198	biimp3a 1470	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ (𝐽 ↾t 𝑆) ∈ Comp) → ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
200	3, 150, 197, 199	syl3anc 1372	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
201	41	ssrab3 4081	. . . . 5 ⊢ 𝑂 ⊆ 𝐽
202		elpw2g 5332	. . . . . 6 ⊢ (𝐽 ∈ Haus → (𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽))
203	1, 202	syl 17	. . . . 5 ⊢ (𝜑 → (𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽))
204	201, 203	mpbiri 258	. . . 4 ⊢ (𝜑 → 𝑂 ∈ 𝒫 𝐽)
205	196, 200, 204	rspcdva 3622	. . 3 ⊢ (𝜑 → (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
206	190, 205	mpd 15	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥)
207	148, 206	r19.29a 3161	1 ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539  ∃wex 1778   ∈ wcel 2107  {cab 2713   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  {crab 3435  Vcvv 3479   ∖ cdif 3947   ∩ cin 3949   ⊆ wss 3950  ∅c0 4332  𝒫 cpw 4599  ∪ cuni 4906  ∩ cint 4945  ∪ ciun 4990  ∩ ciin 4991  dom cdm 5684  ran crn 5685   Fn wfn 6555  ⟶wf 6556  –onto→wfo 6558  ‘cfv 6560  (class class class)co 7432  Fincfn 8986   ↾_t crest 17466  Topctop 22900  Clsdccld 23025  clsccl 23027  Hauscha 23317  Compccmp 23395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-1o 8507  df-2o 8508  df-en 8987  df-dom 8988  df-fin 8990  df-fi 9452  df-rest 17468  df-topgen 17489  df-top 22901  df-topon 22918  df-bases 22954  df-cld 23028  df-cls 23030  df-haus 23324  df-cmp 23396

This theorem is referenced by:  hauscmp  23416  hausllycmp  23503