Theorem opnregcld 35153

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 22535	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐽)‘𝐴) ∈ 𝐽)
3		eqcom 2740	. . . . 5 ⊢ (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 ↔ 𝐴 = ((cls‘𝐽)‘((int‘𝐽)‘𝐴)))
4	3	biimpi 215	. . . 4 ⊢ (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 → 𝐴 = ((cls‘𝐽)‘((int‘𝐽)‘𝐴)))
5		fveq2 6888	. . . . 5 ⊢ (𝑜 = ((int‘𝐽)‘𝐴) → ((cls‘𝐽)‘𝑜) = ((cls‘𝐽)‘((int‘𝐽)‘𝐴)))
6	5	rspceeqv 3632	. . . 4 ⊢ ((((int‘𝐽)‘𝐴) ∈ 𝐽 ∧ 𝐴 = ((cls‘𝐽)‘((int‘𝐽)‘𝐴))) → ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜))
7	2, 4, 6	syl2an 597	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ ((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴) → ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜))
8	7	ex 414	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 → ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜)))
9		simpl 484	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝐽 ∈ Top)
10	1	eltopss 22391	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋)
11	1	clsss3 22545	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ⊆ 𝑋) → ((cls‘𝐽)‘𝑜) ⊆ 𝑋)
12	10, 11	syldan 592	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘𝑜) ⊆ 𝑋)
13	1	ntrss2 22543	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ((cls‘𝐽)‘𝑜) ⊆ 𝑋) → ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ ((cls‘𝐽)‘𝑜))
14	12, 13	syldan 592	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ ((cls‘𝐽)‘𝑜))
15	1	clsss 22540	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ ((cls‘𝐽)‘𝑜) ⊆ 𝑋 ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ ((cls‘𝐽)‘𝑜)) → ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) ⊆ ((cls‘𝐽)‘((cls‘𝐽)‘𝑜)))
16	9, 12, 14, 15	syl3anc 1372	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) ⊆ ((cls‘𝐽)‘((cls‘𝐽)‘𝑜)))
17	1	clsidm 22553	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ⊆ 𝑋) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑜)) = ((cls‘𝐽)‘𝑜))
18	10, 17	syldan 592	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑜)) = ((cls‘𝐽)‘𝑜))
19	16, 18	sseqtrd 4021	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) ⊆ ((cls‘𝐽)‘𝑜))
20	1	ntrss3 22546	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ ((cls‘𝐽)‘𝑜) ⊆ 𝑋) → ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ 𝑋)
21	12, 20	syldan 592	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ 𝑋)
22		simpr 486	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ∈ 𝐽)
23	1	sscls 22542	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ⊆ 𝑋) → 𝑜 ⊆ ((cls‘𝐽)‘𝑜))
24	10, 23	syldan 592	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ ((cls‘𝐽)‘𝑜))
25	1	ssntr 22544	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ ((cls‘𝐽)‘𝑜) ⊆ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ((cls‘𝐽)‘𝑜))) → 𝑜 ⊆ ((int‘𝐽)‘((cls‘𝐽)‘𝑜)))
26	9, 12, 22, 24, 25	syl22anc 838	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ ((int‘𝐽)‘((cls‘𝐽)‘𝑜)))
27	1	clsss 22540	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝑜)) ⊆ 𝑋 ∧ 𝑜 ⊆ ((int‘𝐽)‘((cls‘𝐽)‘𝑜))) → ((cls‘𝐽)‘𝑜) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))))
28	9, 21, 26, 27	syl3anc 1372	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘𝑜) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))))
29	19, 28	eqssd 3998	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) = ((cls‘𝐽)‘𝑜))
30	29	adantlr 714	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑜 ∈ 𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) = ((cls‘𝐽)‘𝑜))
31		2fveq3 6893	. . . . 5 ⊢ (𝐴 = ((cls‘𝐽)‘𝑜) → ((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))))
32		id 22	. . . . 5 ⊢ (𝐴 = ((cls‘𝐽)‘𝑜) → 𝐴 = ((cls‘𝐽)‘𝑜))
33	31, 32	eqeq12d 2749	. . . 4 ⊢ (𝐴 = ((cls‘𝐽)‘𝑜) → (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 ↔ ((cls‘𝐽)‘((int‘𝐽)‘((cls‘𝐽)‘𝑜))) = ((cls‘𝐽)‘𝑜)))
34	30, 33	syl5ibrcom 246	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑜 ∈ 𝐽) → (𝐴 = ((cls‘𝐽)‘𝑜) → ((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴))
35	34	rexlimdva 3156	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜) → ((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴))
36	8, 35	impbid 211	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃wrex 3071   ⊆ wss 3947  ∪ cuni 4907  ‘cfv 6540  Topctop 22377  intcnt 22503  clsccl 22504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-top 22378  df-cld 22505  df-ntr 22506  df-cls 22507

This theorem is referenced by: (None)