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

Theorem ssfi 9189
Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5359, see ssfiALT 9190. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5359. (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 5317 . . 3 ((𝐵𝐴𝐴 ∈ Fin) → 𝐵 ∈ V)
21ancoms 458 . 2 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ V)
3 sseq1 4003 . . . . . 6 (𝑏 = 𝐵 → (𝑏𝐴𝐵𝐴))
4 eleq1 2816 . . . . . 6 (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin))
53, 4imbi12d 344 . . . . 5 (𝑏 = 𝐵 → ((𝑏𝐴𝑏 ∈ Fin) ↔ (𝐵𝐴𝐵 ∈ Fin)))
65imbi2d 340 . . . 4 (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏𝐴𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵𝐴𝐵 ∈ Fin))))
7 sseq2 4004 . . . . . . . 8 (𝑥 = ∅ → (𝑏𝑥𝑏 ⊆ ∅))
87imbi1d 341 . . . . . . 7 (𝑥 = ∅ → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
98albidv 1916 . . . . . 6 (𝑥 = ∅ → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
10 sseq2 4004 . . . . . . . 8 (𝑥 = 𝑦 → (𝑏𝑥𝑏𝑦))
1110imbi1d 341 . . . . . . 7 (𝑥 = 𝑦 → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏𝑦𝑏 ∈ Fin)))
1211albidv 1916 . . . . . 6 (𝑥 = 𝑦 → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏𝑦𝑏 ∈ Fin)))
13 sseq2 4004 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏𝑥𝑏 ⊆ (𝑦 ∪ {𝑧})))
1413imbi1d 341 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
1514albidv 1916 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
16 sseq2 4004 . . . . . . . 8 (𝑥 = 𝐴 → (𝑏𝑥𝑏𝐴))
1716imbi1d 341 . . . . . . 7 (𝑥 = 𝐴 → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏𝐴𝑏 ∈ Fin)))
1817albidv 1916 . . . . . 6 (𝑥 = 𝐴 → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏𝐴𝑏 ∈ Fin)))
19 ss0 4394 . . . . . . . 8 (𝑏 ⊆ ∅ → 𝑏 = ∅)
20 0fin 9187 . . . . . . . 8 ∅ ∈ Fin
2119, 20eqeltrdi 2836 . . . . . . 7 (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
2221ax-gen 1790 . . . . . 6 𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
23 sseq1 4003 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏𝑦𝑐𝑦))
24 eleq1w 2811 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin))
2523, 24imbi12d 344 . . . . . . . . . 10 (𝑏 = 𝑐 → ((𝑏𝑦𝑏 ∈ Fin) ↔ (𝑐𝑦𝑐 ∈ Fin)))
2625cbvalvw 2032 . . . . . . . . 9 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) ↔ ∀𝑐(𝑐𝑦𝑐 ∈ Fin))
27 simp1 1134 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐𝑦𝑐 ∈ Fin))
28 snssi 4807 . . . . . . . . . . . . . . . . 17 (𝑧𝑏 → {𝑧} ⊆ 𝑏)
29 undif 4477 . . . . . . . . . . . . . . . . 17 ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
3028, 29sylib 217 . . . . . . . . . . . . . . . 16 (𝑧𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
31 uncom 4149 . . . . . . . . . . . . . . . 16 ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧})
3230, 31eqtr3di 2782 . . . . . . . . . . . . . . 15 (𝑧𝑏𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))
33 uncom 4149 . . . . . . . . . . . . . . . . 17 (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
3433sseq2i 4007 . . . . . . . . . . . . . . . 16 (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦))
35 ssundif 4483 . . . . . . . . . . . . . . . 16 (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)
3634, 35sylbb 218 . . . . . . . . . . . . . . 15 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦)
3732, 36anim12ci 613 . . . . . . . . . . . . . 14 ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
38373adant1 1128 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
39 3anass 1093 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))))
4027, 38, 39sylanbrc 582 . . . . . . . . . . . 12 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
41 vex 3473 . . . . . . . . . . . . . . . . 17 𝑏 ∈ V
4241difexi 5324 . . . . . . . . . . . . . . . 16 (𝑏 ∖ {𝑧}) ∈ V
43 sseq1 4003 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦))
44 eleq1 2816 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin))
4543, 44imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐𝑦𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)))
4642, 45spcv 3590 . . . . . . . . . . . . . . 15 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))
4746imp 406 . . . . . . . . . . . . . 14 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin)
48 snfi 9060 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
49 unfi 9188 . . . . . . . . . . . . . 14 (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
5047, 48, 49sylancl 585 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
51 eleq1 2816 . . . . . . . . . . . . . 14 (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin))
5251biimparc 479 . . . . . . . . . . . . 13 ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
5350, 52stoic3 1771 . . . . . . . . . . . 12 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
5440, 53syl 17 . . . . . . . . . . 11 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)
55543expib 1120 . . . . . . . . . 10 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
5655alrimiv 1923 . . . . . . . . 9 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
5726, 56sylbi 216 . . . . . . . 8 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
58 disjsn 4711 . . . . . . . . . . . . 13 ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑏)
59 disjssun 4463 . . . . . . . . . . . . 13 ((𝑏 ∩ {𝑧}) = ∅ → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏𝑦))
6058, 59sylbir 234 . . . . . . . . . . . 12 𝑧𝑏 → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏𝑦))
6160biimpa 476 . . . . . . . . . . 11 ((¬ 𝑧𝑏𝑏 ⊆ ({𝑧} ∪ 𝑦)) → 𝑏𝑦)
6234, 61sylan2b 593 . . . . . . . . . 10 ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏𝑦)
6362imim1i 63 . . . . . . . . 9 ((𝑏𝑦𝑏 ∈ Fin) → ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
6463alimi 1806 . . . . . . . 8 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
65 exmid 893 . . . . . . . . . . . 12 (𝑧𝑏 ∨ ¬ 𝑧𝑏)
6665jctl 523 . . . . . . . . . . 11 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧𝑏 ∨ ¬ 𝑧𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
67 andir 1007 . . . . . . . . . . 11 (((𝑧𝑏 ∨ ¬ 𝑧𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))))
6866, 67sylib 217 . . . . . . . . . 10 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))))
69 pm3.44 958 . . . . . . . . . 10 ((((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin))
7068, 69syl5 34 . . . . . . . . 9 ((((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7170alanimi 1811 . . . . . . . 8 ((∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ∀𝑏((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7257, 64, 71syl2anc 583 . . . . . . 7 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7372a1i 11 . . . . . 6 (𝑦 ∈ Fin → (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
749, 12, 15, 18, 22, 73findcard2 9180 . . . . 5 (𝐴 ∈ Fin → ∀𝑏(𝑏𝐴𝑏 ∈ Fin))
757419.21bi 2175 . . . 4 (𝐴 ∈ Fin → (𝑏𝐴𝑏 ∈ Fin))
766, 75vtoclg 3538 . . 3 (𝐵 ∈ V → (𝐴 ∈ Fin → (𝐵𝐴𝐵 ∈ Fin)))
7776impd 410 . 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 395  wo 846  w3a 1085  wal 1532   = wceq 1534  wcel 2099  Vcvv 3469  cdif 3941  cun 3942  cin 3943  wss 3944  c0 4318  {csn 4624  Fincfn 8955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-om 7865  df-1o 8480  df-en 8956  df-fin 8959
This theorem is referenced by:  pwfilem  9193  diffi  9195  fnfi  9197  f1domfi  9200  domfi  9208  ssfid  9283  infi  9284  finresfin  9286  findcard3  9301  findcard3OLD  9302  unfir  9330  xpfi  9333  fofinf1o  9343  cnvfiALT  9350  f1fi  9355  imafiALT  9361  mapfi  9364  ixpfi2  9366  mptfi  9367  cnvimamptfin  9369  suppssfifsupp  9395  snopfsupp  9406  fsuppres  9408  sniffsupp  9415  elfiun  9445  oemapvali  9699  ackbij2lem1  10234  ackbij1lem11  10245  fin23lem26  10340  fin23lem23  10341  fin23lem21  10354  fin11a  10398  isfin1-3  10401  axcclem  10472  ssnn0fi  13974  hashun3  14367  hashss  14392  hashssdif  14395  hashsslei  14409  hashreshashfun  14422  hashbclem  14435  hashf1lem2  14441  seqcoll2  14450  pr2pwpr  14464  fsumless  15766  cvgcmpce  15788  qshash  15797  incexclem  15806  incexc  15807  incexc2  15808  fprodmodd  15965  sumeven  16355  sumodd  16356  bitsfi  16403  bitsinv1  16408  bitsinvp1  16415  sadcaddlem  16423  sadadd2lem  16425  sadadd3  16427  sadaddlem  16432  sadasslem  16436  sadeq  16438  phicl2  16728  phibnd  16731  hashdvds  16735  phiprmpw  16736  phimullem  16739  eulerthlem2  16742  eulerth  16743  phisum  16750  sumhash  16856  prmreclem2  16877  prmreclem3  16878  prmreclem4  16879  prmreclem5  16880  1arith  16887  hashbccl  16963  prmgaplem3  17013  lagsubg  19141  symgfisg  19414  symggen2  19417  odcl2  19511  sylow1lem2  19545  sylow1lem3  19546  sylow1lem4  19547  sylow1lem5  19548  pgpssslw  19560  sylow2alem2  19564  sylow2a  19565  sylow2blem3  19568  sylow3lem3  19575  sylow3lem6  19578  gsumval3lem1  19851  gsumval3lem2  19852  gsumval3  19853  gsumpt  19908  ablfacrplem  20013  ablfacrp2  20015  ablfac1c  20019  ablfac1eulem  20020  ablfac1eu  20021  dsmmfi  21659  mplsubg  21931  mpllss  21932  psrbagsn  21994  psr1baslem  22091  submabas  22467  mdetdiaglem  22487  maducoeval2  22529  fctop  22894  restfpw  23070  fincmp  23284  cmpfi  23299  bwth  23301  finlocfin  23411  lfinpfin  23415  locfincmp  23417  1stckgenlem  23444  ptbasfi  23472  ptcnplem  23512  ptcmpfi  23704  cfinfil  23784  ufinffr  23820  fin1aufil  23823  tsmsres  24035  ovoliunlem1  25418  ovolicc2lem4  25436  ovolicc2lem5  25437  i1fima  25594  i1fd  25597  itg1cl  25601  itg1ge0  25602  i1f0  25603  i1f1  25606  i1fmul  25612  itg1addlem4  25615  itg1addlem4OLD  25616  itg1mulc  25621  itg10a  25627  itg1ge0a  25628  itg1climres  25631  plyexmo  26235  aannenlem2  26251  aalioulem2  26255  birthday  26873  wilthlem2  26988  ppifi  27025  prmdvdsfi  27026  ppiprm  27070  chtprm  27072  chtdif  27077  efchtdvds  27078  ppidif  27082  ppiltx  27096  mumul  27100  sqff1o  27101  musum  27110  ppiub  27124  vmasum  27136  logfac2  27137  dchrabs  27180  dchrptlem1  27184  dchrptlem2  27185  dchrpt  27187  lgsquadlem1  27300  lgsquadlem2  27301  lgsquadlem3  27302  chebbnd1lem1  27389  chtppilimlem1  27393  rpvmasum2  27432  dchrisum0re  27433  rplogsum  27447  dirith2  27448  cusgrfi  29259  hashwwlksnext  29712  relfi  32377  imafi2  32477  unifi3  32478  ffsrn  32495  xrge0tsmsd  32749  gsumle  32782  rmfsupp2  32923  hasheuni  33640  carsgclctunlem1  33873  sibfof  33896  sitgclg  33898  oddpwdc  33910  eulerpartlems  33916  eulerpartlemb  33924  eulerpartlemmf  33931  eulerpartlemgf  33935  eulerpartlemgs2  33936  coinfliplem  34034  coinflippv  34039  ballotlemfelz  34046  ballotlemfp1  34047  ballotlemfc0  34048  ballotlemfcc  34049  ballotlemiex  34057  ballotlemsup  34060  ballotlemfg  34081  ballotlemfrc  34082  ballotlemfrceq  34084  ballotth  34093  breprexpnat  34202  hgt750lemb  34224  hgt750leme  34226  fisshasheq  34660  deranglem  34712  subfacp1lem3  34728  subfacp1lem5  34730  subfacp1lem6  34731  erdszelem2  34738  erdszelem8  34744  erdsze2lem2  34750  snmlff  34875  mvrsfpw  35052  finminlem  35738  topdifinffinlem  36762  matunitlindflem1  37024  poimirlem9  37037  poimirlem26  37054  poimirlem27  37055  poimirlem28  37056  poimirlem30  37058  poimirlem32  37060  itg2addnclem2  37080  nnubfi  37158  nninfnub  37159  sstotbnd2  37182  cntotbnd  37204  sticksstones1  41550  rencldnfilem  42162  jm2.22  42338  jm2.23  42339  filnm  42436  pwssfi  44332  disjinfi  44488  fsumiunss  44886  fprodexp  44905  fprodabs2  44906  mccllem  44908  sumnnodd  44941  fprodcncf  45211  dvmptfprod  45256  dvnprodlem1  45257  dvnprodlem2  45258  fourierdlem25  45443  fourierdlem37  45455  fourierdlem51  45468  fourierdlem79  45496  fouriersw  45542  etransclem16  45561  etransclem24  45569  etransclem33  45578  etransclem44  45589  sge0resplit  45717  sge0iunmptlemfi  45724  sge0iunmptlemre  45726  carageniuncllem2  45833  hsphoidmvle2  45896  hsphoidmvle  45897  hoidmvlelem4  45909  hoidmvlelem5  45910  upwrdfi  46196  fmtnoinf  46799  perfectALTVlem2  46985  rmsuppfi  47360  mndpsuppfi  47362  scmsuppfi  47364  suppmptcfin  47366
  Copyright terms: Public domain W3C validator