tfsconcatrn

Description: The range of the concatenation of two transfinite series. (Contributed by RP, 24-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	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$

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	rneqd	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ran (A \underset{˙}{+} B) = ran (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\})$
4		rnun	$⊢ ran (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}) = ran A \cup ran \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
5	4	a1i	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ran (A \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}) = ran A \cup ran \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
6		df-rex	$⊢ \exists x \in ((C +_{𝑜} D) ∖ C) \exists z \in D (x = C +_{𝑜} z \land y = B (z)) \leftrightarrow \exists x (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))$
7		pm3.22	$⊢ (C \in On \land D \in On) \to (D \in On \land C \in On)$
8	7	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (D \in On \land C \in On)$
9		oaordi	$⊢ (D \in On \land C \in On) \to (d \in D \to C +_{𝑜} d \in (C +_{𝑜} D))$
10	8 9	syl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (d \in D \to C +_{𝑜} d \in (C +_{𝑜} D))$
11	10	imp	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D) \to C +_{𝑜} d \in (C +_{𝑜} D)$
12		simplrl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D) \to C \in On$
13		simprr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to D \in On$
14		onelon	$⊢ (D \in On \land d \in D) \to d \in On$
15	13 14	sylan	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D) \to d \in On$
16		oaword1	$⊢ (C \in On \land d \in On) \to C \subseteq C +_{𝑜} d$
17	12 15 16	syl2anc	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D) \to C \subseteq C +_{𝑜} d$
18		oacl	$⊢ (C \in On \land D \in On) \to C +_{𝑜} D \in On$
19	18	ad2antlr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D) \to C +_{𝑜} D \in On$
20		eloni	$⊢ C +_{𝑜} D \in On \to Ord (C +_{𝑜} D)$
21	19 20	syl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D) \to Ord (C +_{𝑜} D)$
22		eloni	$⊢ C \in On \to Ord C$
23	12 22	syl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D) \to Ord C$
24		ordeldif	$⊢ (Ord (C +_{𝑜} D) \land Ord C) \to (C +_{𝑜} d \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (C +_{𝑜} d \in (C +_{𝑜} D) \land C \subseteq C +_{𝑜} d))$
25	21 23 24	syl2anc	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D) \to (C +_{𝑜} d \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (C +_{𝑜} d \in (C +_{𝑜} D) \land C \subseteq C +_{𝑜} d))$
26	11 17 25	mpbir2and	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D) \to C +_{𝑜} d \in ((C +_{𝑜} D) ∖ C)$
27		simpr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (C \in On \land D \in On)$
28	27	adantr	$⊢ (((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 \land D \in On)$
29	18 20	syl	$⊢ (C \in On \land D \in On) \to Ord (C +_{𝑜} D)$
30	22	adantr	$⊢ (C \in On \land D \in On) \to Ord C$
31	29 30	jca	$⊢ (C \in On \land D \in On) \to (Ord (C +_{𝑜} D) \land Ord C)$
32	31	adantl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (Ord (C +_{𝑜} D) \land Ord C)$
33		ordeldif	$⊢ (Ord (C +_{𝑜} D) \land Ord C) \to (x \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (x \in (C +_{𝑜} D) \land C \subseteq x))$
34	32 33	syl	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (x \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (x \in (C +_{𝑜} D) \land C \subseteq x))$
35	34	biimpa	$⊢ (((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) \land C \subseteq x)$
36	35	ancomd	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to (C \subseteq x \land x \in (C +_{𝑜} D))$
37		oawordex2	$⊢ ((C \in On \land D \in On) \land (C \subseteq x \land x \in (C +_{𝑜} D))) \to \exists d \in D C +_{𝑜} d = x$
38	28 36 37	syl2anc	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to \exists d \in D C +_{𝑜} d = x$
39		eqcom	$⊢ C +_{𝑜} d = x \leftrightarrow x = C +_{𝑜} d$
40	39	rexbii	$⊢ \exists d \in D C +_{𝑜} d = x \leftrightarrow \exists d \in D x = C +_{𝑜} d$
41	38 40	sylib	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to \exists d \in D x = C +_{𝑜} d$
42		simpr	$⊢ (((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \land x = C +_{𝑜} z) \to x = C +_{𝑜} z$
43		simpll3	$⊢ (((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \land x = C +_{𝑜} z) \to x = C +_{𝑜} d$
44	42 43	eqtr3d	$⊢ (((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \land x = C +_{𝑜} z) \to C +_{𝑜} z = C +_{𝑜} d$
45		simp1rl	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \to C \in On$
46	45	adantr	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \to C \in On$
47		simp1rr	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \to D \in On$
48		onelon	$⊢ (D \in On \land z \in D) \to z \in On$
49	47 48	sylan	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \to z \in On$
50		simp2	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \to d \in D$
51	47 50 14	syl2anc	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \to d \in On$
52	51	adantr	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \to d \in On$
53	46 49 52	3jca	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \to (C \in On \land z \in On \land d \in On)$
54	53	adantr	$⊢ (((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \land x = C +_{𝑜} z) \to (C \in On \land z \in On \land d \in On)$
55		oacan	$⊢ (C \in On \land z \in On \land d \in On) \to (C +_{𝑜} z = C +_{𝑜} d \leftrightarrow z = d)$
56	54 55	syl	$⊢ (((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \land x = C +_{𝑜} z) \to (C +_{𝑜} z = C +_{𝑜} d \leftrightarrow z = d)$
57	44 56	mpbid	$⊢ (((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \land x = C +_{𝑜} z) \to z = d$
58		velsn	$⊢ z \in \{d\} \leftrightarrow z = d$
59	57 58	sylibr	$⊢ (((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \land x = C +_{𝑜} z) \to z \in \{d\}$
60	59	ex	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \to (x = C +_{𝑜} z \to z \in \{d\})$
61	60	adantrd	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land z \in D) \to ((x = C +_{𝑜} z \land y = B (z)) \to z \in \{d\})$
62	61	expimpd	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \to ((z \in D \land (x = C +_{𝑜} z \land y = B (z))) \to z \in \{d\})$
63		simprr	$⊢ (z \in D \land (x = C +_{𝑜} z \land y = B (z))) \to y = B (z)$
64	62 63	jca2	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \to ((z \in D \land (x = C +_{𝑜} z \land y = B (z))) \to (z \in \{d\} \land y = B (z)))$
65	64	reximdv2	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \to (\exists z \in D (x = C +_{𝑜} z \land y = B (z)) \to \exists z \in \{d\} y = B (z))$
66		vex	$⊢ d \in V$
67		fveq2	$⊢ z = d \to B (z) = B (d)$
68	67	eqeq2d	$⊢ z = d \to (y = B (z) \leftrightarrow y = B (d))$
69	66 68	rexsn	$⊢ \exists z \in \{d\} y = B (z) \leftrightarrow y = B (d)$
70	65 69	imbitrdi	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \to (\exists z \in D (x = C +_{𝑜} z \land y = B (z)) \to y = B (d))$
71	50	adantr	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land y = B (d)) \to d \in D$
72		simpl3	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land y = B (d)) \to x = C +_{𝑜} d$
73		simpr	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land y = B (d)) \to y = B (d)$
74		oveq2	$⊢ z = d \to C +_{𝑜} z = C +_{𝑜} d$
75	74	eqeq2d	$⊢ z = d \to (x = C +_{𝑜} z \leftrightarrow x = C +_{𝑜} d)$
76	75 68	anbi12d	$⊢ z = d \to ((x = C +_{𝑜} z \land y = B (z)) \leftrightarrow (x = C +_{𝑜} d \land y = B (d)))$
77	76	rspcev	$⊢ (d \in D \land (x = C +_{𝑜} d \land y = B (d))) \to \exists z \in D (x = C +_{𝑜} z \land y = B (z))$
78	71 72 73 77	syl12anc	$⊢ ((((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \land y = B (d)) \to \exists z \in D (x = C +_{𝑜} z \land y = B (z))$
79	78	ex	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \to (y = B (d) \to \exists z \in D (x = C +_{𝑜} z \land y = B (z)))$
80	70 79	impbid	$⊢ (((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \land d \in D \land x = C +_{𝑜} d) \to (\exists z \in D (x = C +_{𝑜} z \land y = B (z)) \leftrightarrow y = B (d))$
81	26 41 80	rexxfrd2	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (\exists x \in ((C +_{𝑜} D) ∖ C) \exists z \in D (x = C +_{𝑜} z \land y = B (z)) \leftrightarrow \exists d \in D y = B (d))$
82	6 81	bitr3id	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to (\exists x (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z))) \leftrightarrow \exists d \in D y = B (d))$
83	82	abbidv	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to \{y \| \exists x (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = \{y \| \exists d \in D y = B (d)\}$
84		rnopab	$⊢ ran \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = \{y \| \exists x (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
85	84	a1i	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ran \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = \{y \| \exists x (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\}$
86		fnrnfv	$⊢ B Fn D \to ran B = \{y \| \exists d \in D y = B (d)\}$
87	86	ad2antlr	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ran B = \{y \| \exists d \in D y = B (d)\}$
88	83 85 87	3eqtr4d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ran \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = ran B$
89	88	uneq2d	$⊢ ((A Fn C \land B Fn D) \land (C \in On \land D \in On)) \to ran A \cup ran \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = B (z)))\} = ran A \cup ran B$
90	3 5 89	3eqtrd	$⊢ ((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$

Metamath Proof Explorer

Theorem tfsconcatrn

Proof