tfsconcatun

Description: The concatenation of two transfinite series is a union of functions. (Contributed by RP, 23-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	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)))\}$

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	a1i	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to \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)))\})$
3		simprl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to a = A$
4		dmeq	$⊢ a = A \to dom a = dom A$
5	4	adantr	$⊢ (a = A \land b = B) \to dom a = dom A$
6		fndm	$⊢ A Fn C \to dom A = C$
7	6	adantr	$⊢ (A Fn C \land B Fn D) \to dom A = C$
8	7	adantr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to dom A = C$
9	5 8	sylan9eqr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to dom a = C$
10		dmeq	$⊢ b = B \to dom b = dom B$
11	10	adantl	$⊢ (a = A \land b = B) \to dom b = dom B$
12		fndm	$⊢ B Fn D \to dom B = D$
13	12	adantl	$⊢ (A Fn C \land B Fn D) \to dom B = D$
14	13	adantr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to dom B = D$
15	11 14	sylan9eqr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to dom b = D$
16	9 15	oveq12d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to dom a +_{𝑜} dom b = C +_{𝑜} D$
17	16 9	difeq12d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to (dom a +_{𝑜} dom b) ∖ dom a = (C +_{𝑜} D) ∖ C$
18	17	eleq2d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to (x \in ((dom a +_{𝑜} dom b) ∖ dom a) \leftrightarrow x \in ((C +_{𝑜} D) ∖ C))$
19	9	oveq1d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to dom a +_{𝑜} z = C +_{𝑜} z$
20	19	eqeq2d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to (x = dom a +_{𝑜} z \leftrightarrow x = C +_{𝑜} z)$
21		fveq1	$⊢ b = B \to b (z) = B (z)$
22	21	eqeq2d	$⊢ b = B \to (y = b (z) \leftrightarrow y = B (z))$
23	22	adantl	$⊢ (a = A \land b = B) \to (y = b (z) \leftrightarrow y = B (z))$
24	23	adantl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to (y = b (z) \leftrightarrow y = B (z))$
25	20 24	anbi12d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to ((x = dom a +_{𝑜} z \land y = b (z)) \leftrightarrow (x = C +_{𝑜} z \land y = B (z)))$
26	15 25	rexeqbidv	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to (\exists z \in dom b (x = dom a +_{𝑜} z \land y = b (z)) \leftrightarrow \exists z \in D (x = C +_{𝑜} z \land y = B (z)))$
27	18 26	anbi12d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to ((x \in ((dom a +_{𝑜} dom b) ∖ dom a) \land \exists z \in dom b (x = dom a +_{𝑜} z \land y = b (z))) \leftrightarrow (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z))))$
28	27	opabbidv	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to \{⟨x, y⟩ \| (x \in ((dom a +_{𝑜} dom b) ∖ dom a) \land \exists z \in dom b (x = dom a +_{𝑜} z \land y = b (z)))\} = \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
29	3 28	uneq12d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land (a = A \land b = B)) \to 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)))\} = A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
30		fnex	$⊢ (A Fn C \land C \in On) \to A \in V$
31	30	ad2ant2r	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to A \in V$
32		fnex	$⊢ (B Fn D \land D \in On) \to B \in V$
33	32	ad2ant2l	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to B \in V$
34		oacl	$⊢ (C \in On \land D \in On) \to C +_{𝑜} D \in On$
35	34	difexd	$⊢ (C \in On \land D \in On) \to (C +_{𝑜} D) ∖ C \in V$
36	35	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (C +_{𝑜} D) ∖ C \in V$
37		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$
38		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$
39		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)$
40		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))$
41	37 38 39 40	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))$
42		euabex	$⊢ \exists! y \exists z \in D (x = C +_{𝑜} z \land y = B (z)) \to \{y \| \exists z \in D (x = C +_{𝑜} z \land y = B (z))\} \in V$
43	41 42	syl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to \{y \| \exists z \in D (x = C +_{𝑜} z \land y = B (z))\} \in V$
44	36 43	opabex3d	$⊢ ((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)))\} \in V$
45	31 44	unexd	$⊢ ((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)))\} \in V$
46	2 29 31 33 45	ovmpod	$⊢ ((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)))\}$

Metamath Proof Explorer

Theorem tfsconcatun

Proof