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

Theorem ssfi 9173
Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5364, see ssfiALT 9174. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5364. (Revised by BTernaryTau, 12-Aug-2024.)
Assertion
Ref Expression
ssfi ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)

Proof of Theorem ssfi
Dummy variables 𝑏 𝑥 𝑦 𝑧 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssexg 5324 . . 3 ((𝐵𝐴𝐴 ∈ Fin) → 𝐵 ∈ V)
21ancoms 460 . 2 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ V)
3 sseq1 4008 . . . . . 6 (𝑏 = 𝐵 → (𝑏𝐴𝐵𝐴))
4 eleq1 2822 . . . . . 6 (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin))
53, 4imbi12d 345 . . . . 5 (𝑏 = 𝐵 → ((𝑏𝐴𝑏 ∈ Fin) ↔ (𝐵𝐴𝐵 ∈ Fin)))
65imbi2d 341 . . . 4 (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏𝐴𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵𝐴𝐵 ∈ Fin))))
7 sseq2 4009 . . . . . . . 8 (𝑥 = ∅ → (𝑏𝑥𝑏 ⊆ ∅))
87imbi1d 342 . . . . . . 7 (𝑥 = ∅ → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
98albidv 1924 . . . . . 6 (𝑥 = ∅ → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
10 sseq2 4009 . . . . . . . 8 (𝑥 = 𝑦 → (𝑏𝑥𝑏𝑦))
1110imbi1d 342 . . . . . . 7 (𝑥 = 𝑦 → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏𝑦𝑏 ∈ Fin)))
1211albidv 1924 . . . . . 6 (𝑥 = 𝑦 → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏𝑦𝑏 ∈ Fin)))
13 sseq2 4009 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏𝑥𝑏 ⊆ (𝑦 ∪ {𝑧})))
1413imbi1d 342 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
1514albidv 1924 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
16 sseq2 4009 . . . . . . . 8 (𝑥 = 𝐴 → (𝑏𝑥𝑏𝐴))
1716imbi1d 342 . . . . . . 7 (𝑥 = 𝐴 → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏𝐴𝑏 ∈ Fin)))
1817albidv 1924 . . . . . 6 (𝑥 = 𝐴 → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏𝐴𝑏 ∈ Fin)))
19 ss0 4399 . . . . . . . 8 (𝑏 ⊆ ∅ → 𝑏 = ∅)
20 0fin 9171 . . . . . . . 8 ∅ ∈ Fin
2119, 20eqeltrdi 2842 . . . . . . 7 (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
2221ax-gen 1798 . . . . . 6 𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
23 sseq1 4008 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏𝑦𝑐𝑦))
24 eleq1w 2817 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin))
2523, 24imbi12d 345 . . . . . . . . . 10 (𝑏 = 𝑐 → ((𝑏𝑦𝑏 ∈ Fin) ↔ (𝑐𝑦𝑐 ∈ Fin)))
2625cbvalvw 2040 . . . . . . . . 9 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) ↔ ∀𝑐(𝑐𝑦𝑐 ∈ Fin))
27 simp1 1137 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐𝑦𝑐 ∈ Fin))
28 snssi 4812 . . . . . . . . . . . . . . . . 17 (𝑧𝑏 → {𝑧} ⊆ 𝑏)
29 undif 4482 . . . . . . . . . . . . . . . . 17 ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
3028, 29sylib 217 . . . . . . . . . . . . . . . 16 (𝑧𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
31 uncom 4154 . . . . . . . . . . . . . . . 16 ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧})
3230, 31eqtr3di 2788 . . . . . . . . . . . . . . 15 (𝑧𝑏𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))
33 uncom 4154 . . . . . . . . . . . . . . . . 17 (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
3433sseq2i 4012 . . . . . . . . . . . . . . . 16 (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦))
35 ssundif 4488 . . . . . . . . . . . . . . . 16 (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)
3634, 35sylbb 218 . . . . . . . . . . . . . . 15 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦)
3732, 36anim12ci 615 . . . . . . . . . . . . . 14 ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
38373adant1 1131 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
39 3anass 1096 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))))
4027, 38, 39sylanbrc 584 . . . . . . . . . . . 12 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
41 vex 3479 . . . . . . . . . . . . . . . . 17 𝑏 ∈ V
4241difexi 5329 . . . . . . . . . . . . . . . 16 (𝑏 ∖ {𝑧}) ∈ V
43 sseq1 4008 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦))
44 eleq1 2822 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin))
4543, 44imbi12d 345 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐𝑦𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)))
4642, 45spcv 3596 . . . . . . . . . . . . . . 15 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))
4746imp 408 . . . . . . . . . . . . . 14 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin)
48 snfi 9044 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
49 unfi 9172 . . . . . . . . . . . . . 14 (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
5047, 48, 49sylancl 587 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
51 eleq1 2822 . . . . . . . . . . . . . 14 (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin))
5251biimparc 481 . . . . . . . . . . . . 13 ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
5350, 52stoic3 1779 . . . . . . . . . . . 12 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
5440, 53syl 17 . . . . . . . . . . 11 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)
55543expib 1123 . . . . . . . . . 10 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
5655alrimiv 1931 . . . . . . . . 9 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
5726, 56sylbi 216 . . . . . . . 8 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
58 disjsn 4716 . . . . . . . . . . . . 13 ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑏)
59 disjssun 4468 . . . . . . . . . . . . 13 ((𝑏 ∩ {𝑧}) = ∅ → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏𝑦))
6058, 59sylbir 234 . . . . . . . . . . . 12 𝑧𝑏 → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏𝑦))
6160biimpa 478 . . . . . . . . . . 11 ((¬ 𝑧𝑏𝑏 ⊆ ({𝑧} ∪ 𝑦)) → 𝑏𝑦)
6234, 61sylan2b 595 . . . . . . . . . 10 ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏𝑦)
6362imim1i 63 . . . . . . . . 9 ((𝑏𝑦𝑏 ∈ Fin) → ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
6463alimi 1814 . . . . . . . 8 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
65 exmid 894 . . . . . . . . . . . 12 (𝑧𝑏 ∨ ¬ 𝑧𝑏)
6665jctl 525 . . . . . . . . . . 11 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧𝑏 ∨ ¬ 𝑧𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
67 andir 1008 . . . . . . . . . . 11 (((𝑧𝑏 ∨ ¬ 𝑧𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))))
6866, 67sylib 217 . . . . . . . . . 10 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))))
69 pm3.44 959 . . . . . . . . . 10 ((((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin))
7068, 69syl5 34 . . . . . . . . 9 ((((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7170alanimi 1819 . . . . . . . 8 ((∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ∀𝑏((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7257, 64, 71syl2anc 585 . . . . . . 7 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7372a1i 11 . . . . . 6 (𝑦 ∈ Fin → (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
749, 12, 15, 18, 22, 73findcard2 9164 . . . . 5 (𝐴 ∈ Fin → ∀𝑏(𝑏𝐴𝑏 ∈ Fin))
757419.21bi 2183 . . . 4 (𝐴 ∈ Fin → (𝑏𝐴𝑏 ∈ Fin))
766, 75vtoclg 3557 . . 3 (𝐵 ∈ V → (𝐴 ∈ Fin → (𝐵𝐴𝐵 ∈ Fin)))
7776impd 412 . 2 (𝐵 ∈ V → ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin))
782, 77mpcom 38 1 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3a 1088  wal 1540   = wceq 1542  wcel 2107  Vcvv 3475  cdif 3946  cun 3947  cin 3948  wss 3949  c0 4323  {csn 4629  Fincfn 8939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-om 7856  df-1o 8466  df-en 8940  df-fin 8943
This theorem is referenced by:  pwfilem  9177  diffi  9179  fnfi  9181  f1domfi  9184  domfi  9192  ssfid  9267  infi  9268  finresfin  9270  findcard3  9285  findcard3OLD  9286  unfir  9314  xpfi  9317  fofinf1o  9327  cnvfiALT  9334  f1fi  9339  imafiALT  9345  mapfi  9348  ixpfi2  9350  mptfi  9351  cnvimamptfin  9353  suppssfifsupp  9378  snopfsupp  9386  fsuppres  9388  sniffsupp  9395  elfiun  9425  oemapvali  9679  ackbij2lem1  10214  ackbij1lem11  10225  fin23lem26  10320  fin23lem23  10321  fin23lem21  10334  fin11a  10378  isfin1-3  10381  axcclem  10452  ssnn0fi  13950  hashun3  14344  hashss  14369  hashssdif  14372  hashsslei  14386  hashreshashfun  14399  hashbclem  14411  hashf1lem2  14417  seqcoll2  14426  pr2pwpr  14440  fsumless  15742  cvgcmpce  15764  qshash  15773  incexclem  15782  incexc  15783  incexc2  15784  fprodmodd  15941  sumeven  16330  sumodd  16331  bitsfi  16378  bitsinv1  16383  bitsinvp1  16390  sadcaddlem  16398  sadadd2lem  16400  sadadd3  16402  sadaddlem  16407  sadasslem  16411  sadeq  16413  phicl2  16701  phibnd  16704  hashdvds  16708  phiprmpw  16709  phimullem  16712  eulerthlem2  16715  eulerth  16716  phisum  16723  sumhash  16829  prmreclem2  16850  prmreclem3  16851  prmreclem4  16852  prmreclem5  16853  1arith  16860  hashbccl  16936  prmgaplem3  16986  lagsubg  19072  symgfisg  19336  symggen2  19339  odcl2  19433  sylow1lem2  19467  sylow1lem3  19468  sylow1lem4  19469  sylow1lem5  19470  pgpssslw  19482  sylow2alem2  19486  sylow2a  19487  sylow2blem3  19490  sylow3lem3  19497  sylow3lem6  19500  gsumval3lem1  19773  gsumval3lem2  19774  gsumval3  19775  gsumpt  19830  ablfacrplem  19935  ablfacrp2  19937  ablfac1c  19941  ablfac1eulem  19942  ablfac1eu  19943  dsmmfi  21293  mplsubg  21561  mpllss  21562  psrbagsn  21624  psr1baslem  21709  submabas  22080  mdetdiaglem  22100  maducoeval2  22142  fctop  22507  restfpw  22683  fincmp  22897  cmpfi  22912  bwth  22914  finlocfin  23024  lfinpfin  23028  locfincmp  23030  1stckgenlem  23057  ptbasfi  23085  ptcnplem  23125  ptcmpfi  23317  cfinfil  23397  ufinffr  23433  fin1aufil  23436  tsmsres  23648  ovoliunlem1  25019  ovolicc2lem4  25037  ovolicc2lem5  25038  i1fima  25195  i1fd  25198  itg1cl  25202  itg1ge0  25203  i1f0  25204  i1f1  25207  i1fmul  25213  itg1addlem4  25216  itg1addlem4OLD  25217  itg1mulc  25222  itg10a  25228  itg1ge0a  25229  itg1climres  25232  plyexmo  25826  aannenlem2  25842  aalioulem2  25846  birthday  26459  wilthlem2  26573  ppifi  26610  prmdvdsfi  26611  ppiprm  26655  chtprm  26657  chtdif  26662  efchtdvds  26663  ppidif  26667  ppiltx  26681  mumul  26685  sqff1o  26686  musum  26695  ppiub  26707  vmasum  26719  logfac2  26720  dchrabs  26763  dchrptlem1  26767  dchrptlem2  26768  dchrpt  26770  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  chebbnd1lem1  26972  chtppilimlem1  26976  rpvmasum2  27015  dchrisum0re  27016  rplogsum  27030  dirith2  27031  cusgrfi  28715  hashwwlksnext  29168  relfi  31833  imafi2  31936  unifi3  31937  ffsrn  31954  xrge0tsmsd  32209  gsumle  32242  rmfsupp2  32387  hasheuni  33083  carsgclctunlem1  33316  sibfof  33339  sitgclg  33341  oddpwdc  33353  eulerpartlems  33359  eulerpartlemb  33367  eulerpartlemmf  33374  eulerpartlemgf  33378  eulerpartlemgs2  33379  coinfliplem  33477  coinflippv  33482  ballotlemfelz  33489  ballotlemfp1  33490  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemiex  33500  ballotlemsup  33503  ballotlemfg  33524  ballotlemfrc  33525  ballotlemfrceq  33527  ballotth  33536  breprexpnat  33646  hgt750lemb  33668  hgt750leme  33670  fisshasheq  34104  deranglem  34157  subfacp1lem3  34173  subfacp1lem5  34175  subfacp1lem6  34176  erdszelem2  34183  erdszelem8  34189  erdsze2lem2  34195  snmlff  34320  mvrsfpw  34497  finminlem  35203  topdifinffinlem  36228  matunitlindflem1  36484  poimirlem9  36497  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem30  36518  poimirlem32  36520  itg2addnclem2  36540  nnubfi  36618  nninfnub  36619  sstotbnd2  36642  cntotbnd  36664  sticksstones1  40962  rencldnfilem  41558  jm2.22  41734  jm2.23  41735  filnm  41832  pwssfi  43732  disjinfi  43891  fsumiunss  44291  fprodexp  44310  fprodabs2  44311  mccllem  44313  sumnnodd  44346  fprodcncf  44616  dvmptfprod  44661  dvnprodlem1  44662  dvnprodlem2  44663  fourierdlem25  44848  fourierdlem37  44860  fourierdlem51  44873  fourierdlem79  44901  fouriersw  44947  etransclem16  44966  etransclem24  44974  etransclem33  44983  etransclem44  44994  sge0resplit  45122  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  carageniuncllem2  45238  hsphoidmvle2  45301  hsphoidmvle  45302  hoidmvlelem4  45314  hoidmvlelem5  45315  upwrdfi  45601  fmtnoinf  46204  perfectALTVlem2  46390  rmsuppfi  47049  mndpsuppfi  47051  scmsuppfi  47053  suppmptcfin  47055
  Copyright terms: Public domain W3C validator