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

Theorem ssfi 9016
Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5302, see ssfiALT 9017. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5302. (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 5261 . . 3 ((𝐵𝐴𝐴 ∈ Fin) → 𝐵 ∈ V)
21ancoms 459 . 2 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵 ∈ V)
3 sseq1 3955 . . . . . 6 (𝑏 = 𝐵 → (𝑏𝐴𝐵𝐴))
4 eleq1 2824 . . . . . 6 (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin))
53, 4imbi12d 344 . . . . 5 (𝑏 = 𝐵 → ((𝑏𝐴𝑏 ∈ Fin) ↔ (𝐵𝐴𝐵 ∈ Fin)))
65imbi2d 340 . . . 4 (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏𝐴𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵𝐴𝐵 ∈ Fin))))
7 sseq2 3956 . . . . . . . 8 (𝑥 = ∅ → (𝑏𝑥𝑏 ⊆ ∅))
87imbi1d 341 . . . . . . 7 (𝑥 = ∅ → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
98albidv 1922 . . . . . 6 (𝑥 = ∅ → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)))
10 sseq2 3956 . . . . . . . 8 (𝑥 = 𝑦 → (𝑏𝑥𝑏𝑦))
1110imbi1d 341 . . . . . . 7 (𝑥 = 𝑦 → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏𝑦𝑏 ∈ Fin)))
1211albidv 1922 . . . . . 6 (𝑥 = 𝑦 → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏𝑦𝑏 ∈ Fin)))
13 sseq2 3956 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏𝑥𝑏 ⊆ (𝑦 ∪ {𝑧})))
1413imbi1d 341 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
1514albidv 1922 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
16 sseq2 3956 . . . . . . . 8 (𝑥 = 𝐴 → (𝑏𝑥𝑏𝐴))
1716imbi1d 341 . . . . . . 7 (𝑥 = 𝐴 → ((𝑏𝑥𝑏 ∈ Fin) ↔ (𝑏𝐴𝑏 ∈ Fin)))
1817albidv 1922 . . . . . 6 (𝑥 = 𝐴 → (∀𝑏(𝑏𝑥𝑏 ∈ Fin) ↔ ∀𝑏(𝑏𝐴𝑏 ∈ Fin)))
19 ss0 4342 . . . . . . . 8 (𝑏 ⊆ ∅ → 𝑏 = ∅)
20 0fin 9014 . . . . . . . 8 ∅ ∈ Fin
2119, 20eqeltrdi 2845 . . . . . . 7 (𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
2221ax-gen 1796 . . . . . 6 𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin)
23 sseq1 3955 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏𝑦𝑐𝑦))
24 eleq1w 2819 . . . . . . . . . . 11 (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin))
2523, 24imbi12d 344 . . . . . . . . . 10 (𝑏 = 𝑐 → ((𝑏𝑦𝑏 ∈ Fin) ↔ (𝑐𝑦𝑐 ∈ Fin)))
2625cbvalvw 2038 . . . . . . . . 9 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) ↔ ∀𝑐(𝑐𝑦𝑐 ∈ Fin))
27 simp1 1135 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐𝑦𝑐 ∈ Fin))
28 snssi 4752 . . . . . . . . . . . . . . . . 17 (𝑧𝑏 → {𝑧} ⊆ 𝑏)
29 undif 4425 . . . . . . . . . . . . . . . . 17 ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
3028, 29sylib 217 . . . . . . . . . . . . . . . 16 (𝑧𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏)
31 uncom 4097 . . . . . . . . . . . . . . . 16 ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧})
3230, 31eqtr3di 2791 . . . . . . . . . . . . . . 15 (𝑧𝑏𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))
33 uncom 4097 . . . . . . . . . . . . . . . . 17 (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
3433sseq2i 3959 . . . . . . . . . . . . . . . 16 (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦))
35 ssundif 4429 . . . . . . . . . . . . . . . 16 (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)
3634, 35sylbb 218 . . . . . . . . . . . . . . 15 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦)
3732, 36anim12ci 614 . . . . . . . . . . . . . 14 ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
38373adant1 1129 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
39 3anass 1094 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))))
4027, 38, 39sylanbrc 583 . . . . . . . . . . . 12 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))
41 vex 3444 . . . . . . . . . . . . . . . . 17 𝑏 ∈ V
4241difexi 5266 . . . . . . . . . . . . . . . 16 (𝑏 ∖ {𝑧}) ∈ V
43 sseq1 3955 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦))
44 eleq1 2824 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin))
4543, 44imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐𝑦𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)))
4642, 45spcv 3552 . . . . . . . . . . . . . . 15 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))
4746imp 407 . . . . . . . . . . . . . 14 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin)
48 snfi 8887 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
49 unfi 9015 . . . . . . . . . . . . . 14 (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
5047, 48, 49sylancl 586 . . . . . . . . . . . . 13 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)
51 eleq1 2824 . . . . . . . . . . . . . 14 (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin))
5251biimparc 480 . . . . . . . . . . . . 13 ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
5350, 52stoic3 1777 . . . . . . . . . . . 12 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin)
5440, 53syl 17 . . . . . . . . . . 11 ((∀𝑐(𝑐𝑦𝑐 ∈ Fin) ∧ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)
55543expib 1121 . . . . . . . . . 10 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
5655alrimiv 1929 . . . . . . . . 9 (∀𝑐(𝑐𝑦𝑐 ∈ Fin) → ∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
5726, 56sylbi 216 . . . . . . . 8 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
58 disjsn 4656 . . . . . . . . . . . . 13 ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑏)
59 disjssun 4411 . . . . . . . . . . . . 13 ((𝑏 ∩ {𝑧}) = ∅ → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏𝑦))
6058, 59sylbir 234 . . . . . . . . . . . 12 𝑧𝑏 → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏𝑦))
6160biimpa 477 . . . . . . . . . . 11 ((¬ 𝑧𝑏𝑏 ⊆ ({𝑧} ∪ 𝑦)) → 𝑏𝑦)
6234, 61sylan2b 594 . . . . . . . . . 10 ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏𝑦)
6362imim1i 63 . . . . . . . . 9 ((𝑏𝑦𝑏 ∈ Fin) → ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
6463alimi 1812 . . . . . . . 8 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin))
65 exmid 892 . . . . . . . . . . . 12 (𝑧𝑏 ∨ ¬ 𝑧𝑏)
6665jctl 524 . . . . . . . . . . 11 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧𝑏 ∨ ¬ 𝑧𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))
67 andir 1006 . . . . . . . . . . 11 (((𝑧𝑏 ∨ ¬ 𝑧𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))))
6866, 67sylib 217 . . . . . . . . . 10 (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))))
69 pm3.44 957 . . . . . . . . . 10 ((((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin))
7068, 69syl5 34 . . . . . . . . 9 ((((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7170alanimi 1817 . . . . . . . 8 ((∀𝑏((𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ∀𝑏((¬ 𝑧𝑏𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7257, 64, 71syl2anc 584 . . . . . . 7 (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))
7372a1i 11 . . . . . 6 (𝑦 ∈ Fin → (∀𝑏(𝑏𝑦𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)))
749, 12, 15, 18, 22, 73findcard2 9007 . . . . 5 (𝐴 ∈ Fin → ∀𝑏(𝑏𝐴𝑏 ∈ Fin))
757419.21bi 2181 . . . 4 (𝐴 ∈ Fin → (𝑏𝐴𝑏 ∈ Fin))
766, 75vtoclg 3513 . . 3 (𝐵 ∈ V → (𝐴 ∈ Fin → (𝐵𝐴𝐵 ∈ Fin)))
7776impd 411 . 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 396  wo 844  w3a 1086  wal 1538   = wceq 1540  wcel 2105  Vcvv 3440  cdif 3893  cun 3894  cin 3895  wss 3896  c0 4266  {csn 4570  Fincfn 8782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366  ax-un 7629
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-om 7759  df-1o 8345  df-en 8783  df-fin 8786
This theorem is referenced by:  pwfilem  9020  diffi  9022  fnfi  9024  f1domfi  9027  domfi  9035  ssfid  9110  infi  9111  finresfin  9113  findcard3  9128  findcard3OLD  9129  unfir  9157  xpfi  9160  fofinf1o  9170  cnvfiALT  9177  f1fi  9182  imafiALT  9188  mapfi  9191  ixpfi2  9193  mptfi  9194  cnvimamptfin  9196  suppssfifsupp  9219  snopfsupp  9227  fsuppres  9229  sniffsupp  9235  elfiun  9265  oemapvali  9519  ackbij2lem1  10054  ackbij1lem11  10065  fin23lem26  10160  fin23lem23  10161  fin23lem21  10174  fin11a  10218  isfin1-3  10221  axcclem  10292  ssnn0fi  13784  hashun3  14177  hashss  14202  hashssdif  14205  hashsslei  14219  hashreshashfun  14232  hashbclem  14242  hashf1lem2  14248  seqcoll2  14257  pr2pwpr  14271  fsumless  15584  cvgcmpce  15606  qshash  15615  incexclem  15624  incexc  15625  incexc2  15626  fprodmodd  15783  sumeven  16172  sumodd  16173  bitsfi  16220  bitsinv1  16225  bitsinvp1  16232  sadcaddlem  16240  sadadd2lem  16242  sadadd3  16244  sadaddlem  16249  sadasslem  16253  sadeq  16255  phicl2  16543  phibnd  16546  hashdvds  16550  phiprmpw  16551  phimullem  16554  eulerthlem2  16557  eulerth  16558  phisum  16565  sumhash  16671  prmreclem2  16692  prmreclem3  16693  prmreclem4  16694  prmreclem5  16695  1arith  16702  hashbccl  16778  prmgaplem3  16828  lagsubg  18891  symgfisg  19149  symggen2  19152  odcl2  19245  sylow1lem2  19277  sylow1lem3  19278  sylow1lem4  19279  sylow1lem5  19280  pgpssslw  19292  sylow2alem2  19296  sylow2a  19297  sylow2blem3  19300  sylow3lem3  19307  sylow3lem6  19310  gsumval3lem1  19578  gsumval3lem2  19579  gsumval3  19580  gsumpt  19635  ablfacrplem  19740  ablfacrp2  19742  ablfac1c  19746  ablfac1eulem  19747  ablfac1eu  19748  dsmmfi  21025  mplsubg  21288  mpllss  21289  psrbagsn  21351  psr1baslem  21436  submabas  21807  mdetdiaglem  21827  maducoeval2  21869  fctop  22234  restfpw  22410  fincmp  22624  cmpfi  22639  bwth  22641  finlocfin  22751  lfinpfin  22755  locfincmp  22757  1stckgenlem  22784  ptbasfi  22812  ptcnplem  22852  ptcmpfi  23044  cfinfil  23124  ufinffr  23160  fin1aufil  23163  tsmsres  23375  ovoliunlem1  24746  ovolicc2lem4  24764  ovolicc2lem5  24765  i1fima  24922  i1fd  24925  itg1cl  24929  itg1ge0  24930  i1f0  24931  i1f1  24934  i1fmul  24940  itg1addlem4  24943  itg1addlem4OLD  24944  itg1mulc  24949  itg10a  24955  itg1ge0a  24956  itg1climres  24959  plyexmo  25553  aannenlem2  25569  aalioulem2  25573  birthday  26184  wilthlem2  26298  ppifi  26335  prmdvdsfi  26336  ppiprm  26380  chtprm  26382  chtdif  26387  efchtdvds  26388  ppidif  26392  ppiltx  26406  mumul  26410  sqff1o  26411  musum  26420  ppiub  26432  vmasum  26444  logfac2  26445  dchrabs  26488  dchrptlem1  26492  dchrptlem2  26493  dchrpt  26495  lgsquadlem1  26608  lgsquadlem2  26609  lgsquadlem3  26610  chebbnd1lem1  26697  chtppilimlem1  26701  rpvmasum2  26740  dchrisum0re  26741  rplogsum  26755  dirith2  26756  cusgrfi  27958  hashwwlksnext  28411  relfi  31072  imafi2  31177  unifi3  31178  ffsrn  31195  xrge0tsmsd  31448  gsumle  31481  rmfsupp2  31623  hasheuni  32189  carsgclctunlem1  32420  sibfof  32443  sitgclg  32445  oddpwdc  32457  eulerpartlems  32463  eulerpartlemb  32471  eulerpartlemmf  32478  eulerpartlemgf  32482  eulerpartlemgs2  32483  coinfliplem  32581  coinflippv  32586  ballotlemfelz  32593  ballotlemfp1  32594  ballotlemfc0  32595  ballotlemfcc  32596  ballotlemiex  32604  ballotlemsup  32607  ballotlemfg  32628  ballotlemfrc  32629  ballotlemfrceq  32631  ballotth  32640  breprexpnat  32750  hgt750lemb  32772  hgt750leme  32774  fisshasheq  33208  deranglem  33263  subfacp1lem3  33279  subfacp1lem5  33281  subfacp1lem6  33282  erdszelem2  33289  erdszelem8  33295  erdsze2lem2  33301  snmlff  33426  mvrsfpw  33603  finminlem  34577  topdifinffinlem  35595  matunitlindflem1  35850  poimirlem9  35863  poimirlem26  35880  poimirlem27  35881  poimirlem28  35882  poimirlem30  35884  poimirlem32  35886  itg2addnclem2  35906  nnubfi  35985  nninfnub  35986  sstotbnd2  36009  cntotbnd  36031  sticksstones1  40331  rencldnfilem  40863  jm2.22  41039  jm2.23  41040  filnm  41137  pwssfi  42832  disjinfi  42977  fsumiunss  43371  fprodexp  43390  fprodabs2  43391  mccllem  43393  sumnnodd  43426  fprodcncf  43696  dvmptfprod  43741  dvnprodlem1  43742  dvnprodlem2  43743  fourierdlem25  43928  fourierdlem37  43940  fourierdlem51  43953  fourierdlem79  43981  fouriersw  44027  etransclem16  44046  etransclem24  44054  etransclem33  44063  etransclem44  44074  sge0resplit  44200  sge0iunmptlemfi  44207  sge0iunmptlemre  44209  carageniuncllem2  44316  hsphoidmvle2  44379  hsphoidmvle  44380  hoidmvlelem4  44392  hoidmvlelem5  44393  fmtnoinf  45258  perfectALTVlem2  45444  rmsuppfi  45979  mndpsuppfi  45981  scmsuppfi  45983  suppmptcfin  45985
  Copyright terms: Public domain W3C validator