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

Theorem findcard2d 9110
Description: Deduction version of findcard2 9108. (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 3966 . 2 𝐴𝐴
2 findcard2d.a . . . 4 (𝜑𝐴 ∈ Fin)
32adantr 481 . . 3 ((𝜑𝐴𝐴) → 𝐴 ∈ Fin)
4 sseq1 3969 . . . . . 6 (𝑥 = ∅ → (𝑥𝐴 ↔ ∅ ⊆ 𝐴))
54anbi2d 629 . . . . 5 (𝑥 = ∅ → ((𝜑𝑥𝐴) ↔ (𝜑 ∧ ∅ ⊆ 𝐴)))
6 findcard2d.ch . . . . 5 (𝑥 = ∅ → (𝜓𝜒))
75, 6imbi12d 344 . . . 4 (𝑥 = ∅ → (((𝜑𝑥𝐴) → 𝜓) ↔ ((𝜑 ∧ ∅ ⊆ 𝐴) → 𝜒)))
8 sseq1 3969 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
98anbi2d 629 . . . . 5 (𝑥 = 𝑦 → ((𝜑𝑥𝐴) ↔ (𝜑𝑦𝐴)))
10 findcard2d.th . . . . 5 (𝑥 = 𝑦 → (𝜓𝜃))
119, 10imbi12d 344 . . . 4 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → 𝜓) ↔ ((𝜑𝑦𝐴) → 𝜃)))
12 sseq1 3969 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
1312anbi2d 629 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝜑𝑥𝐴) ↔ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)))
14 findcard2d.ta . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓𝜏))
1513, 14imbi12d 344 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → (((𝜑𝑥𝐴) → 𝜓) ↔ ((𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → 𝜏)))
16 sseq1 3969 . . . . . 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 4147 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑦𝐴)
2522, 24jca 512 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝜑𝑦𝐴))
26 id 22 . . . . . . . . . . 11 ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
27 vsnid 4623 . . . . . . . . . . . 12 𝑧 ∈ {𝑧}
28 elun2 4137 . . . . . . . . . . . 12 (𝑧 ∈ {𝑧} → 𝑧 ∈ (𝑦 ∪ {𝑧}))
2927, 28mp1i 13 . . . . . . . . . . 11 ((𝑦 ∪ {𝑧}) ⊆ 𝐴𝑧 ∈ (𝑦 ∪ {𝑧}))
3026, 29sseldd 3945 . . . . . . . . . 10 ((𝑦 ∪ {𝑧}) ⊆ 𝐴𝑧𝐴)
3130ad2antll 727 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧𝐴)
32 simplr 767 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧𝑦)
3331, 32eldifd 3921 . . . . . . . 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 9109 . . 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 3907  cun 3908  wss 3910  c0 4282  {csn 4586  Fincfn 8883
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 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-om 7803  df-en 8884  df-fin 8887
This theorem is referenced by:  fprodmodd  15880  sumeven  16269  sumodd  16270  maducoeval2  21989  madugsum  21992  esum2dlem  32691  fiunelcarsg  32916  carsgclctunlem1  32917  fiiuncl  43263  mpct  43412  fprodexp  43825  fprodabs2  43826  mccl  43829  fprodcn  43831  fprodcncf  44131  dvnprodlem3  44179  sge0iunmptlemfi  44644  hoidmvle  44831
  Copyright terms: Public domain W3C validator