Metamath Proof Explorer

Theorem tfsconcatfo

Description: The concatenation of two transfinite series is onto the union of the ranges. (Contributed by RP, 24-Feb-2025)

Ref Expression
Hypothesis tfsconcat.op ⊢ + ˙ = a ∈ V , b ∈ V ⟼ a ∪ x y | x ∈ dom ⁡ a + 𝑜 dom ⁡ b ∖ dom ⁡ a ∧ ∃ z ∈ dom ⁡ b x = dom ⁡ a + 𝑜 z ∧ y = b ⁡ z
Assertion tfsconcatfo ⊢ A Fn C ∧ B Fn D ∧ C ∈ On ∧ D ∈ On → A + ˙ B : C + 𝑜 D ⟶ onto ran ⁡ A ∪ ran ⁡ B

Proof

Step Hyp Ref Expression
1 tfsconcat.op ⊢ + ˙ = a ∈ V , b ∈ V ⟼ a ∪ x y | x ∈ dom ⁡ a + 𝑜 dom ⁡ b ∖ dom ⁡ a ∧ ∃ z ∈ dom ⁡ b x = dom ⁡ a + 𝑜 z ∧ y = b ⁡ z
2 1 tfsconcatfn ⊢ A Fn C ∧ B Fn D ∧ C ∈ On ∧ D ∈ On → A + ˙ B Fn C + 𝑜 D
3 1 tfsconcatrn ⊢ A Fn C ∧ B Fn D ∧ C ∈ On ∧ D ∈ On → ran ⁡ A + ˙ B = ran ⁡ A ∪ ran ⁡ B
4 df-fo ⊢ A + ˙ B : C + 𝑜 D ⟶ onto ran ⁡ A ∪ ran ⁡ B ↔ A + ˙ B Fn C + 𝑜 D ∧ ran ⁡ A + ˙ B = ran ⁡ A ∪ ran ⁡ B
5 2 3 4 sylanbrc ⊢ A Fn C ∧ B Fn D ∧ C ∈ On ∧ D ∈ On → A + ˙ B : C + 𝑜 D ⟶ onto ran ⁡ A ∪ ran ⁡ B