tfsconcat0i

Description: The concatentation with the empty series leaves the series unchanged. (Contributed by RP, 28-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	tfsconcat0i	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A = \emptyset \to A \underset{˙}{+} B = B)$

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		simpr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land A = \emptyset) \to A = \emptyset$
3		fnrel	$⊢ A Fn C \to Rel A$
4		reldm0	$⊢ Rel A \to (A = \emptyset \leftrightarrow dom A = \emptyset)$
5	3 4	syl	$⊢ A Fn C \to (A = \emptyset \leftrightarrow dom A = \emptyset)$
6		fndm	$⊢ A Fn C \to dom A = C$
7	6	eqeq1d	$⊢ A Fn C \to (dom A = \emptyset \leftrightarrow C = \emptyset)$
8	5 7	bitrd	$⊢ A Fn C \to (A = \emptyset \leftrightarrow C = \emptyset)$
9	8	ad2antrr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A = \emptyset \leftrightarrow C = \emptyset)$
10		simpr	$⊢ (A Fn C \land B Fn D) \to B Fn D$
11		simpr	$⊢ (C \in On \land D \in On) \to D \in On$
12	10 11	anim12i	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (B Fn D \land D \in On)$
13	12	anim1i	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land C = \emptyset) \to ((B Fn D \land D \in On) \land C = \emptyset)$
14	9 13	sylbida	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land A = \emptyset) \to ((B Fn D \land D \in On) \land C = \emptyset)$
15		oveq1	$⊢ C = \emptyset \to C +_{𝑜} D = \emptyset +_{𝑜} D$
16		id	$⊢ C = \emptyset \to C = \emptyset$
17	15 16	difeq12d	$⊢ C = \emptyset \to (C +_{𝑜} D) ∖ C = (\emptyset +_{𝑜} D) ∖ \emptyset$
18		dif0	$⊢ (\emptyset +_{𝑜} D) ∖ \emptyset = \emptyset +_{𝑜} D$
19	17 18	eqtrdi	$⊢ C = \emptyset \to (C +_{𝑜} D) ∖ C = \emptyset +_{𝑜} D$
20	19	eleq2d	$⊢ C = \emptyset \to (x \in ((C +_{𝑜} D) ∖ C) \leftrightarrow x \in (\emptyset +_{𝑜} D))$
21		oveq1	$⊢ C = \emptyset \to C +_{𝑜} z = \emptyset +_{𝑜} z$
22	21	eqeq2d	$⊢ C = \emptyset \to (x = C +_{𝑜} z \leftrightarrow x = \emptyset +_{𝑜} z)$
23	22	anbi1d	$⊢ C = \emptyset \to ((x = C +_{𝑜} z \land y = B (z)) \leftrightarrow (x = \emptyset +_{𝑜} z \land y = B (z)))$
24	23	rexbidv	$⊢ C = \emptyset \to (\exists z \in D (x = C +_{𝑜} z \land y = B (z)) \leftrightarrow \exists z \in D (x = \emptyset +_{𝑜} z \land y = B (z)))$
25	20 24	anbi12d	$⊢ C = \emptyset \to ((x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z))) \leftrightarrow (x \in (\emptyset +_{𝑜} D) \land \exists z \in D (x = \emptyset +_{𝑜} z \land y = B (z))))$
26		oa0r	$⊢ D \in On \to \emptyset +_{𝑜} D = D$
27	26	eleq2d	$⊢ D \in On \to (x \in (\emptyset +_{𝑜} D) \leftrightarrow x \in D)$
28		onelon	$⊢ (D \in On \land z \in D) \to z \in On$
29		oa0r	$⊢ z \in On \to \emptyset +_{𝑜} z = z$
30	29	eqeq2d	$⊢ z \in On \to (x = \emptyset +_{𝑜} z \leftrightarrow x = z)$
31	30	anbi1d	$⊢ z \in On \to ((x = \emptyset +_{𝑜} z \land y = B (z)) \leftrightarrow (x = z \land y = B (z)))$
32	28 31	syl	$⊢ (D \in On \land z \in D) \to ((x = \emptyset +_{𝑜} z \land y = B (z)) \leftrightarrow (x = z \land y = B (z)))$
33	32	rexbidva	$⊢ D \in On \to (\exists z \in D (x = \emptyset +_{𝑜} z \land y = B (z)) \leftrightarrow \exists z \in D (x = z \land y = B (z)))$
34	27 33	anbi12d	$⊢ D \in On \to ((x \in (\emptyset +_{𝑜} D) \land \exists z \in D (x = \emptyset +_{𝑜} z \land y = B (z))) \leftrightarrow (x \in D \land \exists z \in D (x = z \land y = B (z))))$
35		df-rex	$⊢ \exists z \in D (x = z \land y = B (z)) \leftrightarrow \exists z (z \in D \land (x = z \land y = B (z)))$
36		an12	$⊢ (z \in D \land (x = z \land y = B (z))) \leftrightarrow (x = z \land (z \in D \land y = B (z)))$
37		eqcom	$⊢ x = z \leftrightarrow z = x$
38	37	anbi1i	$⊢ (x = z \land (z \in D \land y = B (z))) \leftrightarrow (z = x \land (z \in D \land y = B (z)))$
39	36 38	bitri	$⊢ (z \in D \land (x = z \land y = B (z))) \leftrightarrow (z = x \land (z \in D \land y = B (z)))$
40	39	exbii	$⊢ \exists z (z \in D \land (x = z \land y = B (z))) \leftrightarrow \exists z (z = x \land (z \in D \land y = B (z)))$
41		eleq1w	$⊢ z = x \to (z \in D \leftrightarrow x \in D)$
42		fveq2	$⊢ z = x \to B (z) = B (x)$
43	42	eqeq2d	$⊢ z = x \to (y = B (z) \leftrightarrow y = B (x))$
44	41 43	anbi12d	$⊢ z = x \to ((z \in D \land y = B (z)) \leftrightarrow (x \in D \land y = B (x)))$
45	44	equsexvw	$⊢ \exists z (z = x \land (z \in D \land y = B (z))) \leftrightarrow (x \in D \land y = B (x))$
46	35 40 45	3bitri	$⊢ \exists z \in D (x = z \land y = B (z)) \leftrightarrow (x \in D \land y = B (x))$
47	46	baib	$⊢ x \in D \to (\exists z \in D (x = z \land y = B (z)) \leftrightarrow y = B (x))$
48	47	adantl	$⊢ (B Fn D \land x \in D) \to (\exists z \in D (x = z \land y = B (z)) \leftrightarrow y = B (x))$
49		eqcom	$⊢ y = B (x) \leftrightarrow B (x) = y$
50	48 49	bitrdi	$⊢ (B Fn D \land x \in D) \to (\exists z \in D (x = z \land y = B (z)) \leftrightarrow B (x) = y)$
51		fnbrfvb	$⊢ (B Fn D \land x \in D) \to (B (x) = y \leftrightarrow x B y)$
52	50 51	bitrd	$⊢ (B Fn D \land x \in D) \to (\exists z \in D (x = z \land y = B (z)) \leftrightarrow x B y)$
53	52	pm5.32da	$⊢ B Fn D \to ((x \in D \land \exists z \in D (x = z \land y = B (z))) \leftrightarrow (x \in D \land x B y))$
54		fnbr	$⊢ (B Fn D \land x B y) \to x \in D$
55	54	ex	$⊢ B Fn D \to (x B y \to x \in D)$
56	55	pm4.71rd	$⊢ B Fn D \to (x B y \leftrightarrow (x \in D \land x B y))$
57		df-br	$⊢ x B y \leftrightarrow ⟨x, y⟩ \in B$
58	56 57	bitr3di	$⊢ B Fn D \to ((x \in D \land x B y) \leftrightarrow ⟨x, y⟩ \in B)$
59	53 58	bitrd	$⊢ B Fn D \to ((x \in D \land \exists z \in D (x = z \land y = B (z))) \leftrightarrow ⟨x, y⟩ \in B)$
60	34 59	sylan9bbr	$⊢ (B Fn D \land D \in On) \to ((x \in (\emptyset +_{𝑜} D) \land \exists z \in D (x = \emptyset +_{𝑜} z \land y = B (z))) \leftrightarrow ⟨x, y⟩ \in B)$
61	25 60	sylan9bbr	$⊢ ((B Fn D \land D \in On) \land C = \emptyset) \to ((x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z))) \leftrightarrow ⟨x, y⟩ \in B)$
62	61	opabbidv	$⊢ ((B Fn D \land D \in On) \land C = \emptyset) \to \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = \{⟨x, y⟩ \| ⟨x, y⟩ \in B\}$
63	14 62	syl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land A = \emptyset) \to \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = \{⟨x, y⟩ \| ⟨x, y⟩ \in B\}$
64		fnrel	$⊢ B Fn D \to Rel B$
65		opabid2	$⊢ Rel B \to \{⟨x, y⟩ \| ⟨x, y⟩ \in B\} = B$
66	64 65	syl	$⊢ B Fn D \to \{⟨x, y⟩ \| ⟨x, y⟩ \in B\} = B$
67	66	adantl	$⊢ (A Fn C \land B Fn D) \to \{⟨x, y⟩ \| ⟨x, y⟩ \in B\} = B$
68	67	ad2antrr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land A = \emptyset) \to \{⟨x, y⟩ \| ⟨x, y⟩ \in B\} = B$
69	63 68	eqtrd	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land A = \emptyset) \to \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = B$
70	2 69	uneq12d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land A = \emptyset) \to A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = \emptyset \cup B$
71		0un	$⊢ \emptyset \cup B = B$
72	70 71	eqtrdi	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land A = \emptyset) \to A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = B$
73	72	ex	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A = \emptyset \to A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = B)$
74	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)))\}$
75	74	eqeq1d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A \underset{˙}{+} B = B \leftrightarrow A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = B)$
76	73 75	sylibrd	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A = \emptyset \to A \underset{˙}{+} B = B)$

Metamath Proof Explorer

Theorem tfsconcat0i

Proof