Theorem findcard2s 8832

Description: Variation of findcard2 8831 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.)

Hypotheses

Ref	Expression
findcard2s.1	⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
findcard2s.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
findcard2s.3	⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))
findcard2s.4	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
findcard2s.5	⊢ 𝜓
findcard2s.6	⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝜒 → 𝜃))

Assertion

Ref	Expression
findcard2s	⊢ (𝐴 ∈ Fin → 𝜏)

Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝜒,𝑥   𝜑,𝑦,𝑧   𝜓,𝑥   𝜏,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦,𝑧)   𝜒(𝑦,𝑧)   𝜃(𝑦,𝑧)   𝜏(𝑦,𝑧)

Proof of Theorem findcard2s

Step	Hyp	Ref	Expression
1		findcard2s.1	. 2 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
2		findcard2s.2	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
3		findcard2s.3	. 2 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))
4		findcard2s.4	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
5		findcard2s.5	. 2 ⊢ 𝜓
6		findcard2s.6	. . . 4 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝜒 → 𝜃))
7	6	ex 416	. . 3 ⊢ (𝑦 ∈ Fin → (¬ 𝑧 ∈ 𝑦 → (𝜒 → 𝜃)))
8		snssi 4711	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑦 → {𝑧} ⊆ 𝑦)
9		ssequn1 4084	. . . . . . . 8 ⊢ ({𝑧} ⊆ 𝑦 ↔ ({𝑧} ∪ 𝑦) = 𝑦)
10	8, 9	sylib 221	. . . . . . 7 ⊢ (𝑧 ∈ 𝑦 → ({𝑧} ∪ 𝑦) = 𝑦)
11		uncom 4057	. . . . . . 7 ⊢ ({𝑧} ∪ 𝑦) = (𝑦 ∪ {𝑧})
12	10, 11	eqtr3di 2789	. . . . . 6 ⊢ (𝑧 ∈ 𝑦 → 𝑦 = (𝑦 ∪ {𝑧}))
13		vex 3405	. . . . . . 7 ⊢ 𝑦 ∈ V
14	13	eqvinc 3549	. . . . . 6 ⊢ (𝑦 = (𝑦 ∪ {𝑧}) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝑥 = (𝑦 ∪ {𝑧})))
15	12, 14	sylib 221	. . . . 5 ⊢ (𝑧 ∈ 𝑦 → ∃𝑥(𝑥 = 𝑦 ∧ 𝑥 = (𝑦 ∪ {𝑧})))
16	2	bicomd 226	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑))
17	16, 3	sylan9bb 513	. . . . . 6 ⊢ ((𝑥 = 𝑦 ∧ 𝑥 = (𝑦 ∪ {𝑧})) → (𝜒 ↔ 𝜃))
18	17	exlimiv 1938	. . . . 5 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝑥 = (𝑦 ∪ {𝑧})) → (𝜒 ↔ 𝜃))
19	15, 18	syl 17	. . . 4 ⊢ (𝑧 ∈ 𝑦 → (𝜒 ↔ 𝜃))
20	19	biimpd 232	. . 3 ⊢ (𝑧 ∈ 𝑦 → (𝜒 → 𝜃))
21	7, 20	pm2.61d2 184	. 2 ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃))
22	1, 2, 3, 4, 5, 21	findcard2 8831	1 ⊢ (𝐴 ∈ Fin → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2110   ∪ cun 3855   ⊆ wss 3857  ∅c0 4227  {csn 4531  Fincfn 8615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-sep 5181  ax-nul 5188  ax-pr 5311  ax-un 7512

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3403  df-sbc 3688  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-pss 3876  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-tp 4536  df-op 4538  df-uni 4810  df-br 5044  df-opab 5106  df-tr 5151  df-id 5444  df-eprel 5449  df-po 5457  df-so 5458  df-fr 5498  df-we 5500  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-ord 6205  df-on 6206  df-lim 6207  df-suc 6208  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-om 7634  df-en 8616  df-fin 8619

This theorem is referenced by:  findcard2d  8833  unfi  8839  ac6sfi  8904  domunfican  8933  fodomfi  8938  hashxplem  13983  hashmap  13985  hashbc  14000  hashf1lem2  14005  hashf1  14006  fsum2d  15316  fsumabs  15346  fsumrlim  15356  fsumo1  15357  fsumiun  15366  incexclem  15381  fprod2d  15524  coprmprod  16199  coprmproddvds  16201  gsum2dlem2  19328  ablfac1eulem  19431  mplcoe1  20966  mplcoe5  20969  coe1fzgsumd  21195  evl1gsumd  21245  mdetunilem9  21489  ptcmpfi  22682  tmdgsum  22964  fsumcn  23739  ovolfiniun  24370  volfiniun  24416  itgfsum  24696  dvmptfsum  24844  jensen  25843  gsumle  31041  gsumvsca1  31170  gsumvsca2  31171  finixpnum  35456  matunitlindflem1  35467  pwslnm  40574  fnchoice  42197  dvmptfprod  43115