tfsconcatfv

Description: The value of the concatenation of two transfinite series. (Contributed by RP, 24-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	tfsconcatfv	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \to (A \underset{˙}{+} B) (X) = if (X \in C, A (X), B ((ι d \in D \| C +_{𝑜} d = 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	tfsconcatfv1	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in C) \to (A \underset{˙}{+} B) (X) = A (X)$
3	2	adantlr	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land X \in C) \to (A \underset{˙}{+} B) (X) = A (X)$
4		simpr	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land X \in C) \to X \in C$
5	4	iftrued	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land X \in C) \to if (X \in C, A (X), B ((ι d \in D \| C +_{𝑜} d = X))) = A (X)$
6	3 5	eqtr4d	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land X \in C) \to (A \underset{˙}{+} B) (X) = if (X \in C, A (X), B ((ι d \in D \| C +_{𝑜} d = X)))$
7		simpr	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to \neg X \in C$
8	7	iffalsed	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to if (X \in C, A (X), B ((ι d \in D \| C +_{𝑜} d = X))) = B ((ι d \in D \| C +_{𝑜} d = X))$
9		simpll	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to ((A Fn C \land B Fn D) \land (C \in On \land D \in On))$
10		onss	$⊢ D \in On \to D \subseteq On$
11	10	adantl	$⊢ (C \in On \land D \in On) \to D \subseteq On$
12	11	ad3antlr	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to D \subseteq On$
13		simpllr	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to (C \in On \land D \in On)$
14		simplrl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \to C \in On$
15		oacl	$⊢ (C \in On \land D \in On) \to C +_{𝑜} D \in On$
16	15	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to C +_{𝑜} D \in On$
17		onelon	$⊢ (C +_{𝑜} D \in On \land X \in (C +_{𝑜} D)) \to X \in On$
18	16 17	sylan	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \to X \in On$
19		ontri1	$⊢ (C \in On \land X \in On) \to (C \subseteq X \leftrightarrow \neg X \in C)$
20	14 18 19	syl2anc	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \to (C \subseteq X \leftrightarrow \neg X \in C)$
21	20	biimpar	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to C \subseteq X$
22		simplr	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to X \in (C +_{𝑜} D)$
23		oawordex2	$⊢ ((C \in On \land D \in On) \land (C \subseteq X \land X \in (C +_{𝑜} D))) \to \exists d \in D C +_{𝑜} d = X$
24	13 21 22 23	syl12anc	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to \exists d \in D C +_{𝑜} d = X$
25	14 18	jca	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \to (C \in On \land X \in On)$
26		oawordeu	$⊢ ((C \in On \land X \in On) \land C \subseteq X) \to \exists! d \in On C +_{𝑜} d = X$
27	25 21 26	syl2an2r	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to \exists! d \in On C +_{𝑜} d = X$
28		reuss	$⊢ (D \subseteq On \land \exists d \in D C +_{𝑜} d = X \land \exists! d \in On C +_{𝑜} d = X) \to \exists! d \in D C +_{𝑜} d = X$
29	12 24 27 28	syl3anc	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to \exists! d \in D C +_{𝑜} d = X$
30		riotacl	$⊢ \exists! d \in D C +_{𝑜} d = X \to (ι d \in D \| C +_{𝑜} d = X) \in D$
31	29 30	syl	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to (ι d \in D \| C +_{𝑜} d = X) \in D$
32	1	tfsconcatfv2	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (ι d \in D \| C +_{𝑜} d = X) \in D) \to (A \underset{˙}{+} B) (C +_{𝑜} (ι d \in D \| C +_{𝑜} d = X)) = B ((ι d \in D \| C +_{𝑜} d = X))$
33	9 31 32	syl2anc	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to (A \underset{˙}{+} B) (C +_{𝑜} (ι d \in D \| C +_{𝑜} d = X)) = B ((ι d \in D \| C +_{𝑜} d = X))$
34		riotasbc	$⊢ \exists! d \in D C +_{𝑜} d = X \to \underset{˙}{[} (ι d \in D \| C +_{𝑜} d = X) / d \underset{˙}{]} C +_{𝑜} d = X$
35	29 34	syl	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to \underset{˙}{[} (ι d \in D \| C +_{𝑜} d = X) / d \underset{˙}{]} C +_{𝑜} d = X$
36		sbceq1g	$⊢ (ι d \in D \| C +_{𝑜} d = X) \in D \to (\underset{˙}{[} (ι d \in D \| C +_{𝑜} d = X) / d \underset{˙}{]} C +_{𝑜} d = X \leftrightarrow ⦋ (ι d \in D \| C +_{𝑜} d = X) / d ⦌ (C +_{𝑜} d) = X)$
37		csbov2g	$⊢ (ι d \in D \| C +_{𝑜} d = X) \in D \to ⦋ (ι d \in D \| C +_{𝑜} d = X) / d ⦌ (C +_{𝑜} d) = C +_{𝑜} ⦋ (ι d \in D \| C +_{𝑜} d = X) / d ⦌ d$
38		csbvarg	$⊢ (ι d \in D \| C +_{𝑜} d = X) \in D \to ⦋ (ι d \in D \| C +_{𝑜} d = X) / d ⦌ d = (ι d \in D \| C +_{𝑜} d = X)$
39	38	oveq2d	$⊢ (ι d \in D \| C +_{𝑜} d = X) \in D \to C +_{𝑜} ⦋ (ι d \in D \| C +_{𝑜} d = X) / d ⦌ d = C +_{𝑜} (ι d \in D \| C +_{𝑜} d = X)$
40	37 39	eqtrd	$⊢ (ι d \in D \| C +_{𝑜} d = X) \in D \to ⦋ (ι d \in D \| C +_{𝑜} d = X) / d ⦌ (C +_{𝑜} d) = C +_{𝑜} (ι d \in D \| C +_{𝑜} d = X)$
41	40	eqeq1d	$⊢ (ι d \in D \| C +_{𝑜} d = X) \in D \to (⦋ (ι d \in D \| C +_{𝑜} d = X) / d ⦌ (C +_{𝑜} d) = X \leftrightarrow C +_{𝑜} (ι d \in D \| C +_{𝑜} d = X) = X)$
42	36 41	bitrd	$⊢ (ι d \in D \| C +_{𝑜} d = X) \in D \to (\underset{˙}{[} (ι d \in D \| C +_{𝑜} d = X) / d \underset{˙}{]} C +_{𝑜} d = X \leftrightarrow C +_{𝑜} (ι d \in D \| C +_{𝑜} d = X) = X)$
43	42	biimpa	$⊢ ((ι d \in D \| C +_{𝑜} d = X) \in D \land \underset{˙}{[} (ι d \in D \| C +_{𝑜} d = X) / d \underset{˙}{]} C +_{𝑜} d = X) \to C +_{𝑜} (ι d \in D \| C +_{𝑜} d = X) = X$
44	31 35 43	syl2anc	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to C +_{𝑜} (ι d \in D \| C +_{𝑜} d = X) = X$
45	44	fveq2d	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to (A \underset{˙}{+} B) (C +_{𝑜} (ι d \in D \| C +_{𝑜} d = X)) = (A \underset{˙}{+} B) (X)$
46	8 33 45	3eqtr2rd	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \land \neg X \in C) \to (A \underset{˙}{+} B) (X) = if (X \in C, A (X), B ((ι d \in D \| C +_{𝑜} d = X)))$
47	6 46	pm2.61dan	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in (C +_{𝑜} D)) \to (A \underset{˙}{+} B) (X) = if (X \in C, A (X), B ((ι d \in D \| C +_{𝑜} d = X)))$

Metamath Proof Explorer

Theorem tfsconcatfv

Proof