Description: Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | elhf | ⊢ ( 𝐴 ∈ Hf ↔ ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-hf | ⊢ Hf = ∪ ( 𝑅1 “ ω ) | |
2 | 1 | eleq2i | ⊢ ( 𝐴 ∈ Hf ↔ 𝐴 ∈ ∪ ( 𝑅1 “ ω ) ) |
3 | r111 | ⊢ 𝑅1 : On –1-1→ V | |
4 | f1fun | ⊢ ( 𝑅1 : On –1-1→ V → Fun 𝑅1 ) | |
5 | eluniima | ⊢ ( Fun 𝑅1 → ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) ↔ ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) ) | |
6 | 3 4 5 | mp2b | ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) ↔ ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) |
7 | 2 6 | bitri | ⊢ ( 𝐴 ∈ Hf ↔ ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) |