MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  findcard2d Structured version   Visualization version   GIF version

Theorem findcard2d 9117
Description: Deduction version of findcard2 9115. (Contributed by SO, 16-Jul-2018.)
Hypotheses
Ref Expression
findcard2d.ch (𝑥 = ∅ → (𝜓𝜒))
findcard2d.th (𝑥 = 𝑦 → (𝜓𝜃))
findcard2d.ta (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓𝜏))
findcard2d.et (𝑥 = 𝐴 → (𝜓𝜂))
findcard2d.z (𝜑𝜒)
findcard2d.i ((𝜑 ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (𝜃𝜏))
findcard2d.a (𝜑𝐴 ∈ Fin)
Assertion
Ref Expression
findcard2d (𝜑𝜂)
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝜓,𝑦,𝑧   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜂,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑦,𝑧)   𝜃(𝑦,𝑧)   𝜏(𝑦,𝑧)   𝜂(𝑦,𝑧)

Proof of Theorem findcard2d
StepHypRef Expression
1 ssid 3969 . 2 𝐴𝐴
2 findcard2d.a . . . 4 (𝜑𝐴 ∈ Fin)
32adantr 481 . . 3 ((𝜑𝐴𝐴) → 𝐴 ∈ Fin)
4 sseq1 3972 . . . . . 6 (𝑥 = ∅ → (𝑥𝐴 ↔ ∅ ⊆ 𝐴))
54anbi2d 629 . . . . 5 (𝑥 = ∅ → ((𝜑𝑥𝐴) ↔ (𝜑 ∧ ∅ ⊆ 𝐴)))
6 findcard2d.ch . . . . 5 (𝑥 = ∅ → (𝜓𝜒))
75, 6imbi12d 344 . . . 4 (𝑥 = ∅ → (((𝜑𝑥𝐴) → 𝜓) ↔ ((𝜑 ∧ ∅ ⊆ 𝐴) → 𝜒)))
8 sseq1 3972 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
98anbi2d 629 . . . . 5 (𝑥 = 𝑦 → ((𝜑𝑥𝐴) ↔ (𝜑𝑦𝐴)))
10 findcard2d.th . . . . 5 (𝑥 = 𝑦 → (𝜓𝜃))
119, 10imbi12d 344 . . . 4 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → 𝜓) ↔ ((𝜑𝑦𝐴) → 𝜃)))
12 sseq1 3972 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
1312anbi2d 629 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝜑𝑥𝐴) ↔ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)))
14 findcard2d.ta . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓𝜏))
1513, 14imbi12d 344 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → (((𝜑𝑥𝐴) → 𝜓) ↔ ((𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → 𝜏)))
16 sseq1 3972 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝐴𝐴𝐴))
1716anbi2d 629 . . . . 5 (𝑥 = 𝐴 → ((𝜑𝑥𝐴) ↔ (𝜑𝐴𝐴)))
18 findcard2d.et . . . . 5 (𝑥 = 𝐴 → (𝜓𝜂))
1917, 18imbi12d 344 . . . 4 (𝑥 = 𝐴 → (((𝜑𝑥𝐴) → 𝜓) ↔ ((𝜑𝐴𝐴) → 𝜂)))
20 findcard2d.z . . . . 5 (𝜑𝜒)
2120adantr 481 . . . 4 ((𝜑 ∧ ∅ ⊆ 𝐴) → 𝜒)
22 simprl 769 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝜑)
23 simprr 771 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
2423unssad 4152 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑦𝐴)
2522, 24jca 512 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝜑𝑦𝐴))
26 id 22 . . . . . . . . . . 11 ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
27 vsnid 4628 . . . . . . . . . . . 12 𝑧 ∈ {𝑧}
28 elun2 4142 . . . . . . . . . . . 12 (𝑧 ∈ {𝑧} → 𝑧 ∈ (𝑦 ∪ {𝑧}))
2927, 28mp1i 13 . . . . . . . . . . 11 ((𝑦 ∪ {𝑧}) ⊆ 𝐴𝑧 ∈ (𝑦 ∪ {𝑧}))
3026, 29sseldd 3948 . . . . . . . . . 10 ((𝑦 ∪ {𝑧}) ⊆ 𝐴𝑧𝐴)
3130ad2antll 727 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧𝐴)
32 simplr 767 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧𝑦)
3331, 32eldifd 3924 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ (𝐴𝑦))
34 findcard2d.i . . . . . . . 8 ((𝜑 ∧ (𝑦𝐴𝑧 ∈ (𝐴𝑦))) → (𝜃𝜏))
3522, 24, 33, 34syl12anc 835 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝜃𝜏))
3625, 35embantd 59 . . . . . 6 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (((𝜑𝑦𝐴) → 𝜃) → 𝜏))
3736ex 413 . . . . 5 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (((𝜑𝑦𝐴) → 𝜃) → 𝜏)))
3837com23 86 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (((𝜑𝑦𝐴) → 𝜃) → ((𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → 𝜏)))
397, 11, 15, 19, 21, 38findcard2s 9116 . . 3 (𝐴 ∈ Fin → ((𝜑𝐴𝐴) → 𝜂))
403, 39mpcom 38 . 2 ((𝜑𝐴𝐴) → 𝜂)
411, 40mpan2 689 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  cdif 3910  cun 3911  wss 3913  c0 4287  {csn 4591  Fincfn 8890
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-om 7808  df-en 8891  df-fin 8894
This theorem is referenced by:  fprodmodd  15891  sumeven  16280  sumodd  16281  maducoeval2  22026  madugsum  22029  esum2dlem  32780  fiunelcarsg  33005  carsgclctunlem1  33006  fiiuncl  43395  mpct  43543  fprodexp  43955  fprodabs2  43956  mccl  43959  fprodcn  43961  fprodcncf  44261  dvnprodlem3  44309  sge0iunmptlemfi  44774  hoidmvle  44961
  Copyright terms: Public domain W3C validator