Description: Definition of a VII-finite set. (Contributed by Stefan O'Rear, 16-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | isfin7 | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinVII ↔ ¬ ∃ 𝑦 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑦 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 | ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝑦 ↔ 𝐴 ≈ 𝑦 ) ) | |
2 | 1 | rexbidv | ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∈ ( On ∖ ω ) 𝑥 ≈ 𝑦 ↔ ∃ 𝑦 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑦 ) ) |
3 | 2 | notbid | ⊢ ( 𝑥 = 𝐴 → ( ¬ ∃ 𝑦 ∈ ( On ∖ ω ) 𝑥 ≈ 𝑦 ↔ ¬ ∃ 𝑦 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑦 ) ) |
4 | df-fin7 | ⊢ FinVII = { 𝑥 ∣ ¬ ∃ 𝑦 ∈ ( On ∖ ω ) 𝑥 ≈ 𝑦 } | |
5 | 3 4 | elab2g | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinVII ↔ ¬ ∃ 𝑦 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑦 ) ) |