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	$$⊢\underset{\dot{}}{+}=\left(a\in \mathrm{V},b\in \mathrm{V}⟼a\cup \left\{⟨x,y⟩|\left(x\in \left(\left(\mathrm{dom}a{+}_{𝑜}\mathrm{dom}b\right)\setminus \mathrm{dom}a\right)\wedge \exists z\in \mathrm{dom}b\left(x=\mathrm{dom}a{+}_{𝑜}z\wedge y=b\left(z\right)\right)\right)\right\}\right)$$
Assertion	tfsconcatrnss12	$$⊢\left(\left(AFnC\wedge BFnD\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\to \left(\mathrm{ran}A\subseteq \mathrm{ran}\left(A\underset{\dot{}}{+}B\right)\wedge \mathrm{ran}B\subseteq \mathrm{ran}\left(A\underset{\dot{}}{+}B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tfsconcat.op	$$⊢\underset{\dot{}}{+}=\left(a\in \mathrm{V},b\in \mathrm{V}⟼a\cup \left\{⟨x,y⟩|\left(x\in \left(\left(\mathrm{dom}a{+}_{𝑜}\mathrm{dom}b\right)\setminus \mathrm{dom}a\right)\wedge \exists z\in \mathrm{dom}b\left(x=\mathrm{dom}a{+}_{𝑜}z\wedge y=b\left(z\right)\right)\right)\right\}\right)$$
2	1	tfsconcatrn	$$⊢\left(\left(AFnC\wedge BFnD\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\to \mathrm{ran}\left(A\underset{\dot{}}{+}B\right)=\mathrm{ran}A\cup \mathrm{ran}B$$
3		ssun1	$$⊢\mathrm{ran}A\subseteq \mathrm{ran}A\cup \mathrm{ran}B$$
4		id	$$⊢\mathrm{ran}\left(A\underset{\dot{}}{+}B\right)=\mathrm{ran}A\cup \mathrm{ran}B\to \mathrm{ran}\left(A\underset{\dot{}}{+}B\right)=\mathrm{ran}A\cup \mathrm{ran}B$$
5	3 4	sseqtrrid	$$⊢\mathrm{ran}\left(A\underset{\dot{}}{+}B\right)=\mathrm{ran}A\cup \mathrm{ran}B\to \mathrm{ran}A\subseteq \mathrm{ran}\left(A\underset{\dot{}}{+}B\right)$$
6		ssun2	$$⊢\mathrm{ran}B\subseteq \mathrm{ran}A\cup \mathrm{ran}B$$
7	6 4	sseqtrrid	$$⊢\mathrm{ran}\left(A\underset{\dot{}}{+}B\right)=\mathrm{ran}A\cup \mathrm{ran}B\to \mathrm{ran}B\subseteq \mathrm{ran}\left(A\underset{\dot{}}{+}B\right)$$
8	5 7	jca	$$⊢\mathrm{ran}\left(A\underset{\dot{}}{+}B\right)=\mathrm{ran}A\cup \mathrm{ran}B\to \left(\mathrm{ran}A\subseteq \mathrm{ran}\left(A\underset{\dot{}}{+}B\right)\wedge \mathrm{ran}B\subseteq \mathrm{ran}\left(A\underset{\dot{}}{+}B\right)\right)$$
9	2 8	syl	$$⊢\left(\left(AFnC\wedge BFnD\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\to \left(\mathrm{ran}A\subseteq \mathrm{ran}\left(A\underset{\dot{}}{+}B\right)\wedge \mathrm{ran}B\subseteq \mathrm{ran}\left(A\underset{\dot{}}{+}B\right)\right)$$