Theorem ssfii 9323

Description: Any element of a set 𝐴 is the intersection of a finite subset of 𝐴. (Contributed by FL, 27-Apr-2008.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)

Assertion

Ref	Expression
ssfii	⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (fi‘𝐴))

Proof of Theorem ssfii

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3434	. . . . 5 ⊢ 𝑥 ∈ V
2	1	intsn 4927	. . . 4 ⊢ ∩ {𝑥} = 𝑥
3		simpl 482	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ 𝑉)
4		simpr 484	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
5	4	snssd 4753	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → {𝑥} ⊆ 𝐴)
6	1	snnz 4721	. . . . . 6 ⊢ {𝑥} ≠ ∅
7	6	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → {𝑥} ≠ ∅)
8		snfi 8981	. . . . . 6 ⊢ {𝑥} ∈ Fin
9	8	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → {𝑥} ∈ Fin)
10		elfir 9319	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ({𝑥} ⊆ 𝐴 ∧ {𝑥} ≠ ∅ ∧ {𝑥} ∈ Fin)) → ∩ {𝑥} ∈ (fi‘𝐴))
11	3, 5, 7, 9, 10	syl13anc 1375	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → ∩ {𝑥} ∈ (fi‘𝐴))
12	2, 11	eqeltrrid 2842	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (fi‘𝐴))
13	12	ex 412	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 → 𝑥 ∈ (fi‘𝐴)))
14	13	ssrdv 3928	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (fi‘𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933   ⊆ wss 3890  ∅c0 4274  {csn 4568  ∩ cint 4890  ‘cfv 6490  Fincfn 8884  ficfi 9314

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-om 7809  df-1o 8396  df-en 8885  df-fin 8888  df-fi 9315

This theorem is referenced by:  fieq0  9325  dffi2  9327  inficl  9329  fiuni  9332  dffi3  9335  inffien  9974  fictb  10155  ordtbas2  23134  ordtbas  23135  ordtopn1  23137  ordtopn2  23138  leordtval2  23155  subbascn  23197  2ndcsb  23392  ptbasfi  23524  xkoopn  23532  fsubbas  23810  fbunfip  23812  isufil2  23851  ufileu  23862  filufint  23863  fmfnfmlem4  23900  fmfnfm  23901  hausflim  23924  flimclslem  23927  fclsfnflim  23970  flimfnfcls  23971  fclscmp  23973  alexsubb  23989  alexsubALTlem4  23993  ordtconnlem1  34074  topjoin  36553