Theorem ptbasin2 22322

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015.)

Hypothesis

Ref	Expression
ptbas.1	⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}

Assertion

Ref	Expression
ptbasin2	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)

Distinct variable groups:   𝑥,𝑔,𝑦,𝑧,𝐴   𝑔,𝐹,𝑥,𝑦,𝑧   𝑔,𝑉,𝑥,𝑦,𝑧

Allowed substitution hints:   𝐵(𝑥,𝑦,𝑧,𝑔)

Proof of Theorem ptbasin2

Dummy variables 𝑘 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptbas.1	. . . 4 ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}
2	1	ptbasin 22321	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢 ∩ 𝑣) ∈ 𝐵)
3	2	ralrimivva 3103	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ∩ 𝑣) ∈ 𝐵)
4	1	ptuni2 22320	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ 𝐵)
5		ixpexg 8525	. . . . . 6 ⊢ (∀𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∈ V → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∈ V)
6		fvex 6681	. . . . . . . 8 ⊢ (𝐹‘𝑘) ∈ V
7	6	uniex 7479	. . . . . . 7 ⊢ ∪ (𝐹‘𝑘) ∈ V
8	7	a1i 11	. . . . . 6 ⊢ (𝑘 ∈ 𝐴 → ∪ (𝐹‘𝑘) ∈ V)
9	5, 8	mprg 3067	. . . . 5 ⊢ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∈ V
10	4, 9	eqeltrrdi 2842	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ 𝐵 ∈ V)
11		uniexb 7499	. . . 4 ⊢ (𝐵 ∈ V ↔ ∪ 𝐵 ∈ V)
12	10, 11	sylibr 237	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ V)
13		inficl 8955	. . 3 ⊢ (𝐵 ∈ V → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ∩ 𝑣) ∈ 𝐵 ↔ (fi‘𝐵) = 𝐵))
14	12, 13	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ∩ 𝑣) ∈ 𝐵 ↔ (fi‘𝐵) = 𝐵))
15	3, 14	mpbid 235	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1088   = wceq 1542  ∃wex 1786   ∈ wcel 2113  {cab 2716  ∀wral 3053  ∃wrex 3054  Vcvv 3397   ∖ cdif 3838   ∩ cin 3840  ∪ cuni 4793   Fn wfn 6328  ⟶wf 6329  ‘cfv 6333  Xcixp 8500  Fincfn 8548  ficfi 8940  Topctop 21637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-om 7594  df-1o 8124  df-er 8313  df-ixp 8501  df-en 8549  df-fin 8552  df-fi 8941  df-top 21638

This theorem is referenced by:  ptbas  22323  ptbasfi  22325