tfsconcatfv2

Description: A latter 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	tfsconcatfv2	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to (A \underset{˙}{+} B) (C +_{𝑜} X) = B (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) (C +_{𝑜} X) = (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}) (C +_{𝑜} X)$
4	3	adantr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to (A \underset{˙}{+} B) (C +_{𝑜} X) = (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}) (C +_{𝑜} X)$
5		simplll	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \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		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)))\}$
13	12	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)$
14	11 13	sylib	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} Fn ((C +_{𝑜} D) ∖ C)$
15	14	adantr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \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 D) \to C \cap ((C +_{𝑜} D) ∖ C) = \emptyset$
18		pm3.22	$⊢ (C \in On \land D \in On) \to (D \in On \land C \in On)$
19	18	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (D \in On \land C \in On)$
20		oaordi	$⊢ (D \in On \land C \in On) \to (X \in D \to C +_{𝑜} X \in (C +_{𝑜} D))$
21	19 20	syl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (X \in D \to C +_{𝑜} X \in (C +_{𝑜} D))$
22	21	imp	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to C +_{𝑜} X \in (C +_{𝑜} D)$
23		simplrl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to C \in On$
24		simpr	$⊢ (C \in On \land D \in On) \to D \in On$
25	24	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to D \in On$
26		onelon	$⊢ (D \in On \land X \in D) \to X \in On$
27	25 26	sylan	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to X \in On$
28		oaword1	$⊢ (C \in On \land X \in On) \to C \subseteq C +_{𝑜} X$
29	23 27 28	syl2anc	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to C \subseteq C +_{𝑜} X$
30		oacl	$⊢ (C \in On \land D \in On) \to C +_{𝑜} D \in On$
31		eloni	$⊢ C +_{𝑜} D \in On \to Ord (C +_{𝑜} D)$
32	30 31	syl	$⊢ (C \in On \land D \in On) \to Ord (C +_{𝑜} D)$
33		eloni	$⊢ C \in On \to Ord C$
34	33	adantr	$⊢ (C \in On \land D \in On) \to Ord C$
35	32 34	jca	$⊢ (C \in On \land D \in On) \to (Ord (C +_{𝑜} D) \land Ord C)$
36	35	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (Ord (C +_{𝑜} D) \land Ord C)$
37	36	adantr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to (Ord (C +_{𝑜} D) \land Ord C)$
38		ordeldif	$⊢ (Ord (C +_{𝑜} D) \land Ord C) \to (C +_{𝑜} X \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (C +_{𝑜} X \in (C +_{𝑜} D) \land C \subseteq C +_{𝑜} X))$
39	37 38	syl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to (C +_{𝑜} X \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (C +_{𝑜} X \in (C +_{𝑜} D) \land C \subseteq C +_{𝑜} X))$
40	22 29 39	mpbir2and	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to C +_{𝑜} X \in ((C +_{𝑜} D) ∖ C)$
41	5 15 17 40	fvun2d	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}) (C +_{𝑜} X) = \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} (C +_{𝑜} X)$
42		eqid	$⊢ C +_{𝑜} X = C +_{𝑜} X$
43		eqid	$⊢ B (X) = B (X)$
44		oveq2	$⊢ z = X \to C +_{𝑜} z = C +_{𝑜} X$
45	44	eqeq2d	$⊢ z = X \to (C +_{𝑜} X = C +_{𝑜} z \leftrightarrow C +_{𝑜} X = C +_{𝑜} X)$
46		fveq2	$⊢ z = X \to B (z) = B (X)$
47	46	eqeq2d	$⊢ z = X \to (B (X) = B (z) \leftrightarrow B (X) = B (X))$
48	45 47	anbi12d	$⊢ z = X \to ((C +_{𝑜} X = C +_{𝑜} z \land B (X) = B (z)) \leftrightarrow (C +_{𝑜} X = C +_{𝑜} X \land B (X) = B (X)))$
49	48	rspcev	$⊢ (X \in D \land (C +_{𝑜} X = C +_{𝑜} X \land B (X) = B (X))) \to \exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land B (X) = B (z))$
50	42 43 49	mpanr12	$⊢ X \in D \to \exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land B (X) = B (z))$
51	50	adantl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to \exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land B (X) = B (z))$
52		ovex	$⊢ C +_{𝑜} X \in V$
53		fvex	$⊢ B (X) \in V$
54	52 53	pm3.2i	$⊢ (C +_{𝑜} X \in V \land B (X) \in V)$
55		eleq1	$⊢ x = C +_{𝑜} X \to (x \in ((C +_{𝑜} D) ∖ C) \leftrightarrow C +_{𝑜} X \in ((C +_{𝑜} D) ∖ C))$
56		eqeq1	$⊢ x = C +_{𝑜} X \to (x = C +_{𝑜} z \leftrightarrow C +_{𝑜} X = C +_{𝑜} z)$
57	56	anbi1d	$⊢ x = C +_{𝑜} X \to ((x = C +_{𝑜} z \land y = B (z)) \leftrightarrow (C +_{𝑜} X = C +_{𝑜} z \land y = B (z)))$
58	57	rexbidv	$⊢ x = C +_{𝑜} X \to (\exists z \in D (x = C +_{𝑜} z \land y = B (z)) \leftrightarrow \exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land y = B (z)))$
59	55 58	anbi12d	$⊢ x = C +_{𝑜} X \to ((x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z))) \leftrightarrow (C +_{𝑜} X \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land y = B (z))))$
60		eqeq1	$⊢ y = B (X) \to (y = B (z) \leftrightarrow B (X) = B (z))$
61	60	anbi2d	$⊢ y = B (X) \to ((C +_{𝑜} X = C +_{𝑜} z \land y = B (z)) \leftrightarrow (C +_{𝑜} X = C +_{𝑜} z \land B (X) = B (z)))$
62	61	rexbidv	$⊢ y = B (X) \to (\exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land y = B (z)) \leftrightarrow \exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land B (X) = B (z)))$
63	62	anbi2d	$⊢ y = B (X) \to ((C +_{𝑜} X \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land y = B (z))) \leftrightarrow (C +_{𝑜} X \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land B (X) = B (z))))$
64	59 63	opelopabg	$⊢ (C +_{𝑜} X \in V \land B (X) \in V) \to (⟨C +_{𝑜} X, B (X)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \leftrightarrow (C +_{𝑜} X \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land B (X) = B (z))))$
65	54 64	mp1i	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to (⟨C +_{𝑜} X, B (X)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} \leftrightarrow (C +_{𝑜} X \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (C +_{𝑜} X = C +_{𝑜} z \land B (X) = B (z))))$
66	40 51 65	mpbir2and	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to ⟨C +_{𝑜} X, B (X)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
67		fnopfvb	$⊢ (\{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} Fn ((C +_{𝑜} D) ∖ C) \land C +_{𝑜} X \in ((C +_{𝑜} D) ∖ C)) \to (\{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} (C +_{𝑜} X) = B (X) \leftrightarrow ⟨C +_{𝑜} X, B (X)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\})$
68	15 40 67	syl2anc	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to (\{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} (C +_{𝑜} X) = B (X) \leftrightarrow ⟨C +_{𝑜} X, B (X)⟩ \in \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\})$
69	66 68	mpbird	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} (C +_{𝑜} X) = B (X)$
70	4 41 69	3eqtrd	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land X \in D) \to (A \underset{˙}{+} B) (C +_{𝑜} X) = B (X)$

Metamath Proof Explorer

Theorem tfsconcatfv2

Proof