Metamath Proof Explorer

Theorem tfsconcatrnss

Description: The concatenation of transfinite sequences yields elements from a class iff both sequences yield elements from that class. (Contributed by RP, 2-Mar-2025)

		Ref	Expression
	Hypothesis	tfsconcat.op	$⊢ \underset{˙}{+} = (a \in V, b \in V ⟼ a \cup \{⟨x, y⟩ \| (x \in ((dom a +_{𝑜} dom b) ∖ dom a) \land \exists z \in dom b (x = dom a +_{𝑜} z \land y = b (z)))\})$
	Assertion	tfsconcatrnss	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (ran (A \underset{˙}{+} B) \subseteq X \leftrightarrow (ran A \subseteq X \land ran B \subseteq X))$

Proof

Step	Hyp	Ref	Expression
1		tfsconcat.op	$⊢ \underset{˙}{+} = (a \in V, b \in V ⟼ a \cup \{⟨x, y⟩ \| (x \in ((dom a +_{𝑜} dom b) ∖ dom a) \land \exists z \in dom b (x = dom a +_{𝑜} z \land y = b (z)))\})$
2	1	tfsconcatrn	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ran (A \underset{˙}{+} B) = ran A \cup ran B$
3	2	sseq1d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (ran (A \underset{˙}{+} B) \subseteq X \leftrightarrow ran A \cup ran B \subseteq X)$
4		unss	$⊢ (ran A \subseteq X \land ran B \subseteq X) \leftrightarrow ran A \cup ran B \subseteq X$
5	3 4	bitr4di	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (ran (A \underset{˙}{+} B) \subseteq X \leftrightarrow (ran A \subseteq X \land ran B \subseteq X))$