Theorem tfsconcatrnsson

Description: The concatenation of transfinite sequences yields ordinals iff both sequences yield ordinals. Theorem 4 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	tfsconcatrnsson	$$⊢\left(\left(AFnC\wedge BFnD\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\to \left(\mathrm{ran}\left(A\underset{\dot{}}{+}B\right)\subseteq \mathrm{On}\leftrightarrow \left(\mathrm{ran}A\subseteq \mathrm{On}\wedge \mathrm{ran}B\subseteq \mathrm{On}\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	tfsconcatrnss	$$⊢\left(\left(AFnC\wedge BFnD\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\to \left(\mathrm{ran}\left(A\underset{\dot{}}{+}B\right)\subseteq \mathrm{On}\leftrightarrow \left(\mathrm{ran}A\subseteq \mathrm{On}\wedge \mathrm{ran}B\subseteq \mathrm{On}\right)\right)$$