Theorem hauscmplem 23574

Description: Lemma for hauscmp 23575. (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 23499	. . . . . . 7 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
3	1, 2	syl 18	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Top)
4	3	ad3antrrr 742	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝐽 ∈ Top)
5		hauscmp.1	. . . . . 6 ⊢ 𝑋 = ∪ 𝐽
6	5	topopn 23074	. . . . 5 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
7	4, 6	syl 18	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑋 ∈ 𝐽)
8		hauscmplem.6	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆))
9	8	eldifad 3916	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
10	9	ad3antrrr 742	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝐴 ∈ 𝑋)
11	5	clstop 23237	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
12	4, 11	syl 18	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = 𝑋)
13		simplr 780	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∪ 𝑥)
14		unieq 4882	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∪ ∅)
15		uni0 4900	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
16	14, 15	eqtrdi 2813	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∅)
17	16	adantl 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ∪ 𝑥 = ∅)
18	13, 17	sseqtrd 3972	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∅)
19		ss0 4358	. . . . . . . . 9 ⊢ (𝑆 ⊆ ∅ → 𝑆 = ∅)
20	18, 19	syl 18	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 = ∅)
21	20	difeq2d 4080	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → (𝑋 ∖ 𝑆) = (𝑋 ∖ ∅))
22		dif0 4333	. . . . . . 7 ⊢ (𝑋 ∖ ∅) = 𝑋
23	21, 22	eqtrdi 2813	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → (𝑋 ∖ 𝑆) = 𝑋)
24	12, 23	eqtr4d 2800	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = (𝑋 ∖ 𝑆))
25		eqimss 3994	. . . . 5 ⊢ (((cls‘𝐽)‘𝑋) = (𝑋 ∖ 𝑆) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))
26	24, 25	syl 18	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))
27		eleq2 2851	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋))
28		fveq2 6881	. . . . . . 7 ⊢ (𝑧 = 𝑋 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘𝑋))
29	28	sseq1d 3967	. . . . . 6 ⊢ (𝑧 = 𝑋 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆) ↔ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆)))
30	27, 29	anbi12d 643	. . . . 5 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)) ↔ (𝐴 ∈ 𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))))
31	30	rspcev 3580	. . . 4 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝐴 ∈ 𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
32	7, 10, 26, 31	syl12anc 849	. . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
33		elin 3920	. . . . . . 7 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin))
34		id 23	. . . . . . . 8 ⊢ (𝑥 ∈ Fin → 𝑥 ∈ Fin)
35		elpwi 4568	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝑂 → 𝑥 ⊆ 𝑂)
36	35	sseld 3935	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝒫 𝑂 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑂))
37		difeq2 4074	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑧))
38	37	sseq2d 3968	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦) ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
39	38	anbi2d 641	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → ((𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) ↔ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
40	39	rexbidv 3188	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) ↔ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
41		hauscmplem.2	. . . . . . . . . . . 12 ⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}
42	40, 41	elrab2 3653	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑂 ↔ (𝑧 ∈ 𝐽 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
43	42	simprbi 502	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑂 → ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
44	36, 43	syl6 36	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝒫 𝑂 → (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))))
45	44	ralrimiv 3155	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝑂 → ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))
46		eleq2 2851	. . . . . . . . . 10 ⊢ (𝑤 = (𝑓‘𝑧) → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ (𝑓‘𝑧)))
47		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑓‘𝑧) → ((cls‘𝐽)‘𝑤) = ((cls‘𝐽)‘(𝑓‘𝑧)))
48	47	sseq1d 3967	. . . . . . . . . 10 ⊢ (𝑤 = (𝑓‘𝑧) → (((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧) ↔ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))
49	46, 48	anbi12d 643	. . . . . . . . 9 ⊢ (𝑤 = (𝑓‘𝑧) → ((𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)) ↔ (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
50	49	ac6sfi 9242	. . . . . . . 8 ⊢ ((𝑥 ∈ Fin ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
51	34, 45, 50	syl2anr 608	. . . . . . 7 ⊢ ((𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
52	33, 51	sylbi 220	. . . . . 6 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
53	52	ad2antlr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))))
54	3	ad3antrrr 742	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐽 ∈ Top)
55		frn 6713	. . . . . . . 8 ⊢ (𝑓:𝑥⟶𝐽 → ran 𝑓 ⊆ 𝐽)
56	55	ad2antrl 740	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ⊆ 𝐽)
57		simprr 784	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → 𝑥 ≠ ∅)
58		simpl 487	. . . . . . . 8 ⊢ ((𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) → 𝑓:𝑥⟶𝐽)
59		fdm 6715	. . . . . . . . . . . 12 ⊢ (𝑓:𝑥⟶𝐽 → dom 𝑓 = 𝑥)
60	59	eqeq1d 2764	. . . . . . . . . . 11 ⊢ (𝑓:𝑥⟶𝐽 → (dom 𝑓 = ∅ ↔ 𝑥 = ∅))
61		dm0rn0 5913	. . . . . . . . . . 11 ⊢ (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
62	60, 61	bitr3di 289	. . . . . . . . . 10 ⊢ (𝑓:𝑥⟶𝐽 → (𝑥 = ∅ ↔ ran 𝑓 = ∅))
63	62	necon3bid 3001	. . . . . . . . 9 ⊢ (𝑓:𝑥⟶𝐽 → (𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅))
64	63	biimpac 483	. . . . . . . 8 ⊢ ((𝑥 ≠ ∅ ∧ 𝑓:𝑥⟶𝐽) → ran 𝑓 ≠ ∅)
65	57, 58, 64	syl2an 607	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ≠ ∅)
66	33	simprbi 502	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → 𝑥 ∈ Fin)
67	66	ad2antlr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ Fin)
68		ffn 6705	. . . . . . . . . 10 ⊢ (𝑓:𝑥⟶𝐽 → 𝑓 Fn 𝑥)
69		dffn4 6798	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ 𝑓:𝑥–onto→ran 𝑓)
70	68, 69	sylib 221	. . . . . . . . 9 ⊢ (𝑓:𝑥⟶𝐽 → 𝑓:𝑥–onto→ran 𝑓)
71	70	adantr 485	. . . . . . . 8 ⊢ ((𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) → 𝑓:𝑥–onto→ran 𝑓)
72		fofi 9271	. . . . . . . 8 ⊢ ((𝑥 ∈ Fin ∧ 𝑓:𝑥–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
73	67, 71, 72	syl2an 607	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ∈ Fin)
74		fiinopn 23069	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ∩ ran 𝑓 ∈ 𝐽))
75	74	imp 411	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ∩ ran 𝑓 ∈ 𝐽)
76	54, 56, 65, 73, 75	syl13anc 1398	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 ∈ 𝐽)
77		simpl 487	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → 𝐴 ∈ (𝑓‘𝑧))
78	77	ralimi 3101	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧))
79	78	ad2antll 741	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧))
80	8	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ (𝑋 ∖ 𝑆))
81		eliin 4960	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑋 ∖ 𝑆) → (𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧)))
82	80, 81	syl 18	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → (𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧)))
83	79, 82	mpbird 260	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
84	68	ad2antrl 740	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑓 Fn 𝑥)
85		fnrnfv 6940	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 → ran 𝑓 = {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)})
86	85	inteqd 4916	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑥 → ∩ ran 𝑓 = ∩ {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)})
87		fvex 6894	. . . . . . . . . 10 ⊢ (𝑓‘𝑧) ∈ V
88	87	dfiin2 4996	. . . . . . . . 9 ⊢ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) = ∩ {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)}
89	86, 88	eqtr4di 2815	. . . . . . . 8 ⊢ (𝑓 Fn 𝑥 → ∩ ran 𝑓 = ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
90	84, 89	syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 = ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧))
91	83, 90	eleqtrrd 2865	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ ∩ ran 𝑓)
92	57	adantr 485	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑥 ≠ ∅)
93	3	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → 𝐽 ∈ Top)
94		ffvelcdm 7076	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:𝑥⟶𝐽 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ 𝐽)
95	94	adantll 726	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ 𝐽)
96		elssuni 4903	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑧) ∈ 𝐽 → (𝑓‘𝑧) ⊆ ∪ 𝐽)
97	95, 96	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ ∪ 𝐽)
98	97, 5	sseqtrrdi 3977	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ 𝑋)
99	5	clscld 23215	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ (𝑓‘𝑧) ⊆ 𝑋) → ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
100	93, 98, 99	syl2anc 595	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
101	100	ralrimiva 3156	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
102	101	adantrr 729	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
103		iincld 23207	. . . . . . . . 9 ⊢ ((𝑥 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
104	92, 102, 103	syl2anc 595	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽))
105	5	sscls 23224	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (𝑓‘𝑧) ⊆ 𝑋) → (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
106	93, 98, 105	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
107	106	ralrimiva 3156	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)))
108		ssel 3930	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (𝑦 ∈ (𝑓‘𝑧) → 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
109	108	ral2imi 3103	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧) → ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
110		eliin 4960	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧)))
111	110	elv 3459	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧))
112		eliin 4960	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))))
113	112	elv 3459	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)))
114	109, 111, 113	3imtr4g 299	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) → 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))))
115	114	ssrdv 3942	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
116	107, 115	syl 18	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
117	116	adantrr 729	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
118	90, 117	eqsstrd 3970	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran 𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
119	5	clsss2 23240	. . . . . . . 8 ⊢ ((∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽) ∧ ∩ ran 𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
120	104, 118, 119	syl2anc 595	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))
121		ssel 3930	. . . . . . . . . . . . 13 ⊢ (((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ (𝑋 ∖ 𝑧)))
122	121	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ (𝑋 ∖ 𝑧)))
123	122	ral2imi 3103	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧)))
124		eliin 4960	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧)))
125	124	elv 3459	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧))
126	123, 113, 125	3imtr4g 299	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧)))
127	126	ssrdv 3942	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧))
128	127	ad2antll 741	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧))
129		iindif2 5042	. . . . . . . . . 10 ⊢ (𝑥 ≠ ∅ → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) = (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧))
130	92, 129	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) = (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧))
131		simplrl 788	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑆 ⊆ ∪ 𝑥)
132		uniiun 5022	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 = ∪ 𝑧 ∈ 𝑥 𝑧
133	132	sseq2i 3965	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ ∪ 𝑥 ↔ 𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧)
134		sscon 4096	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧 → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
135	133, 134	sylbi 220	. . . . . . . . . 10 ⊢ (𝑆 ⊆ ∪ 𝑥 → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
136	131, 135	syl 18	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆))
137	130, 136	eqsstrd 3970	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑆))
138	128, 137	sstrd 3946	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑆))
139	120, 138	sstrd 3946	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))
140		eleq2 2851	. . . . . . . 8 ⊢ (𝑧 = ∩ ran 𝑓 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ ∩ ran 𝑓))
141		fveq2 6881	. . . . . . . . 9 ⊢ (𝑧 = ∩ ran 𝑓 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘∩ ran 𝑓))
142	141	sseq1d 3967	. . . . . . . 8 ⊢ (𝑧 = ∩ ran 𝑓 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆) ↔ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆)))
143	140, 142	anbi12d 643	. . . . . . 7 ⊢ (𝑧 = ∩ ran 𝑓 → ((𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)) ↔ (𝐴 ∈ ∩ ran 𝑓 ∧ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))))
144	143	rspcev 3580	. . . . . 6 ⊢ ((∩ ran 𝑓 ∈ 𝐽 ∧ (𝐴 ∈ ∩ ran 𝑓 ∧ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
145	76, 91, 139, 144	syl12anc 849	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
146	53, 145	exlimddv 1964	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
147	146	anassrs 472	. . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
148	32, 147	pm2.61dane 3044	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
149	1	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ Haus)
150		hauscmplem.4	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ⊆ 𝑋)
151	150	sselda 3936	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑋)
152	9	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑋)
153		id 23	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ 𝑆)
154	8	eldifbd 3917	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝑆)
155		nelne2 3055	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑆 ∧ ¬ 𝐴 ∈ 𝑆) → 𝑥 ≠ 𝐴)
156	153, 154, 155	syl2anr 608	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≠ 𝐴)
157	5	hausnei 23496	. . . . . . . 8 ⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ≠ 𝐴)) → ∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅))
158	149, 151, 152, 156, 157	syl13anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅))
159		3anass 1110	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) ↔ (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)))
160		elssuni 4903	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽)
161	160, 5	sseqtrrdi 3977	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑋)
162	161	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → 𝑤 ⊆ 𝑋)
163		incom 4161	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∩ 𝑤) = (𝑤 ∩ 𝑦)
164	163	eqeq1i 2767	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∩ 𝑤) = ∅ ↔ (𝑤 ∩ 𝑦) = ∅)
165		reldisj 4412	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ⊆ 𝑋 → ((𝑤 ∩ 𝑦) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
166	164, 165	bitrid 286	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ⊆ 𝑋 → ((𝑦 ∩ 𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
167	162, 166	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑦 ∩ 𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦)))
168	149, 2	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ Top)
169	5	opncld 23201	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
170	168, 169	sylan 591	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
171	170	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽))
172	5	clsss2 23240	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽) ∧ 𝑤 ⊆ (𝑋 ∖ 𝑦)) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))
173	172	ex 417	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽) → (𝑤 ⊆ (𝑋 ∖ 𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
174	171, 173	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑤 ⊆ (𝑋 ∖ 𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
175	167, 174	sylbid 243	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑦 ∩ 𝑤) = ∅ → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))
176	175	anim2d 623	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
177	176	anim2d 623	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)) → (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
178	159, 177	biimtrid 245	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
179	178	reximdva 3177	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
180		r19.42v 3196	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
181	179, 180	imbitrdi 254	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
182	181	reximdva 3177	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))))
183	158, 182	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
184	41	unieqi 4883	. . . . . . . 8 ⊢ ∪ 𝑂 = ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}
185	184	eleq2i 2854	. . . . . . 7 ⊢ (𝑥 ∈ ∪ 𝑂 ↔ 𝑥 ∈ ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))})
186		elunirab 4886	. . . . . . 7 ⊢ (𝑥 ∈ ∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))} ↔ ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
187	185, 186	bitri 278	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑂 ↔ ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))
188	183, 187	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ∪ 𝑂)
189	188	ex 417	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑂))
190	189	ssrdv 3942	. . 3 ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝑂)
191		unieq 4882	. . . . . 6 ⊢ (𝑧 = 𝑂 → ∪ 𝑧 = ∪ 𝑂)
192	191	sseq2d 3968	. . . . 5 ⊢ (𝑧 = 𝑂 → (𝑆 ⊆ ∪ 𝑧 ↔ 𝑆 ⊆ ∪ 𝑂))
193		pweq 4575	. . . . . . 7 ⊢ (𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂)
194	193	ineq1d 4171	. . . . . 6 ⊢ (𝑧 = 𝑂 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑂 ∩ Fin))
195	194	rexeqdv 3323	. . . . 5 ⊢ (𝑧 = 𝑂 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
196	192, 195	imbi12d 347	. . . 4 ⊢ (𝑧 = 𝑂 → ((𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥) ↔ (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥)))
197		hauscmplem.5	. . . . 5 ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp)
198	5	cmpsub 23568	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥)))
199	198	biimp3a 1497	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ (𝐽 ↾t 𝑆) ∈ Comp) → ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
200	3, 150, 197, 199	syl3anc 1397	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
201	41	ssrab3 4035	. . . . 5 ⊢ 𝑂 ⊆ 𝐽
202		elpw2g 5303	. . . . . 6 ⊢ (𝐽 ∈ Haus → (𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽))
203	1, 202	syl 18	. . . . 5 ⊢ (𝜑 → (𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽))
204	201, 203	mpbiri 261	. . . 4 ⊢ (𝜑 → 𝑂 ∈ 𝒫 𝐽)
205	196, 200, 204	rspcdva 3581	. . 3 ⊢ (𝜑 → (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥))
206	190, 205	mpd 16	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥)
207	148, 206	r19.29a 3172	1 ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102   = wceq 1569  ∃wex 1808   ∈ wcel 2142  {cab 2740   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  {crab 3415  Vcvv 3454   ∖ cdif 3901   ∩ cin 3903   ⊆ wss 3904  ∅c0 4285  𝒫 cpw 4561  ∪ cuni 4871  ∩ cint 4911  ∪ ciun 4955  ∩ ciin 4956  dom cdm 5660  ran crn 5661   Fn wfn 6531  ⟶wf 6532  –onto→wfo 6534  ‘cfv 6536  (class class class)co 7412  Fincfn 8941   ↾_t crest 17479  Topctop 23061  Clsdccld 23184  clsccl 23186  Hauscha 23476  Compccmp 23554

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-iin 4958  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-1st 7984  df-2nd 7985  df-1o 8451  df-2o 8452  df-en 8942  df-dom 8943  df-fin 8945  df-fi 9369  df-rest 17481  df-topgen 17502  df-top 23062  df-topon 23079  df-bases 23114  df-cld 23187  df-cls 23189  df-haus 23483  df-cmp 23555

This theorem is used by:  hauscmp  23575  hausllycmp  23662