Description: Express " A 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 | ||
|---|---|---|---|
| Assertion | isfi | ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-fin | ⊢ Fin = { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 } | |
| 2 | 1 | eleq2i | ⊢ ( 𝐴 ∈ Fin ↔ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 } ) |
| 3 | relen | ⊢ Rel ≈ | |
| 4 | 3 | brrelex1i | ⊢ ( 𝐴 ≈ 𝑥 → 𝐴 ∈ V ) |
| 5 | 4 | rexlimivw | ⊢ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → 𝐴 ∈ V ) |
| 6 | breq1 | ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ≈ 𝑥 ↔ 𝐴 ≈ 𝑥 ) ) | |
| 7 | 6 | rexbidv | ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ) ) |
| 8 | 5 7 | elab3 | ⊢ ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 } ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ) |
| 9 | 2 8 | bitri | ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ) |