Theorem tfsconcatrnss12

Description: The range of the concatenation of transfinite sequences is a superset of the ranges of both sequences. Theorem 3 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025)

	Ref	Expression
Hypothesis	tfsconcat.op	⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
Assertion	tfsconcatrnss12	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ran 𝐴 ⊆ ran ( 𝐴 + 𝐵 ) ∧ ran 𝐵 ⊆ ran ( 𝐴 + 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tfsconcat.op	⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
2	1	tfsconcatrn	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) )
3		ssun1	⊢ ran 𝐴 ⊆ ( ran 𝐴 ∪ ran 𝐵 )
4		id	⊢ ( ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) → ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) )
5	3 4	sseqtrrid	⊢ ( ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) → ran 𝐴 ⊆ ran ( 𝐴 + 𝐵 ) )
6		ssun2	⊢ ran 𝐵 ⊆ ( ran 𝐴 ∪ ran 𝐵 )
7	6 4	sseqtrrid	⊢ ( ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) → ran 𝐵 ⊆ ran ( 𝐴 + 𝐵 ) )
8	5 7	jca	⊢ ( ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) → ( ran 𝐴 ⊆ ran ( 𝐴 + 𝐵 ) ∧ ran 𝐵 ⊆ ran ( 𝐴 + 𝐵 ) ) )
9	2 8	syl	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ran 𝐴 ⊆ ran ( 𝐴 + 𝐵 ) ∧ ran 𝐵 ⊆ ran ( 𝐴 + 𝐵 ) ) )