tfsconcatfn

Description: The concatenation of two transfinite series is a transfinite series. (Contributed by RP, 22-Feb-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	tfsconcatfn	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A \underset{˙}{+} B) Fn (C +_{𝑜} D)$

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		simpll	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to A Fn C$
3		simplrl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to C \in On$
4		simplrr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to D \in On$
5		simpr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to x \in ((C +_{𝑜} D) ∖ C)$
6		tfsconcatlem	$⊢ (C \in On \land D \in On \land x \in ((C +_{𝑜} D) ∖ C)) \to \exists! y \exists z \in D (x = C +_{𝑜} z \land y = B (z))$
7	3 4 5 6	syl3anc	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to \exists! y \exists z \in D (x = C +_{𝑜} z \land y = B (z))$
8	7	ralrimiva	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to \forall x \in ((C +_{𝑜} D) ∖ C) \exists! y \exists z \in D (x = C +_{𝑜} z \land y = B (z))$
9		eqid	$⊢ \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
10	9	fnopabg	$⊢ \forall x \in ((C +_{𝑜} D) ∖ C) \exists! y \exists z \in D (x = C +_{𝑜} z \land y = B (z)) \leftrightarrow \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} Fn ((C +_{𝑜} D) ∖ C)$
11	8 10	sylib	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} Fn ((C +_{𝑜} D) ∖ C)$
12		disjdif	$⊢ C \cap ((C +_{𝑜} D) ∖ C) = \emptyset$
13	12	a1i	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to C \cap ((C +_{𝑜} D) ∖ C) = \emptyset$
14	2 11 13	fnund	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}) Fn (C \cup ((C +_{𝑜} D) ∖ C))$
15	1	tfsconcatun	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to A \underset{˙}{+} B = A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
16		oaword1	$⊢ (C \in On \land D \in On) \to C \subseteq C +_{𝑜} D$
17		undif	$⊢ C \subseteq C +_{𝑜} D \leftrightarrow C \cup ((C +_{𝑜} D) ∖ C) = C +_{𝑜} D$
18	16 17	sylib	$⊢ (C \in On \land D \in On) \to C \cup ((C +_{𝑜} D) ∖ C) = C +_{𝑜} D$
19	18	eqcomd	$⊢ (C \in On \land D \in On) \to C +_{𝑜} D = C \cup ((C +_{𝑜} D) ∖ C)$
20	19	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to C +_{𝑜} D = C \cup ((C +_{𝑜} D) ∖ C)$
21	15 20	fneq12d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ((A \underset{˙}{+} B) Fn (C +_{𝑜} D) \leftrightarrow (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}) Fn (C \cup ((C +_{𝑜} D) ∖ C)))$
22	14 21	mpbird	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A \underset{˙}{+} B) Fn (C +_{𝑜} D)$

Metamath Proof Explorer

Theorem tfsconcatfn

Proof