tfsconcatb0

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

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		fnrel	$⊢ B Fn D \to Rel B$
3		reldm0	$⊢ Rel B \to (B = \emptyset \leftrightarrow dom B = \emptyset)$
4	2 3	syl	$⊢ B Fn D \to (B = \emptyset \leftrightarrow dom B = \emptyset)$
5		fndm	$⊢ B Fn D \to dom B = D$
6	5	eqeq1d	$⊢ B Fn D \to (dom B = \emptyset \leftrightarrow D = \emptyset)$
7	4 6	bitrd	$⊢ B Fn D \to (B = \emptyset \leftrightarrow D = \emptyset)$
8	7	ad2antlr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (B = \emptyset \leftrightarrow D = \emptyset)$
9		rex0	$⊢ \neg \exists z \in \emptyset (x = C +_{𝑜} z \land y = B (z))$
10		rexeq	$⊢ D = \emptyset \to (\exists z \in D (x = C +_{𝑜} z \land y = B (z)) \leftrightarrow \exists z \in \emptyset (x = C +_{𝑜} z \land y = B (z)))$
11	10	adantl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land D = \emptyset) \to (\exists z \in D (x = C +_{𝑜} z \land y = B (z)) \leftrightarrow \exists z \in \emptyset (x = C +_{𝑜} z \land y = B (z)))$
12	9 11	mtbiri	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land D = \emptyset) \to \neg \exists z \in D (x = C +_{𝑜} z \land y = B (z))$
13	12	intnand	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land D = \emptyset) \to \neg (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))$
14	13	alrimivv	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land D = \emptyset) \to \forall x \forall y \neg (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))$
15		opab0	$⊢ \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = \emptyset \leftrightarrow \forall x \forall y \neg (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))$
16	14 15	sylibr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land D = \emptyset) \to \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = \emptyset$
17		0ss	$⊢ \emptyset \subseteq A$
18	16 17	eqsstrdi	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land D = \emptyset) \to \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \subseteq A$
19	18	ex	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (D = \emptyset \to \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \subseteq A)$
20		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
21		simpl	$⊢ (D \in On \land \neg D = \emptyset) \to D \in On$
22		on0eln0	$⊢ D \in On \to (\emptyset \in D \leftrightarrow D \neq \emptyset)$
23		df-ne	$⊢ D \neq \emptyset \leftrightarrow \neg D = \emptyset$
24	22 23	bitrdi	$⊢ D \in On \to (\emptyset \in D \leftrightarrow \neg D = \emptyset)$
25	24	biimpar	$⊢ (D \in On \land \neg D = \emptyset) \to \emptyset \in D$
26		onsucss	$⊢ D \in On \to (\emptyset \in D \to suc \emptyset \subseteq D)$
27	21 25 26	sylc	$⊢ (D \in On \land \neg D = \emptyset) \to suc \emptyset \subseteq D$
28	20 27	eqsstrid	$⊢ (D \in On \land \neg D = \emptyset) \to 1_{𝑜} \subseteq D$
29	28	ex	$⊢ D \in On \to (\neg D = \emptyset \to 1_{𝑜} \subseteq D)$
30	29	adantl	$⊢ (C \in On \land D \in On) \to (\neg D = \emptyset \to 1_{𝑜} \subseteq D)$
31	30	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (\neg D = \emptyset \to 1_{𝑜} \subseteq D)$
32		simpr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to 1_{𝑜} \subseteq D$
33		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
34	33	a1i	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to \emptyset \in 1_{𝑜}$
35	32 34	sseldd	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to \emptyset \in D$
36		oaord1	$⊢ (C \in On \land D \in On) \to (\emptyset \in D \leftrightarrow C \in (C +_{𝑜} D))$
37	36	ad2antlr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to (\emptyset \in D \leftrightarrow C \in (C +_{𝑜} D))$
38	35 37	mpbid	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to C \in (C +_{𝑜} D)$
39		ssidd	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to C \subseteq C$
40		oacl	$⊢ (C \in On \land D \in On) \to C +_{𝑜} D \in On$
41		eloni	$⊢ C +_{𝑜} D \in On \to Ord (C +_{𝑜} D)$
42	40 41	syl	$⊢ (C \in On \land D \in On) \to Ord (C +_{𝑜} D)$
43		eloni	$⊢ C \in On \to Ord C$
44	43	adantr	$⊢ (C \in On \land D \in On) \to Ord C$
45	42 44	jca	$⊢ (C \in On \land D \in On) \to (Ord (C +_{𝑜} D) \land Ord C)$
46	45	ad2antlr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to (Ord (C +_{𝑜} D) \land Ord C)$
47		ordeldif	$⊢ (Ord (C +_{𝑜} D) \land Ord C) \to (C \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (C \in (C +_{𝑜} D) \land C \subseteq C))$
48	46 47	syl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to (C \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (C \in (C +_{𝑜} D) \land C \subseteq C))$
49	38 39 48	mpbir2and	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to C \in ((C +_{𝑜} D) ∖ C)$
50		simpl	$⊢ (C \in On \land D \in On) \to C \in On$
51	50	ad2antlr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to C \in On$
52		oa0	$⊢ C \in On \to C +_{𝑜} \emptyset = C$
53	51 52	syl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to C +_{𝑜} \emptyset = C$
54	53	eqcomd	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to C = C +_{𝑜} \emptyset$
55		eqidd	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to B (\emptyset) = B (\emptyset)$
56	54 55	jca	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to (C = C +_{𝑜} \emptyset \land B (\emptyset) = B (\emptyset))$
57		oveq2	$⊢ z = \emptyset \to C +_{𝑜} z = C +_{𝑜} \emptyset$
58	57	eqeq2d	$⊢ z = \emptyset \to (C = C +_{𝑜} z \leftrightarrow C = C +_{𝑜} \emptyset)$
59		fveq2	$⊢ z = \emptyset \to B (z) = B (\emptyset)$
60	59	eqeq2d	$⊢ z = \emptyset \to (B (\emptyset) = B (z) \leftrightarrow B (\emptyset) = B (\emptyset))$
61	58 60	anbi12d	$⊢ z = \emptyset \to ((C = C +_{𝑜} z \land B (\emptyset) = B (z)) \leftrightarrow (C = C +_{𝑜} \emptyset \land B (\emptyset) = B (\emptyset)))$
62	61	rspcev	$⊢ (\emptyset \in D \land (C = C +_{𝑜} \emptyset \land B (\emptyset) = B (\emptyset))) \to \exists z \in D (C = C +_{𝑜} z \land B (\emptyset) = B (z))$
63	35 56 62	syl2anc	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to \exists z \in D (C = C +_{𝑜} z \land B (\emptyset) = B (z))$
64		fvexd	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to B (\emptyset) \in V$
65		eleq1	$⊢ x = C \to (x \in ((C +_{𝑜} D) ∖ C) \leftrightarrow C \in ((C +_{𝑜} D) ∖ C))$
66	65	adantr	$⊢ (x = C \land y = B (\emptyset)) \to (x \in ((C +_{𝑜} D) ∖ C) \leftrightarrow C \in ((C +_{𝑜} D) ∖ C))$
67		eqeq1	$⊢ x = C \to (x = C +_{𝑜} z \leftrightarrow C = C +_{𝑜} z)$
68		eqeq1	$⊢ y = B (\emptyset) \to (y = B (z) \leftrightarrow B (\emptyset) = B (z))$
69	67 68	bi2anan9	$⊢ (x = C \land y = B (\emptyset)) \to ((x = C +_{𝑜} z \land y = B (z)) \leftrightarrow (C = C +_{𝑜} z \land B (\emptyset) = B (z)))$
70	69	rexbidv	$⊢ (x = C \land y = B (\emptyset)) \to (\exists z \in D (x = C +_{𝑜} z \land y = B (z)) \leftrightarrow \exists z \in D (C = C +_{𝑜} z \land B (\emptyset) = B (z)))$
71	66 70	anbi12d	$⊢ (x = C \land y = B (\emptyset)) \to ((x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z))) \leftrightarrow (C \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (C = C +_{𝑜} z \land B (\emptyset) = B (z))))$
72	71	opelopabga	$⊢ (C \in On \land B (\emptyset) \in V) \to (⟨C, B (\emptyset)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \leftrightarrow (C \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (C = C +_{𝑜} z \land B (\emptyset) = B (z))))$
73	51 64 72	syl2anc	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to (⟨C, B (\emptyset)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \leftrightarrow (C \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (C = C +_{𝑜} z \land B (\emptyset) = B (z))))$
74	49 63 73	mpbir2and	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land 1_{𝑜} \subseteq D) \to ⟨C, B (\emptyset)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
75	74	ex	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (1_{𝑜} \subseteq D \to ⟨C, B (\emptyset)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\})$
76		ordirr	$⊢ Ord C \to \neg C \in C$
77	43 76	syl	$⊢ C \in On \to \neg C \in C$
78	77	adantr	$⊢ (C \in On \land D \in On) \to \neg C \in C$
79	78	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to \neg C \in C$
80		fndm	$⊢ A Fn C \to dom A = C$
81	80	adantr	$⊢ (A Fn C \land B Fn D) \to dom A = C$
82	81	adantr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to dom A = C$
83	79 82	neleqtrrd	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to \neg C \in dom A$
84	50	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to C \in On$
85		fvexd	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to B (\emptyset) \in V$
86	84 85	opeldmd	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (⟨C, B (\emptyset)⟩ \in A \to C \in dom A)$
87	83 86	mtod	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to \neg ⟨C, B (\emptyset)⟩ \in A$
88	75 87	jctird	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (1_{𝑜} \subseteq D \to (⟨C, B (\emptyset)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \land \neg ⟨C, B (\emptyset)⟩ \in A))$
89		nelss	$⊢ (⟨C, B (\emptyset)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \land \neg ⟨C, B (\emptyset)⟩ \in A) \to \neg \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \subseteq A$
90	88 89	syl6	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (1_{𝑜} \subseteq D \to \neg \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \subseteq A)$
91	31 90	syld	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (\neg D = \emptyset \to \neg \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \subseteq A)$
92	19 91	impcon4bid	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (D = \emptyset \leftrightarrow \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \subseteq A)$
93	8 92	bitrd	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (B = \emptyset \leftrightarrow \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \subseteq A)$
94		ssequn2	$⊢ \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \subseteq A \leftrightarrow A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = A$
95	93 94	bitrdi	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (B = \emptyset \leftrightarrow A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = A)$
96	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)))\}$
97	96	eqeq1d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A \underset{˙}{+} B = A \leftrightarrow A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = A)$
98	95 97	bitr4d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (B = \emptyset \leftrightarrow A \underset{˙}{+} B = A)$

Metamath Proof Explorer

Theorem tfsconcatb0

Proof