Theorem elutop 23490

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 23489	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎})
2	1	eleq2d 2823	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ 𝐴 ∈ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎}))
3		sseq2 3961	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((𝑣 “ {𝑥}) ⊆ 𝑎 ↔ (𝑣 “ {𝑥}) ⊆ 𝐴))
4	3	rexbidv 3172	. . . . 5 ⊢ (𝑎 = 𝐴 → (∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎 ↔ ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴))
5	4	raleqbi1dv 3304	. . . 4 ⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎 ↔ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴))
6	5	elrab 3637	. . 3 ⊢ (𝐴 ∈ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎} ↔ (𝐴 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴))
7	2, 6	bitrdi 287	. 2 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴)))
8		elex 3460	. . . . 5 ⊢ (𝐴 ∈ 𝒫 𝑋 → 𝐴 ∈ V)
9	8	a1i 11	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ 𝒫 𝑋 → 𝐴 ∈ V))
10		elfvex 6867	. . . . . . 7 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
11	10	adantr 482	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ V)
12		simpr 486	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
13	11, 12	ssexd 5272	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
14	13	ex 414	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ⊆ 𝑋 → 𝐴 ∈ V))
15		elpwg 4554	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋))
16	15	a1i 11	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋)))
17	9, 14, 16	pm5.21ndd 381	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋))
18	17	anbi1d 631	. 2 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((𝐴 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴)))
19	7, 18	bitrd 279	1 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1541   ∈ wcel 2106  ∀wral 3062  ∃wrex 3071  {crab 3404  Vcvv 3442   ⊆ wss 3901  𝒫 cpw 4551  {csn 4577   “ cima 5627  ‘cfv 6483  UnifOncust 23456  unifTopcutop 23487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-opab 5159  df-mpt 5180  df-id 5522  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-iota 6435  df-fun 6485  df-fv 6491  df-ust 23457  df-utop 23488

This theorem is referenced by:  utoptop  23491  utopbas  23492  restutop  23494  restutopopn  23495  ucncn  23542