Theorem opnregcld 37295

Description: A set is regularly closed iff it is the closure of some open set. (Contributed by Jeff Hankins, 27-Sep-2009.)

Hypothesis

Ref	Expression
opnregcld.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
opnregcld	⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜)))

Distinct variable groups:   𝐴,𝑜   𝑜,𝐽   𝑜,𝑋

Proof of Theorem opnregcld

Step	Hyp	Ref	Expression
1		opnregcld.1	. . . . 5 ⊢ 𝑋 = ∪ 𝐽
2	1	ntropn 23394	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐽)‘𝐴) ∈ 𝐽)
3		eqcom 2770	. . . . 5 ⊢ (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 ↔ 𝐴 = ((cls‘𝐽)‘((int‘𝐽)‘𝐴)))
4	3	biimpi 219	. . . 4 ⊢ (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 → 𝐴 = ((cls‘𝐽)‘((int‘𝐽)‘𝐴)))
5		fveq2 6905	. . . . 5 ⊢ (𝑜 = ((int‘𝐽)‘𝐴) → ((cls‘𝐽)‘𝑜) = ((cls‘𝐽)‘((int‘𝐽)‘𝐴)))
6	5	rspceeqv 3602	. . . 4 ⊢ ((((int‘𝐽)‘𝐴) ∈ 𝐽 ∧ 𝐴 = ((cls‘𝐽)‘((int‘𝐽)‘𝐴))) → ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜))
7	2, 4, 6	syl2an 608	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ ((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴) → ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜))
8	7	ex 418	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 → ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜)))
9		simpl 488	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝐽 ∈ Top)
10	1	eltopss 23252	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
11	1	clsss3 23404	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ⊆ 𝑋) → ((cls‘𝐽)‘𝑜) ⊆ 𝑋)
12	10, 11	syldan 603	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘𝑜) ⊆ 𝑋)
13	1	ntrss2 23402	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ((cls‘𝐽)‘𝑜) ⊆ 𝑋) → ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ ((cls‘𝐽)‘𝑜))
14	12, 13	syldan 603	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ ((cls‘𝐽)‘𝑜))
15	1	clsss 23399	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ ((cls‘𝐽)‘𝑜) ⊆ 𝑋 ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ ((cls‘𝐽)‘𝑜)) → ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) ⊆ ((cls‘𝐽)‘((cls‘𝐽)‘𝑜)))
16	9, 12, 14, 15	syl3anc 1399	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) ⊆ ((cls‘𝐽)‘((cls‘𝐽)‘𝑜)))
17	1	clsidm 23412	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ⊆ 𝑋) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑜)) = ((cls‘𝐽)‘𝑜))
18	10, 17	syldan 603	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑜)) = ((cls‘𝐽)‘𝑜))
19	16, 18	sseqtrd 3949	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) ⊆ ((cls‘𝐽)‘𝑜))
20	1	ntrss3 23405	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ ((cls‘𝐽)‘𝑜) ⊆ 𝑋) → ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ 𝑋)
21	12, 20	syldan 603	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ 𝑋)
22		simpr 490	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ∈ 𝐽)
23	1	sscls 23401	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ⊆ 𝑋) → 𝑜 ⊆ ((cls‘𝐽)‘𝑜))
24	10, 23	syldan 603	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ ((cls‘𝐽)‘𝑜))
25	1	ssntr 23403	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ ((cls‘𝐽)‘𝑜) ⊆ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ((cls‘𝐽)‘𝑜))) → 𝑜 ⊆ ((int‘𝐽)‘((cls‘𝐽)‘𝑜)))
26	9, 12, 22, 24, 25	syl22anc 852	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ ((int‘𝐽)‘((cls‘𝐽)‘𝑜)))
27	1	clsss 23399	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ 𝑋 ∧ 𝑜 ⊆ ((int‘𝐽)‘((cls‘𝐽)‘𝑜))) → ((cls‘𝐽)‘𝑜) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))))
28	9, 21, 26, 27	syl3anc 1399	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘𝑜) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))))
29	19, 28	eqssd 3930	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) = ((cls‘𝐽)‘𝑜))
30	29	adantlr 728	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) = ((cls‘𝐽)‘𝑜))
31		2fveq3 6910	. . . . 5 ⊢ (𝐴 = ((cls‘𝐽)‘𝑜) → ((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))))
32		id 23	. . . . 5 ⊢ (𝐴 = ((cls‘𝐽)‘𝑜) → 𝐴 = ((cls‘𝐽)‘𝑜))
33	31, 32	eqeq12d 2779	. . . 4 ⊢ (𝐴 = ((cls‘𝐽)‘𝑜) → (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 ↔ ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) = ((cls‘𝐽)‘𝑜)))
34	30, 33	syl5ibrcom 250	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑜 ∈ 𝐽) → (𝐴 = ((cls‘𝐽)‘𝑜) → ((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴))
35	34	rexlimdva 3167	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜) → ((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴))
36	8, 35	impbid 215	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∃wrex 3090   ⊆ wss 3900  ∪ cuni 4870  ‘cfv 6555  Topctop 23238  intcnt 23362  clsccl 23363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-top 23239  df-cld 23364  df-ntr 23365  df-cls 23366

This theorem is used by: (None)