Metamath Proof Explorer

Theorem tfsconcat00

Description: The concatentation of two empty series results in an empty series. (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	tfsconcat00	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ((A = \emptyset \land B = \emptyset) \leftrightarrow A \underset{˙}{+} B = \emptyset)$

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	tfsconcatrn	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ran (A \underset{˙}{+} B) = ran A \cup ran B$
3	2	eqeq1d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (ran (A \underset{˙}{+} B) = \emptyset \leftrightarrow ran A \cup ran B = \emptyset)$
4	1	tfsconcatfn	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A \underset{˙}{+} B) Fn (C +_{𝑜} D)$
5		fnrel	$⊢ (A \underset{˙}{+} B) Fn (C +_{𝑜} D) \to Rel (A \underset{˙}{+} B)$
6		relrn0	$⊢ Rel (A \underset{˙}{+} B) \to (A \underset{˙}{+} B = \emptyset \leftrightarrow ran (A \underset{˙}{+} B) = \emptyset)$
7	4 5 6	3syl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A \underset{˙}{+} B = \emptyset \leftrightarrow ran (A \underset{˙}{+} B) = \emptyset)$
8		fnrel	$⊢ A Fn C \to Rel A$
9		relrn0	$⊢ Rel A \to (A = \emptyset \leftrightarrow ran A = \emptyset)$
10	8 9	syl	$⊢ A Fn C \to (A = \emptyset \leftrightarrow ran A = \emptyset)$
11		fnrel	$⊢ B Fn D \to Rel B$
12		relrn0	$⊢ Rel B \to (B = \emptyset \leftrightarrow ran B = \emptyset)$
13	11 12	syl	$⊢ B Fn D \to (B = \emptyset \leftrightarrow ran B = \emptyset)$
14	10 13	bi2anan9	$⊢ (A Fn C \land B Fn D) \to ((A = \emptyset \land B = \emptyset) \leftrightarrow (ran A = \emptyset \land ran B = \emptyset))$
15		un00	$⊢ (ran A = \emptyset \land ran B = \emptyset) \leftrightarrow ran A \cup ran B = \emptyset$
16	14 15	bitrdi	$⊢ (A Fn C \land B Fn D) \to ((A = \emptyset \land B = \emptyset) \leftrightarrow ran A \cup ran B = \emptyset)$
17	16	adantr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ((A = \emptyset \land B = \emptyset) \leftrightarrow ran A \cup ran B = \emptyset)$
18	3 7 17	3bitr4rd	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ((A = \emptyset \land B = \emptyset) \leftrightarrow A \underset{˙}{+} B = \emptyset)$