Theorem istopon 22061

Description: Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.)

Assertion

Ref	Expression
istopon	⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))

Proof of Theorem istopon

Dummy variables 𝑏 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfvex 6807	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ V)
2		uniexg 7593	. . . 4 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
3		eleq1 2826	. . . 4 ⊢ (𝐵 = ∪ 𝐽 → (𝐵 ∈ V ↔ ∪ 𝐽 ∈ V))
4	2, 3	syl5ibrcom 246	. . 3 ⊢ (𝐽 ∈ Top → (𝐵 = ∪ 𝐽 → 𝐵 ∈ V))
5	4	imp 407	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽) → 𝐵 ∈ V)
6		eqeq1 2742	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 = ∪ 𝑗 ↔ 𝐵 = ∪ 𝑗))
7	6	rabbidv 3414	. . . . 5 ⊢ (𝑏 = 𝐵 → {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} = {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗})
8		df-topon 22060	. . . . 5 ⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗})
9		vpwex 5300	. . . . . . 7 ⊢ 𝒫 𝑏 ∈ V
10	9	pwex 5303	. . . . . 6 ⊢ 𝒫 𝒫 𝑏 ∈ V
11		rabss 4005	. . . . . . 7 ⊢ ({𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} ⊆ 𝒫 𝒫 𝑏 ↔ ∀𝑗 ∈ Top (𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏))
12		pwuni 4878	. . . . . . . . . 10 ⊢ 𝑗 ⊆ 𝒫 ∪ 𝑗
13		pweq 4549	. . . . . . . . . 10 ⊢ (𝑏 = ∪ 𝑗 → 𝒫 𝑏 = 𝒫 ∪ 𝑗)
14	12, 13	sseqtrrid 3974	. . . . . . . . 9 ⊢ (𝑏 = ∪ 𝑗 → 𝑗 ⊆ 𝒫 𝑏)
15		velpw 4538	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝒫 𝒫 𝑏 ↔ 𝑗 ⊆ 𝒫 𝑏)
16	14, 15	sylibr 233	. . . . . . . 8 ⊢ (𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏)
17	16	a1i 11	. . . . . . 7 ⊢ (𝑗 ∈ Top → (𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏))
18	11, 17	mprgbir 3079	. . . . . 6 ⊢ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} ⊆ 𝒫 𝒫 𝑏
19	10, 18	ssexi 5246	. . . . 5 ⊢ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} ∈ V
20	7, 8, 19	fvmpt3i 6880	. . . 4 ⊢ (𝐵 ∈ V → (TopOn‘𝐵) = {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗})
21	20	eleq2d 2824	. . 3 ⊢ (𝐵 ∈ V → (𝐽 ∈ (TopOn‘𝐵) ↔ 𝐽 ∈ {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗}))
22		unieq 4850	. . . . 5 ⊢ (𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽)
23	22	eqeq2d 2749	. . . 4 ⊢ (𝑗 = 𝐽 → (𝐵 = ∪ 𝑗 ↔ 𝐵 = ∪ 𝐽))
24	23	elrab 3624	. . 3 ⊢ (𝐽 ∈ {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗} ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
25	21, 24	bitrdi 287	. 2 ⊢ (𝐵 ∈ V → (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)))
26	1, 5, 25	pm5.21nii 380	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {crab 3068  Vcvv 3432   ⊆ wss 3887  𝒫 cpw 4533  ∪ cuni 4839  ‘cfv 6433  Topctop 22042  TopOnctopon 22059

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-topon 22060

This theorem is referenced by:  topontop  22062  toponuni  22063  toptopon  22066  toponcom  22077  istps2  22084  tgtopon  22121  distopon  22147  indistopon  22151  fctop  22154  cctop  22156  ppttop  22157  epttop  22159  mretopd  22243  toponmre  22244  resttopon  22312  resttopon2  22319  kgentopon  22689  txtopon  22742  pttopon  22747  xkotopon  22751  qtoptopon  22855  flimtopon  23121  fclstopon  23163  fclsfnflim  23178  utoptopon  23388  qtopt1  31785  neibastop1  34548  onsuctopon  34623  rfcnpre1  42562  cnfex  42571  icccncfext  43428  stoweidlem47  43588