![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isfinite | Structured version Visualization version GIF version |
Description: A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of [Suppes] p. 151. The Axiom of Infinity is used for the forward implication. (Contributed by FL, 16-Apr-2011.) |
Ref | Expression |
---|---|
isfinite | ⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺ ω) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omex 8818 | . 2 ⊢ ω ∈ V | |
2 | isfiniteg 8490 | . 2 ⊢ (ω ∈ V → (𝐴 ∈ Fin ↔ 𝐴 ≺ ω)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺ ω) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∈ wcel 2166 Vcvv 3415 class class class wbr 4874 ωcom 7327 ≺ csdm 8222 Fincfn 8223 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210 ax-inf2 8816 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-ral 3123 df-rex 3124 df-reu 3125 df-rab 3127 df-v 3417 df-sbc 3664 df-csb 3759 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-pss 3815 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4660 df-int 4699 df-iun 4743 df-br 4875 df-opab 4937 df-mpt 4954 df-tr 4977 df-id 5251 df-eprel 5256 df-po 5264 df-so 5265 df-fr 5302 df-we 5304 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-pred 5921 df-ord 5967 df-on 5968 df-lim 5969 df-suc 5970 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-f1 6129 df-fo 6130 df-f1o 6131 df-fv 6132 df-om 7328 df-wrecs 7673 df-recs 7735 df-rdg 7773 df-er 8010 df-en 8224 df-dom 8225 df-sdom 8226 df-fin 8227 |
This theorem is referenced by: fict 8828 infxpenlem 9150 pwsdompw 9342 cflim2 9401 axcc4dom 9579 domtriom 9581 fin41 9582 dominf 9583 infinf 9704 unirnfdomd 9705 dominfac 9711 cfpwsdom 9722 canthp1lem2 9791 pwfseqlem3 9798 pwfseqlem4a 9799 pwfseqlem4 9800 gchpwdom 9808 gchaleph 9809 gchhar 9817 omina 9829 gchina 9837 tskpr 9908 rexpen 15332 odinf 18332 fctop2 21181 dis1stc 21674 ovolfi 23661 iunmbl2 23724 dyadmbl 23767 f1ocnt 30107 sibfof 30948 mblfinlem1 33991 ovoliunnfl 33996 heiborlem3 34155 ctbnfien 38227 pellex 38244 numinfctb 38517 saluncl 41329 meadjun 41471 meaiunlelem 41477 omeunle 41525 |
Copyright terms: Public domain | W3C validator |