tfsconcat0b

Description: The concatentation with the empty series leaves the finite series unchanged. (Contributed by RP, 1-Mar-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	tfsconcat0b	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to (A = \emptyset \leftrightarrow 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		nnon	$⊢ D \in ω \to D \in On$
3	2	anim2i	$⊢ (C \in On \land D \in ω) \to (C \in On \land D \in On)$
4	3	anim2i	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to ((A Fn C \land B Fn D) \land (C \in On \land D \in On))$
5	1	tfsconcat0i	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A = \emptyset \to A \underset{˙}{+} B = B)$
6	4 5	syl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to (A = \emptyset \to A \underset{˙}{+} B = B)$
7		dmeq	$⊢ A \underset{˙}{+} B = B \to dom (A \underset{˙}{+} B) = dom B$
8		nna0r	$⊢ D \in ω \to \emptyset +_{𝑜} D = D$
9	8	adantl	$⊢ (C \in On \land D \in ω) \to \emptyset +_{𝑜} D = D$
10	9	eqeq2d	$⊢ (C \in On \land D \in ω) \to (C +_{𝑜} D = \emptyset +_{𝑜} D \leftrightarrow C +_{𝑜} D = D)$
11		eqcom	$⊢ C +_{𝑜} D = \emptyset +_{𝑜} D \leftrightarrow \emptyset +_{𝑜} D = C +_{𝑜} D$
12	10 11	bitr3di	$⊢ (C \in On \land D \in ω) \to (C +_{𝑜} D = D \leftrightarrow \emptyset +_{𝑜} D = C +_{𝑜} D)$
13		on0eln0	$⊢ C \in On \to (\emptyset \in C \leftrightarrow C \neq \emptyset)$
14	13	adantr	$⊢ (C \in On \land D \in ω) \to (\emptyset \in C \leftrightarrow C \neq \emptyset)$
15		df-ne	$⊢ C \neq \emptyset \leftrightarrow \neg C = \emptyset$
16	14 15	bitr2di	$⊢ (C \in On \land D \in ω) \to (\neg C = \emptyset \leftrightarrow \emptyset \in C)$
17		peano1	$⊢ \emptyset \in ω$
18		nnaordr	$⊢ (\emptyset \in ω \land C \in ω \land D \in ω) \to (\emptyset \in C \leftrightarrow \emptyset +_{𝑜} D \in (C +_{𝑜} D))$
19	17 18	mp3an1	$⊢ (C \in ω \land D \in ω) \to (\emptyset \in C \leftrightarrow \emptyset +_{𝑜} D \in (C +_{𝑜} D))$
20	19	biimpd	$⊢ (C \in ω \land D \in ω) \to (\emptyset \in C \to \emptyset +_{𝑜} D \in (C +_{𝑜} D))$
21	20	ex	$⊢ C \in ω \to (D \in ω \to (\emptyset \in C \to \emptyset +_{𝑜} D \in (C +_{𝑜} D)))$
22	21	a1i	$⊢ C \in On \to (C \in ω \to (D \in ω \to (\emptyset \in C \to \emptyset +_{𝑜} D \in (C +_{𝑜} D))))$
23		simpr	$⊢ ((C \in On \land D \in ω) \land ω \subseteq C) \to ω \subseteq C$
24		oaword1	$⊢ (C \in On \land D \in On) \to C \subseteq C +_{𝑜} D$
25	3 24	syl	$⊢ (C \in On \land D \in ω) \to C \subseteq C +_{𝑜} D$
26	25	adantr	$⊢ ((C \in On \land D \in ω) \land ω \subseteq C) \to C \subseteq C +_{𝑜} D$
27	23 26	sstrd	$⊢ ((C \in On \land D \in ω) \land ω \subseteq C) \to ω \subseteq C +_{𝑜} D$
28		id	$⊢ D \in ω \to D \in ω$
29	8 28	eqeltrd	$⊢ D \in ω \to \emptyset +_{𝑜} D \in ω$
30	29	ad2antlr	$⊢ ((C \in On \land D \in ω) \land ω \subseteq C) \to \emptyset +_{𝑜} D \in ω$
31	27 30	sseldd	$⊢ ((C \in On \land D \in ω) \land ω \subseteq C) \to \emptyset +_{𝑜} D \in (C +_{𝑜} D)$
32	31	a1d	$⊢ ((C \in On \land D \in ω) \land ω \subseteq C) \to (\emptyset \in C \to \emptyset +_{𝑜} D \in (C +_{𝑜} D))$
33	32	exp31	$⊢ C \in On \to (D \in ω \to (ω \subseteq C \to (\emptyset \in C \to \emptyset +_{𝑜} D \in (C +_{𝑜} D))))$
34	33	com23	$⊢ C \in On \to (ω \subseteq C \to (D \in ω \to (\emptyset \in C \to \emptyset +_{𝑜} D \in (C +_{𝑜} D))))$
35		eloni	$⊢ C \in On \to Ord C$
36		ordom	$⊢ Ord ω$
37		ordtri2or	$⊢ (Ord C \land Ord ω) \to (C \in ω \lor ω \subseteq C)$
38	35 36 37	sylancl	$⊢ C \in On \to (C \in ω \lor ω \subseteq C)$
39	22 34 38	mpjaod	$⊢ C \in On \to (D \in ω \to (\emptyset \in C \to \emptyset +_{𝑜} D \in (C +_{𝑜} D)))$
40	39	imp	$⊢ (C \in On \land D \in ω) \to (\emptyset \in C \to \emptyset +_{𝑜} D \in (C +_{𝑜} D))$
41		elneq	$⊢ \emptyset +_{𝑜} D \in (C +_{𝑜} D) \to \emptyset +_{𝑜} D \neq C +_{𝑜} D$
42	41	neneqd	$⊢ \emptyset +_{𝑜} D \in (C +_{𝑜} D) \to \neg \emptyset +_{𝑜} D = C +_{𝑜} D$
43	40 42	syl6	$⊢ (C \in On \land D \in ω) \to (\emptyset \in C \to \neg \emptyset +_{𝑜} D = C +_{𝑜} D)$
44	16 43	sylbid	$⊢ (C \in On \land D \in ω) \to (\neg C = \emptyset \to \neg \emptyset +_{𝑜} D = C +_{𝑜} D)$
45	44	con4d	$⊢ (C \in On \land D \in ω) \to (\emptyset +_{𝑜} D = C +_{𝑜} D \to C = \emptyset)$
46	12 45	sylbid	$⊢ (C \in On \land D \in ω) \to (C +_{𝑜} D = D \to C = \emptyset)$
47	46	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to (C +_{𝑜} D = D \to C = \emptyset)$
48	1	tfsconcatfn	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A \underset{˙}{+} B) Fn (C +_{𝑜} D)$
49	4 48	syl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to (A \underset{˙}{+} B) Fn (C +_{𝑜} D)$
50	49	fndmd	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to dom (A \underset{˙}{+} B) = C +_{𝑜} D$
51		fndm	$⊢ B Fn D \to dom B = D$
52	51	ad2antlr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to dom B = D$
53	50 52	eqeq12d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to (dom (A \underset{˙}{+} B) = dom B \leftrightarrow C +_{𝑜} D = D)$
54		fnrel	$⊢ A Fn C \to Rel A$
55		reldm0	$⊢ Rel A \to (A = \emptyset \leftrightarrow dom A = \emptyset)$
56	54 55	syl	$⊢ A Fn C \to (A = \emptyset \leftrightarrow dom A = \emptyset)$
57		fndm	$⊢ A Fn C \to dom A = C$
58	57	eqeq1d	$⊢ A Fn C \to (dom A = \emptyset \leftrightarrow C = \emptyset)$
59	56 58	bitrd	$⊢ A Fn C \to (A = \emptyset \leftrightarrow C = \emptyset)$
60	59	adantr	$⊢ (A Fn C \land B Fn D) \to (A = \emptyset \leftrightarrow C = \emptyset)$
61	60	adantr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to (A = \emptyset \leftrightarrow C = \emptyset)$
62	47 53 61	3imtr4d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to (dom (A \underset{˙}{+} B) = dom B \to A = \emptyset)$
63	7 62	syl5	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to (A \underset{˙}{+} B = B \to A = \emptyset)$
64	6 63	impbid	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in ω)) \to (A = \emptyset \leftrightarrow A \underset{˙}{+} B = B)$

Metamath Proof Explorer

Theorem tfsconcat0b

Proof