Theorem elutop 24220

Description: Open sets in the topology induced by an uniform structure 𝑈 on 𝑋 (Contributed by Thierry Arnoux, 30-Nov-2017.)

Assertion

Ref	Expression
elutop	⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴)))

Distinct variable groups:   𝑥,𝑣,𝐴   𝑣,𝑈,𝑥   𝑥,𝑋

Allowed substitution hint:   𝑋(𝑣)

Proof of Theorem elutop

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		utopval 24219	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎})
2	1	eleq2d 2827	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ 𝐴 ∈ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎}))
3		sseq2 3943	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((𝑣 “ {𝑥}) ⊆ 𝑎 ↔ (𝑣 “ {𝑥}) ⊆ 𝐴))
4	3	rexbidv 3165	. . . . 5 ⊢ (𝑎 = 𝐴 → (∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎 ↔ ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴))
5	4	raleqbi1dv 3309	. . . 4 ⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎 ↔ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴))
6	5	elrab 3631	. . 3 ⊢ (𝐴 ∈ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎} ↔ (𝐴 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴))
7	2, 6	bitrdi 289	. 2 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴)))
8		elex 3454	. . . . 5 ⊢ (𝐴 ∈ 𝒫 𝑋 → 𝐴 ∈ V)
9	8	a1i 11	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ 𝒫 𝑋 → 𝐴 ∈ V))
10		elfvex 6866	. . . . . . 7 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
11	10	adantr 482	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ V)
12		simpr 486	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
13	11, 12	ssexd 5255	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
14	13	ex 414	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ⊆ 𝑋 → 𝐴 ∈ V))
15		elpwg 4535	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋))
16	15	a1i 11	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋)))
17	9, 14, 16	pm5.21ndd 381	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋))
18	17	anbi1d 638	. 2 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((𝐴 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴)))
19	7, 18	bitrd 281	1 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ∀wral 3055  ∃wrex 3065  {crab 3393  Vcvv 3433   ⊆ wss 3885  𝒫 cpw 4532  {csn 4558   “ cima 5624  ‘cfv 6489  UnifOncust 24187  unifTopcutop 24217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-iota 6445  df-fun 6491  df-fv 6497  df-ust 24188  df-utop 24218

This theorem is referenced by:  utoptop  24221  utopbas  24222  restutop  24224  restutopopn  24225  ucncn  24271