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

Theorem ssfi 9211
Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5370, see ssfiALT 9212. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5370. (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 5328 . . 3 ((𝐵𝐴𝐴 ∈ Fin) → 𝐵 ∈ V)
21ancoms 458 . 2 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ V)
3 sseq1 4020 . . . . . 6 (𝑏 = 𝐵 → (𝑏𝐴𝐵𝐴))
4 eleq1 2826 . . . . . 6 (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin))
53, 4imbi12d 344 . . . . 5 (𝑏 = 𝐵 → ((𝑏𝐴𝑏 ∈ Fin) ↔ (𝐵𝐴𝐵 ∈ Fin)))
65imbi2d 340 . . . 4 (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏𝐴𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵𝐴𝐵 ∈ Fin))))
7 sseq2 4021 . . . . . . . 8 (𝑥 = ∅ → (𝑏𝑥𝑏 ⊆ ∅))
87imbi1d 341 . . . . . . 7 (𝑥 = ∅ → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
98albidv 1917 . . . . . 6 (𝑥 = ∅ → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
10 sseq2 4021 . . . . . . . 8 (𝑥 = 𝑦 → (𝑏𝑥𝑏𝑦))
1110imbi1d 341 . . . . . . 7 (𝑥 = 𝑦 → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏𝑦𝑏 ∈ Fin)))
1211albidv 1917 . . . . . 6 (𝑥 = 𝑦 → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏𝑦𝑏 ∈ Fin)))
13 sseq2 4021 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏𝑥𝑏 ⊆ (𝑦 ∪ {𝑧})))
1413imbi1d 341 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
1514albidv 1917 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
16 sseq2 4021 . . . . . . . 8 (𝑥 = 𝐴 → (𝑏𝑥𝑏𝐴))
1716imbi1d 341 . . . . . . 7 (𝑥 = 𝐴 → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏𝐴𝑏 ∈ Fin)))
1817albidv 1917 . . . . . 6 (𝑥 = 𝐴 → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏𝐴𝑏 ∈ Fin)))
19 ss0 4407 . . . . . . . 8 (𝑏 ⊆ ∅ → 𝑏 = ∅)
20 0fi 9080 . . . . . . . 8 ∅ ∈ Fin
2119, 20eqeltrdi 2846 . . . . . . 7 (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
2221ax-gen 1791 . . . . . 6 𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
23 sseq1 4020 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏𝑦𝑐𝑦))
24 eleq1w 2821 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin))
2523, 24imbi12d 344 . . . . . . . . . 10 (𝑏 = 𝑐 → ((𝑏𝑦𝑏 ∈ Fin) ↔ (𝑐𝑦𝑐 ∈ Fin)))
2625cbvalvw 2032 . . . . . . . . 9 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) ↔ ∀𝑐(𝑐𝑦𝑐 ∈ Fin))
27 simp1 1135 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐𝑦𝑐 ∈ Fin))
28 snssi 4812 . . . . . . . . . . . . . . . . 17 (𝑧𝑏 → {𝑧} ⊆ 𝑏)
29 undif 4487 . . . . . . . . . . . . . . . . 17 ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
3028, 29sylib 218 . . . . . . . . . . . . . . . 16 (𝑧𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
31 uncom 4167 . . . . . . . . . . . . . . . 16 ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧})
3230, 31eqtr3di 2789 . . . . . . . . . . . . . . 15 (𝑧𝑏𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))
33 uncom 4167 . . . . . . . . . . . . . . . . 17 (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
3433sseq2i 4024 . . . . . . . . . . . . . . . 16 (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦))
35 ssundif 4493 . . . . . . . . . . . . . . . 16 (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)
3634, 35sylbb 219 . . . . . . . . . . . . . . 15 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦)
3732, 36anim12ci 614 . . . . . . . . . . . . . 14 ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
38373adant1 1129 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
39 3anass 1094 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))))
4027, 38, 39sylanbrc 583 . . . . . . . . . . . 12 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
41 vex 3481 . . . . . . . . . . . . . . . . 17 𝑏 ∈ V
4241difexi 5335 . . . . . . . . . . . . . . . 16 (𝑏 ∖ {𝑧}) ∈ V
43 sseq1 4020 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦))
44 eleq1 2826 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin))
4543, 44imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐𝑦𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)))
4642, 45spcv 3604 . . . . . . . . . . . . . . 15 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))
4746imp 406 . . . . . . . . . . . . . 14 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin)
48 snfi 9081 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
49 unfi 9209 . . . . . . . . . . . . . 14 (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
5047, 48, 49sylancl 586 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
51 eleq1 2826 . . . . . . . . . . . . . 14 (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin))
5251biimparc 479 . . . . . . . . . . . . 13 ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
5350, 52stoic3 1772 . . . . . . . . . . . 12 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
5440, 53syl 17 . . . . . . . . . . 11 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)
55543expib 1121 . . . . . . . . . 10 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
5655alrimiv 1924 . . . . . . . . 9 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
5726, 56sylbi 217 . . . . . . . 8 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
58 disjsn 4715 . . . . . . . . . . . . 13 ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑏)
59 disjssun 4473 . . . . . . . . . . . . 13 ((𝑏 ∩ {𝑧}) = ∅ → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏𝑦))
6058, 59sylbir 235 . . . . . . . . . . . 12 𝑧𝑏 → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏𝑦))
6160biimpa 476 . . . . . . . . . . 11 ((¬ 𝑧𝑏𝑏 ⊆ ({𝑧} ∪ 𝑦)) → 𝑏𝑦)
6234, 61sylan2b 594 . . . . . . . . . 10 ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏𝑦)
6362imim1i 63 . . . . . . . . 9 ((𝑏𝑦𝑏 ∈ Fin) → ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
6463alimi 1807 . . . . . . . 8 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
65 exmid 894 . . . . . . . . . . . 12 (𝑧𝑏 ∨ ¬ 𝑧𝑏)
6665jctl 523 . . . . . . . . . . 11 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧𝑏 ∨ ¬ 𝑧𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
67 andir 1010 . . . . . . . . . . 11 (((𝑧𝑏 ∨ ¬ 𝑧𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))))
6866, 67sylib 218 . . . . . . . . . 10 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))))
69 pm3.44 961 . . . . . . . . . 10 ((((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin))
7068, 69syl5 34 . . . . . . . . 9 ((((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7170alanimi 1812 . . . . . . . 8 ((∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ∀𝑏((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7257, 64, 71syl2anc 584 . . . . . . 7 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7372a1i 11 . . . . . 6 (𝑦 ∈ Fin → (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
749, 12, 15, 18, 22, 73findcard2 9202 . . . . 5 (𝐴 ∈ Fin → ∀𝑏(𝑏𝐴𝑏 ∈ Fin))
757419.21bi 2186 . . . 4 (𝐴 ∈ Fin → (𝑏𝐴𝑏 ∈ Fin))
766, 75vtoclg 3553 . . 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 206  wa 395  wo 847  w3a 1086  wal 1534   = wceq 1536  wcel 2105  Vcvv 3477  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  {csn 4630  Fincfn 8983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-om 7887  df-1o 8504  df-en 8984  df-fin 8987
This theorem is referenced by:  diffi  9213  fnfi  9215  f1domfi  9218  domfi  9226  ssfid  9298  infi  9299  finresfin  9301  findcard3  9315  findcard3OLD  9316  unfir  9343  f1fi  9349  imafi  9350  pwfilem  9353  xpfi  9355  fofinf1o  9369  cnvfiALT  9376  mapfi  9385  ixpfi2  9387  mptfi  9388  cnvimamptfin  9390  suppssfifsupp  9417  snopfsupp  9428  fsuppres  9430  sniffsupp  9437  elfiun  9467  oemapvali  9721  ackbij2lem1  10255  ackbij1lem11  10266  fin23lem26  10362  fin23lem23  10363  fin23lem21  10376  fin11a  10420  isfin1-3  10423  axcclem  10494  ssnn0fi  14022  hashun3  14419  hashss  14444  hashssdif  14447  hashsslei  14461  hashreshashfun  14474  hashbclem  14487  hashf1lem2  14491  seqcoll2  14500  pr2pwpr  14514  fsumless  15828  cvgcmpce  15850  qshash  15859  incexclem  15868  incexc  15869  incexc2  15870  fprodmodd  16029  sumeven  16420  sumodd  16421  bitsfi  16470  bitsinv1  16475  bitsinvp1  16482  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  sadaddlem  16499  sadasslem  16503  sadeq  16505  phicl2  16801  phibnd  16804  hashdvds  16808  phiprmpw  16809  phimullem  16812  eulerthlem2  16815  eulerth  16816  phisum  16823  sumhash  16929  prmreclem2  16950  prmreclem3  16951  prmreclem4  16952  prmreclem5  16953  1arith  16960  hashbccl  17036  prmgaplem3  17086  mndpsuppfi  18791  lagsubg  19225  symgfisg  19500  symggen2  19503  odcl2  19597  sylow1lem2  19631  sylow1lem3  19632  sylow1lem4  19633  sylow1lem5  19634  pgpssslw  19646  sylow2alem2  19650  sylow2a  19651  sylow2blem3  19654  sylow3lem3  19661  sylow3lem6  19664  gsumval3lem1  19937  gsumval3lem2  19938  gsumval3  19939  gsumpt  19994  ablfacrplem  20099  ablfacrp2  20101  ablfac1c  20105  ablfac1eulem  20106  ablfac1eu  20107  dsmmfi  21775  mplsubg  22039  mpllss  22040  psrbagsn  22104  psr1baslem  22201  submabas  22599  mdetdiaglem  22619  maducoeval2  22661  fctop  23026  restfpw  23202  fincmp  23416  cmpfi  23431  bwth  23433  finlocfin  23543  lfinpfin  23547  locfincmp  23549  1stckgenlem  23576  ptbasfi  23604  ptcnplem  23644  ptcmpfi  23836  cfinfil  23916  ufinffr  23952  fin1aufil  23955  tsmsres  24167  ovoliunlem1  25550  ovolicc2lem4  25568  ovolicc2lem5  25569  i1fima  25726  i1fd  25729  itg1cl  25733  itg1ge0  25734  i1f0  25735  i1f1  25738  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  itg1mulc  25753  itg10a  25759  itg1ge0a  25760  itg1climres  25763  plyexmo  26369  aannenlem2  26385  aalioulem2  26389  birthday  27011  wilthlem2  27126  ppifi  27163  prmdvdsfi  27164  ppiprm  27208  chtprm  27210  chtdif  27215  efchtdvds  27216  ppidif  27220  ppiltx  27234  mumul  27238  sqff1o  27239  musum  27248  ppiub  27262  vmasum  27274  logfac2  27275  dchrabs  27318  dchrptlem1  27322  dchrptlem2  27323  dchrpt  27325  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  chebbnd1lem1  27527  chtppilimlem1  27531  rpvmasum2  27570  dchrisum0re  27571  rplogsum  27585  dirith2  27586  cusgrfi  29490  hashwwlksnext  29943  relfi  32621  imafi2  32728  unifi3  32729  ffsrn  32746  xrge0tsmsd  33047  gsumle  33083  rmfsupp2  33227  hasheuni  34065  carsgclctunlem1  34298  sibfof  34321  sitgclg  34323  oddpwdc  34335  eulerpartlems  34341  eulerpartlemb  34349  eulerpartlemmf  34356  eulerpartlemgf  34360  eulerpartlemgs2  34361  coinfliplem  34459  coinflippv  34464  ballotlemfelz  34471  ballotlemfp1  34472  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemiex  34482  ballotlemsup  34485  ballotlemfg  34506  ballotlemfrc  34507  ballotlemfrceq  34509  ballotth  34518  breprexpnat  34627  hgt750lemb  34649  hgt750leme  34651  fisshasheq  35098  deranglem  35150  subfacp1lem3  35166  subfacp1lem5  35168  subfacp1lem6  35169  erdszelem2  35176  erdszelem8  35182  erdsze2lem2  35188  snmlff  35313  mvrsfpw  35490  finminlem  36300  topdifinffinlem  37329  matunitlindflem1  37602  poimirlem9  37615  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem30  37636  poimirlem32  37638  itg2addnclem2  37658  nnubfi  37736  nninfnub  37737  sstotbnd2  37760  cntotbnd  37782  sticksstones1  42127  rencldnfilem  42807  jm2.22  42983  jm2.23  42984  filnm  43078  pwssfi  44984  disjinfi  45134  fsumiunss  45530  fprodexp  45549  fprodabs2  45550  mccllem  45552  sumnnodd  45585  fprodcncf  45855  dvnprodlem2  45902  fourierdlem25  46087  fourierdlem37  46099  fourierdlem51  46112  fourierdlem79  46140  fouriersw  46186  etransclem16  46205  etransclem24  46213  etransclem33  46222  etransclem44  46233  sge0resplit  46361  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  carageniuncllem2  46477  hsphoidmvle2  46540  hsphoidmvle  46541  hoidmvlelem4  46553  hoidmvlelem5  46554  upwrdfi  46840  fmtnoinf  47460  perfectALTVlem2  47646  rmsuppfi  48216  scmsuppfi  48218  suppmptcfin  48220
  Copyright terms: Public domain W3C validator