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	⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
Assertion	tfsconcatfo	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 + 𝐵 ) : ( 𝐶 +o 𝐷 ) –onto→ ( ran 𝐴 ∪ ran 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		tfsconcat.op	⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
2	1	tfsconcatfn	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 + 𝐵 ) Fn ( 𝐶 +o 𝐷 ) )
3	1	tfsconcatrn	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) )
4		df-fo	⊢ ( ( 𝐴 + 𝐵 ) : ( 𝐶 +o 𝐷 ) –onto→ ( ran 𝐴 ∪ ran 𝐵 ) ↔ ( ( 𝐴 + 𝐵 ) Fn ( 𝐶 +o 𝐷 ) ∧ ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) ) )
5	2 3 4	sylanbrc	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 + 𝐵 ) : ( 𝐶 +o 𝐷 ) –onto→ ( ran 𝐴 ∪ ran 𝐵 ) )