tfsconcatfv1

Description: An early value of the concatenation of two transfinite series. (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	tfsconcatfv1	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in C) \to (A \underset{˙}{+} B) (X) = A (X)$

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	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)))\}$
3	2	fveq1d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (A \underset{˙}{+} B) (X) = (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}) (X)$
4	3	adantr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in C) \to (A \underset{˙}{+} B) (X) = (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}) (X)$
5		simplll	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in C) \to A Fn C$
6		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$
7		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$
8		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)$
9		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))$
10	6 7 8 9	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))$
11	10	ralrimiva	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to \forall x \in ((C +_{𝑜} D) ∖ C) \exists! y \exists z \in D (x = C +_{𝑜} z \land y = B (z))$
12	11	adantr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in C) \to \forall x \in ((C +_{𝑜} D) ∖ C) \exists! y \exists z \in D (x = C +_{𝑜} z \land y = B (z))$
13		eqid	$⊢ \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
14	13	fnopabg	$⊢ \forall x \in ((C +_{𝑜} D) ∖ C) \exists! y \exists z \in D (x = C +_{𝑜} z \land y = B (z)) \leftrightarrow \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} Fn ((C +_{𝑜} D) ∖ C)$
15	12 14	sylib	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in C) \to \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} Fn ((C +_{𝑜} D) ∖ C)$
16		disjdif	$⊢ C \cap ((C +_{𝑜} D) ∖ C) = \emptyset$
17	16	a1i	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in C) \to C \cap ((C +_{𝑜} D) ∖ C) = \emptyset$
18		simpr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in C) \to X \in C$
19	5 15 17 18	fvun1d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in C) \to (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}) (X) = A (X)$
20	4 19	eqtrd	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in C) \to (A \underset{˙}{+} B) (X) = A (X)$

Metamath Proof Explorer

Theorem tfsconcatfv1

Proof