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

Theorem ssfi 9169
Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5353, see ssfiALT 9170. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5353. (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 5313 . . 3 ((𝐵𝐴𝐴 ∈ Fin) → 𝐵 ∈ V)
21ancoms 458 . 2 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ V)
3 sseq1 3999 . . . . . 6 (𝑏 = 𝐵 → (𝑏𝐴𝐵𝐴))
4 eleq1 2813 . . . . . 6 (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin))
53, 4imbi12d 344 . . . . 5 (𝑏 = 𝐵 → ((𝑏𝐴𝑏 ∈ Fin) ↔ (𝐵𝐴𝐵 ∈ Fin)))
65imbi2d 340 . . . 4 (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏𝐴𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵𝐴𝐵 ∈ Fin))))
7 sseq2 4000 . . . . . . . 8 (𝑥 = ∅ → (𝑏𝑥𝑏 ⊆ ∅))
87imbi1d 341 . . . . . . 7 (𝑥 = ∅ → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
98albidv 1915 . . . . . 6 (𝑥 = ∅ → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
10 sseq2 4000 . . . . . . . 8 (𝑥 = 𝑦 → (𝑏𝑥𝑏𝑦))
1110imbi1d 341 . . . . . . 7 (𝑥 = 𝑦 → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏𝑦𝑏 ∈ Fin)))
1211albidv 1915 . . . . . 6 (𝑥 = 𝑦 → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏𝑦𝑏 ∈ Fin)))
13 sseq2 4000 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏𝑥𝑏 ⊆ (𝑦 ∪ {𝑧})))
1413imbi1d 341 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
1514albidv 1915 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
16 sseq2 4000 . . . . . . . 8 (𝑥 = 𝐴 → (𝑏𝑥𝑏𝐴))
1716imbi1d 341 . . . . . . 7 (𝑥 = 𝐴 → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏𝐴𝑏 ∈ Fin)))
1817albidv 1915 . . . . . 6 (𝑥 = 𝐴 → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏𝐴𝑏 ∈ Fin)))
19 ss0 4390 . . . . . . . 8 (𝑏 ⊆ ∅ → 𝑏 = ∅)
20 0fin 9167 . . . . . . . 8 ∅ ∈ Fin
2119, 20eqeltrdi 2833 . . . . . . 7 (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
2221ax-gen 1789 . . . . . 6 𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
23 sseq1 3999 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏𝑦𝑐𝑦))
24 eleq1w 2808 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin))
2523, 24imbi12d 344 . . . . . . . . . 10 (𝑏 = 𝑐 → ((𝑏𝑦𝑏 ∈ Fin) ↔ (𝑐𝑦𝑐 ∈ Fin)))
2625cbvalvw 2031 . . . . . . . . 9 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) ↔ ∀𝑐(𝑐𝑦𝑐 ∈ Fin))
27 simp1 1133 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐𝑦𝑐 ∈ Fin))
28 snssi 4803 . . . . . . . . . . . . . . . . 17 (𝑧𝑏 → {𝑧} ⊆ 𝑏)
29 undif 4473 . . . . . . . . . . . . . . . . 17 ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
3028, 29sylib 217 . . . . . . . . . . . . . . . 16 (𝑧𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
31 uncom 4145 . . . . . . . . . . . . . . . 16 ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧})
3230, 31eqtr3di 2779 . . . . . . . . . . . . . . 15 (𝑧𝑏𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))
33 uncom 4145 . . . . . . . . . . . . . . . . 17 (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
3433sseq2i 4003 . . . . . . . . . . . . . . . 16 (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦))
35 ssundif 4479 . . . . . . . . . . . . . . . 16 (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)
3634, 35sylbb 218 . . . . . . . . . . . . . . 15 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦)
3732, 36anim12ci 613 . . . . . . . . . . . . . 14 ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
38373adant1 1127 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
39 3anass 1092 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))))
4027, 38, 39sylanbrc 582 . . . . . . . . . . . 12 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
41 vex 3470 . . . . . . . . . . . . . . . . 17 𝑏 ∈ V
4241difexi 5318 . . . . . . . . . . . . . . . 16 (𝑏 ∖ {𝑧}) ∈ V
43 sseq1 3999 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦))
44 eleq1 2813 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin))
4543, 44imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐𝑦𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)))
4642, 45spcv 3587 . . . . . . . . . . . . . . 15 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))
4746imp 406 . . . . . . . . . . . . . 14 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin)
48 snfi 9040 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
49 unfi 9168 . . . . . . . . . . . . . 14 (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
5047, 48, 49sylancl 585 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
51 eleq1 2813 . . . . . . . . . . . . . 14 (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin))
5251biimparc 479 . . . . . . . . . . . . 13 ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
5350, 52stoic3 1770 . . . . . . . . . . . 12 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
5440, 53syl 17 . . . . . . . . . . 11 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)
55543expib 1119 . . . . . . . . . 10 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
5655alrimiv 1922 . . . . . . . . 9 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
5726, 56sylbi 216 . . . . . . . 8 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
58 disjsn 4707 . . . . . . . . . . . . 13 ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑏)
59 disjssun 4459 . . . . . . . . . . . . 13 ((𝑏 ∩ {𝑧}) = ∅ → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏𝑦))
6058, 59sylbir 234 . . . . . . . . . . . 12 𝑧𝑏 → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏𝑦))
6160biimpa 476 . . . . . . . . . . 11 ((¬ 𝑧𝑏𝑏 ⊆ ({𝑧} ∪ 𝑦)) → 𝑏𝑦)
6234, 61sylan2b 593 . . . . . . . . . 10 ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏𝑦)
6362imim1i 63 . . . . . . . . 9 ((𝑏𝑦𝑏 ∈ Fin) → ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
6463alimi 1805 . . . . . . . 8 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
65 exmid 891 . . . . . . . . . . . 12 (𝑧𝑏 ∨ ¬ 𝑧𝑏)
6665jctl 523 . . . . . . . . . . 11 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧𝑏 ∨ ¬ 𝑧𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
67 andir 1005 . . . . . . . . . . 11 (((𝑧𝑏 ∨ ¬ 𝑧𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))))
6866, 67sylib 217 . . . . . . . . . 10 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))))
69 pm3.44 956 . . . . . . . . . 10 ((((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin))
7068, 69syl5 34 . . . . . . . . 9 ((((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7170alanimi 1810 . . . . . . . 8 ((∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ∀𝑏((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7257, 64, 71syl2anc 583 . . . . . . 7 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7372a1i 11 . . . . . 6 (𝑦 ∈ Fin → (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
749, 12, 15, 18, 22, 73findcard2 9160 . . . . 5 (𝐴 ∈ Fin → ∀𝑏(𝑏𝐴𝑏 ∈ Fin))
757419.21bi 2174 . . . 4 (𝐴 ∈ Fin → (𝑏𝐴𝑏 ∈ Fin))
766, 75vtoclg 3535 . . 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 844  w3a 1084  wal 1531   = wceq 1533  wcel 2098  Vcvv 3466  cdif 3937  cun 3938  cin 3939  wss 3940  c0 4314  {csn 4620  Fincfn 8935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-om 7849  df-1o 8461  df-en 8936  df-fin 8939
This theorem is referenced by:  pwfilem  9173  diffi  9175  fnfi  9177  f1domfi  9180  domfi  9188  ssfid  9263  infi  9264  finresfin  9266  findcard3  9281  findcard3OLD  9282  unfir  9310  xpfi  9313  fofinf1o  9323  cnvfiALT  9330  f1fi  9335  imafiALT  9341  mapfi  9344  ixpfi2  9346  mptfi  9347  cnvimamptfin  9349  suppssfifsupp  9374  snopfsupp  9382  fsuppres  9384  sniffsupp  9391  elfiun  9421  oemapvali  9675  ackbij2lem1  10210  ackbij1lem11  10221  fin23lem26  10316  fin23lem23  10317  fin23lem21  10330  fin11a  10374  isfin1-3  10377  axcclem  10448  ssnn0fi  13947  hashun3  14341  hashss  14366  hashssdif  14369  hashsslei  14383  hashreshashfun  14396  hashbclem  14408  hashf1lem2  14414  seqcoll2  14423  pr2pwpr  14437  fsumless  15739  cvgcmpce  15761  qshash  15770  incexclem  15779  incexc  15780  incexc2  15781  fprodmodd  15938  sumeven  16327  sumodd  16328  bitsfi  16375  bitsinv1  16380  bitsinvp1  16387  sadcaddlem  16395  sadadd2lem  16397  sadadd3  16399  sadaddlem  16404  sadasslem  16408  sadeq  16410  phicl2  16700  phibnd  16703  hashdvds  16707  phiprmpw  16708  phimullem  16711  eulerthlem2  16714  eulerth  16715  phisum  16722  sumhash  16828  prmreclem2  16849  prmreclem3  16850  prmreclem4  16851  prmreclem5  16852  1arith  16859  hashbccl  16935  prmgaplem3  16985  lagsubg  19111  symgfisg  19378  symggen2  19381  odcl2  19475  sylow1lem2  19509  sylow1lem3  19510  sylow1lem4  19511  sylow1lem5  19512  pgpssslw  19524  sylow2alem2  19528  sylow2a  19529  sylow2blem3  19532  sylow3lem3  19539  sylow3lem6  19542  gsumval3lem1  19815  gsumval3lem2  19816  gsumval3  19817  gsumpt  19872  ablfacrplem  19977  ablfacrp2  19979  ablfac1c  19983  ablfac1eulem  19984  ablfac1eu  19985  dsmmfi  21601  mplsubg  21871  mpllss  21872  psrbagsn  21934  psr1baslem  22027  submabas  22402  mdetdiaglem  22422  maducoeval2  22464  fctop  22829  restfpw  23005  fincmp  23219  cmpfi  23234  bwth  23236  finlocfin  23346  lfinpfin  23350  locfincmp  23352  1stckgenlem  23379  ptbasfi  23407  ptcnplem  23447  ptcmpfi  23639  cfinfil  23719  ufinffr  23755  fin1aufil  23758  tsmsres  23970  ovoliunlem1  25353  ovolicc2lem4  25371  ovolicc2lem5  25372  i1fima  25529  i1fd  25532  itg1cl  25536  itg1ge0  25537  i1f0  25538  i1f1  25541  i1fmul  25547  itg1addlem4  25550  itg1addlem4OLD  25551  itg1mulc  25556  itg10a  25562  itg1ge0a  25563  itg1climres  25566  plyexmo  26167  aannenlem2  26183  aalioulem2  26187  birthday  26802  wilthlem2  26917  ppifi  26954  prmdvdsfi  26955  ppiprm  26999  chtprm  27001  chtdif  27006  efchtdvds  27007  ppidif  27011  ppiltx  27025  mumul  27029  sqff1o  27030  musum  27039  ppiub  27053  vmasum  27065  logfac2  27066  dchrabs  27109  dchrptlem1  27113  dchrptlem2  27114  dchrpt  27116  lgsquadlem1  27229  lgsquadlem2  27230  lgsquadlem3  27231  chebbnd1lem1  27318  chtppilimlem1  27322  rpvmasum2  27361  dchrisum0re  27362  rplogsum  27376  dirith2  27377  cusgrfi  29184  hashwwlksnext  29637  relfi  32302  imafi2  32405  unifi3  32406  ffsrn  32423  xrge0tsmsd  32677  gsumle  32710  rmfsupp2  32853  hasheuni  33572  carsgclctunlem1  33805  sibfof  33828  sitgclg  33830  oddpwdc  33842  eulerpartlems  33848  eulerpartlemb  33856  eulerpartlemmf  33863  eulerpartlemgf  33867  eulerpartlemgs2  33868  coinfliplem  33966  coinflippv  33971  ballotlemfelz  33978  ballotlemfp1  33979  ballotlemfc0  33980  ballotlemfcc  33981  ballotlemiex  33989  ballotlemsup  33992  ballotlemfg  34013  ballotlemfrc  34014  ballotlemfrceq  34016  ballotth  34025  breprexpnat  34135  hgt750lemb  34157  hgt750leme  34159  fisshasheq  34593  deranglem  34646  subfacp1lem3  34662  subfacp1lem5  34664  subfacp1lem6  34665  erdszelem2  34672  erdszelem8  34678  erdsze2lem2  34684  snmlff  34809  mvrsfpw  34986  finminlem  35693  topdifinffinlem  36718  matunitlindflem1  36974  poimirlem9  36987  poimirlem26  37004  poimirlem27  37005  poimirlem28  37006  poimirlem30  37008  poimirlem32  37010  itg2addnclem2  37030  nnubfi  37108  nninfnub  37109  sstotbnd2  37132  cntotbnd  37154  sticksstones1  41455  rencldnfilem  42047  jm2.22  42223  jm2.23  42224  filnm  42321  pwssfi  44220  disjinfi  44376  fsumiunss  44776  fprodexp  44795  fprodabs2  44796  mccllem  44798  sumnnodd  44831  fprodcncf  45101  dvmptfprod  45146  dvnprodlem1  45147  dvnprodlem2  45148  fourierdlem25  45333  fourierdlem37  45345  fourierdlem51  45358  fourierdlem79  45386  fouriersw  45432  etransclem16  45451  etransclem24  45459  etransclem33  45468  etransclem44  45479  sge0resplit  45607  sge0iunmptlemfi  45614  sge0iunmptlemre  45616  carageniuncllem2  45723  hsphoidmvle2  45786  hsphoidmvle  45787  hoidmvlelem4  45799  hoidmvlelem5  45800  upwrdfi  46086  fmtnoinf  46689  perfectALTVlem2  46875  rmsuppfi  47238  mndpsuppfi  47240  scmsuppfi  47242  suppmptcfin  47244
  Copyright terms: Public domain W3C validator