Theorem iinopn 22929

Description: The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014.)

Assertion

Ref	Expression
iinopn	⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐽

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem iinopn

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr3 1196	. . 3 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)
2		dfiin2g 5055	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
3	1, 2	syl 17	. 2 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
4		simpl 482	. . 3 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → 𝐽 ∈ Top)
5		eqid 2740	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
6	5	rnmpt 5980	. . . 4 ⊢ ran (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
7	5	fmpt 7144	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐽)
8	1, 7	sylib 218	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐽)
9	8	frnd 6755	. . . 4 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐽)
10	6, 9	eqsstrrid 4058	. . 3 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐽)
11	8	fdmd 6757	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴)
12		simpr2 1195	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → 𝐴 ≠ ∅)
13	11, 12	eqnetrd 3014	. . . 4 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ≠ ∅)
14		dm0rn0 5949	. . . . . 6 ⊢ (dom (𝑥 ∈ 𝐴 ↦ 𝐵) = ∅ ↔ ran (𝑥 ∈ 𝐴 ↦ 𝐵) = ∅)
15	6	eqeq1i 2745	. . . . . 6 ⊢ (ran (𝑥 ∈ 𝐴 ↦ 𝐵) = ∅ ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = ∅)
16	14, 15	bitri 275	. . . . 5 ⊢ (dom (𝑥 ∈ 𝐴 ↦ 𝐵) = ∅ ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = ∅)
17	16	necon3bii 2999	. . . 4 ⊢ (dom (𝑥 ∈ 𝐴 ↦ 𝐵) ≠ ∅ ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≠ ∅)
18	13, 17	sylib 218	. . 3 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≠ ∅)
19		simpr1 1194	. . . 4 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → 𝐴 ∈ Fin)
20		abrexfi 9422	. . . 4 ⊢ (𝐴 ∈ Fin → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin)
21	19, 20	syl 17	. . 3 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin)
22		fiinopn 22928	. . . 4 ⊢ (𝐽 ∈ Top → (({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐽 ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≠ ∅ ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin) → ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ 𝐽))
23	22	imp 406	. . 3 ⊢ ((𝐽 ∈ Top ∧ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐽 ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≠ ∅ ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin)) → ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ 𝐽)
24	4, 10, 18, 21, 23	syl13anc 1372	. 2 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ 𝐽)
25	3, 24	eqeltrd 2844	1 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  {cab 2717   ≠ wne 2946  ∀wral 3067  ∃wrex 3076   ⊆ wss 3976  ∅c0 4352  ∩ cint 4970  ∩ ciin 5016   ↦ cmpt 5249  dom cdm 5700  ran crn 5701  ⟶wf 6569  Fincfn 9003  Topctop 22920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-om 7904  df-1st 8030  df-2nd 8031  df-1o 8522  df-2o 8523  df-en 9004  df-dom 9005  df-fin 9007  df-top 22921

This theorem is referenced by:  riinopn  22935  subbascn  23283