Metamath Proof Explorer

Theorem r1om

Description: The set of hereditarily finite sets is countable. See ackbij2 for an explicit bijection that works without Infinity. See also r1omALT . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Assertion r1om ⊢ R1 ⁡ ω ≈ ω

Proof

Step Hyp Ref Expression
1 omex ⊢ ω ∈ V
2 limom ⊢ Lim ⁡ ω
3 r1lim ⊢ ω ∈ V ∧ Lim ⁡ ω → R1 ⁡ ω = ⋃ a ∈ ω R1 ⁡ a
4 1 2 3 mp2an ⊢ R1 ⁡ ω = ⋃ a ∈ ω R1 ⁡ a
5 r1fnon ⊢ R1 Fn On
6 fnfun ⊢ R1 Fn On → Fun ⁡ R1
7 funiunfv ⊢ Fun ⁡ R1 → ⋃ a ∈ ω R1 ⁡ a = ⋃ R1 ω
8 5 6 7 mp2b ⊢ ⋃ a ∈ ω R1 ⁡ a = ⋃ R1 ω
9 4 8 eqtri ⊢ R1 ⁡ ω = ⋃ R1 ω
10 iuneq1 ⊢ e = a → ⋃ f ∈ e f × 𝒫 f = ⋃ f ∈ a f × 𝒫 f
11 sneq ⊢ f = b → f = b
12 pweq ⊢ f = b → 𝒫 f = 𝒫 b
13 11 12 xpeq12d ⊢ f = b → f × 𝒫 f = b × 𝒫 b
14 13 cbviunv ⊢ ⋃ f ∈ a f × 𝒫 f = ⋃ b ∈ a b × 𝒫 b
15 10 14 eqtrdi ⊢ e = a → ⋃ f ∈ e f × 𝒫 f = ⋃ b ∈ a b × 𝒫 b
16 15 fveq2d ⊢ e = a → card ⁡ ⋃ f ∈ e f × 𝒫 f = card ⁡ ⋃ b ∈ a b × 𝒫 b
17 16 cbvmptv ⊢ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f = a ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ b ∈ a b × 𝒫 b
18 dmeq ⊢ c = a → dom ⁡ c = dom ⁡ a
19 18 pweqd ⊢ c = a → 𝒫 dom ⁡ c = 𝒫 dom ⁡ a
20 imaeq1 ⊢ c = a → c d = a d
21 20 fveq2d ⊢ c = a → e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ c d = e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ a d
22 19 21 mpteq12dv ⊢ c = a → d ∈ 𝒫 dom ⁡ c ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ c d = d ∈ 𝒫 dom ⁡ a ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ a d
23 imaeq2 ⊢ d = b → a d = a b
24 23 fveq2d ⊢ d = b → e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ a d = e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ a b
25 24 cbvmptv ⊢ d ∈ 𝒫 dom ⁡ a ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ a d = b ∈ 𝒫 dom ⁡ a ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ a b
26 22 25 eqtrdi ⊢ c = a → d ∈ 𝒫 dom ⁡ c ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ c d = b ∈ 𝒫 dom ⁡ a ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ a b
27 26 cbvmptv ⊢ c ∈ V ⟼ d ∈ 𝒫 dom ⁡ c ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ c d = a ∈ V ⟼ b ∈ 𝒫 dom ⁡ a ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ a b
28 eqid ⊢ ⋃ rec ⁡ c ∈ V ⟼ d ∈ 𝒫 dom ⁡ c ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ c d ∅ ω = ⋃ rec ⁡ c ∈ V ⟼ d ∈ 𝒫 dom ⁡ c ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ c d ∅ ω
29 17 27 28 ackbij2 ⊢ ⋃ rec ⁡ c ∈ V ⟼ d ∈ 𝒫 dom ⁡ c ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ c d ∅ ω : ⋃ R1 ω ⟶ 1-1 onto ω
30 fvex ⊢ R1 ⁡ ω ∈ V
31 9 30 eqeltrri ⊢ ⋃ R1 ω ∈ V
32 31 f1oen ⊢ ⋃ rec ⁡ c ∈ V ⟼ d ∈ 𝒫 dom ⁡ c ⟼ e ∈ 𝒫 ω ∩ Fin ⟼ card ⁡ ⋃ f ∈ e f × 𝒫 f ⁡ c d ∅ ω : ⋃ R1 ω ⟶ 1-1 onto ω → ⋃ R1 ω ≈ ω
33 29 32 ax-mp ⊢ ⋃ R1 ω ≈ ω
34 9 33 eqbrtri ⊢ R1 ⁡ ω ≈ ω