![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isfi | Structured version Visualization version GIF version |
Description: Express "𝐴 is finite." Definition 10.29 of [TakeutiZaring] p. 91 (whose "Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008.) |
Ref | Expression |
---|---|
isfi | ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fin 8310 | . . 3 ⊢ Fin = {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 ≈ 𝑥} | |
2 | 1 | eleq2i 2858 | . 2 ⊢ (𝐴 ∈ Fin ↔ 𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 ≈ 𝑥}) |
3 | relen 8311 | . . . . 5 ⊢ Rel ≈ | |
4 | 3 | brrelex1i 5458 | . . . 4 ⊢ (𝐴 ≈ 𝑥 → 𝐴 ∈ V) |
5 | 4 | rexlimivw 3228 | . . 3 ⊢ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 → 𝐴 ∈ V) |
6 | breq1 4932 | . . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ≈ 𝑥 ↔ 𝐴 ≈ 𝑥)) | |
7 | 6 | rexbidv 3243 | . . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦 ≈ 𝑥 ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)) |
8 | 5, 7 | elab3 3590 | . 2 ⊢ (𝐴 ∈ {𝑦 ∣ ∃𝑥 ∈ ω 𝑦 ≈ 𝑥} ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
9 | 2, 8 | bitri 267 | 1 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1507 ∈ wcel 2050 {cab 2759 ∃wrex 3090 Vcvv 3416 class class class wbr 4929 ωcom 7396 ≈ cen 8303 Fincfn 8306 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2751 ax-sep 5060 ax-nul 5067 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3418 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-nul 4180 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-br 4930 df-opab 4992 df-xp 5413 df-rel 5414 df-en 8307 df-fin 8310 |
This theorem is referenced by: snfi 8391 php3 8499 onfin 8504 ominf 8525 isinf 8526 enfi 8529 ssnnfi 8532 ssfi 8533 dif1en 8546 findcard 8552 findcard2 8553 findcard3 8556 nnsdomg 8572 isfiniteg 8573 unfi 8580 fiint 8590 pwfi 8614 finnum 9171 ficardom 9184 dif1card 9230 infpwfien 9282 ficard 9785 hashkf 13507 finminlem 33184 domalom 34123 |
Copyright terms: Public domain | W3C validator |