tfsconcatrev

Description: If the domain of a transfinite sequence is an ordinal sum, the sequence can be decomposed into two sequences with domains corresponding to the addends. Theorem 2 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-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	tfsconcatrev	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to \exists u \in ({ran F}^{C}) \exists v \in ({ran F}^{D}) (u \underset{˙}{+} v = F \land dom u = C \land dom v = D)$

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		dffn3	$⊢ F Fn (C +_{𝑜} D) \leftrightarrow F : C +_{𝑜} D ⟶ ran F$
3	2	biimpi	$⊢ F Fn (C +_{𝑜} D) \to F : C +_{𝑜} D ⟶ ran F$
4	3	adantr	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to F : C +_{𝑜} D ⟶ ran F$
5		fndm	$⊢ F Fn (C +_{𝑜} D) \to dom F = C +_{𝑜} D$
6	5	adantr	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to dom F = C +_{𝑜} D$
7		oacl	$⊢ (C \in On \land D \in On) \to C +_{𝑜} D \in On$
8	7	adantl	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to C +_{𝑜} D \in On$
9	6 8	eqeltrd	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to dom F \in On$
10		fnfun	$⊢ F Fn (C +_{𝑜} D) \to Fun F$
11	10	adantr	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to Fun F$
12		funrnex	$⊢ dom F \in On \to (Fun F \to ran F \in V)$
13	9 11 12	sylc	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to ran F \in V$
14	13 8	elmapd	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to (F \in ({ran F}^{(C +_{𝑜} D)}) \leftrightarrow F : C +_{𝑜} D ⟶ ran F)$
15	4 14	mpbird	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to F \in ({ran F}^{(C +_{𝑜} D)})$
16		oaword1	$⊢ (C \in On \land D \in On) \to C \subseteq C +_{𝑜} D$
17	16	adantl	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to C \subseteq C +_{𝑜} D$
18		elmapssres	$⊢ (F \in ({ran F}^{(C +_{𝑜} D)}) \land C \subseteq C +_{𝑜} D) \to {F ↾}_{C} \in ({ran F}^{C})$
19	15 17 18	syl2anc	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to {F ↾}_{C} \in ({ran F}^{C})$
20		simpl	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to F Fn (C +_{𝑜} D)$
21		oaordi	$⊢ (D \in On \land C \in On) \to (d \in D \to C +_{𝑜} d \in (C +_{𝑜} D))$
22	21	ancoms	$⊢ (C \in On \land D \in On) \to (d \in D \to C +_{𝑜} d \in (C +_{𝑜} D))$
23	22	adantl	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to (d \in D \to C +_{𝑜} d \in (C +_{𝑜} D))$
24	23	imp	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land d \in D) \to C +_{𝑜} d \in (C +_{𝑜} D)$
25		fnfvelrn	$⊢ (F Fn (C +_{𝑜} D) \land C +_{𝑜} d \in (C +_{𝑜} D)) \to F (C +_{𝑜} d) \in ran F$
26	20 24 25	syl2an2r	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land d \in D) \to F (C +_{𝑜} d) \in ran F$
27	26	fmpttd	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to (d \in D ⟼ F (C +_{𝑜} d)) : D ⟶ ran F$
28		simprr	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to D \in On$
29	13 28	elmapd	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to ((d \in D ⟼ F (C +_{𝑜} d)) \in ({ran F}^{D}) \leftrightarrow (d \in D ⟼ F (C +_{𝑜} d)) : D ⟶ ran F)$
30	27 29	mpbird	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to (d \in D ⟼ F (C +_{𝑜} d)) \in ({ran F}^{D})$
31	20 17	fnssresd	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to ({F ↾}_{C}) Fn C$
32		fvex	$⊢ F (C +_{𝑜} d) \in V$
33		eqid	$⊢ (d \in D ⟼ F (C +_{𝑜} d)) = (d \in D ⟼ F (C +_{𝑜} d))$
34	32 33	fnmpti	$⊢ (d \in D ⟼ F (C +_{𝑜} d)) Fn D$
35	34	a1i	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to (d \in D ⟼ F (C +_{𝑜} d)) Fn D$
36		simpr	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to (C \in On \land D \in On)$
37	1	tfsconcatun	$⊢ ((({F ↾}_{C}) Fn C \land (d \in D ⟼ F (C +_{𝑜} d)) Fn D) \land (C \in On \land D \in On)) \to ({F ↾}_{C}) \underset{˙}{+} (d \in D ⟼ F (C +_{𝑜} d)) = ({F ↾}_{C}) \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z)))\}$
38	31 35 36 37	syl21anc	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to ({F ↾}_{C}) \underset{˙}{+} (d \in D ⟼ F (C +_{𝑜} d)) = ({F ↾}_{C}) \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z)))\}$
39		oveq2	$⊢ d = z \to C +_{𝑜} d = C +_{𝑜} z$
40	39	fveq2d	$⊢ d = z \to F (C +_{𝑜} d) = F (C +_{𝑜} z)$
41		fvex	$⊢ F (C +_{𝑜} z) \in V$
42	40 33 41	fvmpt	$⊢ z \in D \to (d \in D ⟼ F (C +_{𝑜} d)) (z) = F (C +_{𝑜} z)$
43	42	ad2antlr	$⊢ ((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land z \in D) \land x = C +_{𝑜} z) \to (d \in D ⟼ F (C +_{𝑜} d)) (z) = F (C +_{𝑜} z)$
44		fveq2	$⊢ x = C +_{𝑜} z \to F (x) = F (C +_{𝑜} z)$
45	44	adantl	$⊢ ((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land z \in D) \land x = C +_{𝑜} z) \to F (x) = F (C +_{𝑜} z)$
46	43 45	eqtr4d	$⊢ ((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land z \in D) \land x = C +_{𝑜} z) \to (d \in D ⟼ F (C +_{𝑜} d)) (z) = F (x)$
47	46	eqeq2d	$⊢ ((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land z \in D) \land x = C +_{𝑜} z) \to (y = (d \in D ⟼ F (C +_{𝑜} d)) (z) \leftrightarrow y = F (x))$
48	47	biimpd	$⊢ ((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land z \in D) \land x = C +_{𝑜} z) \to (y = (d \in D ⟼ F (C +_{𝑜} d)) (z) \to y = F (x))$
49	48	expimpd	$⊢ (((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land z \in D) \to ((x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z)) \to y = F (x))$
50	49	rexlimdva	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to (\exists z \in D (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z)) \to y = F (x))$
51		simplr	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to (C \in On \land D \in On)$
52		eloni	$⊢ C +_{𝑜} D \in On \to Ord (C +_{𝑜} D)$
53	7 52	syl	$⊢ (C \in On \land D \in On) \to Ord (C +_{𝑜} D)$
54		eloni	$⊢ C \in On \to Ord C$
55	54	adantr	$⊢ (C \in On \land D \in On) \to Ord C$
56		ordeldif	$⊢ (Ord (C +_{𝑜} D) \land Ord C) \to (x \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (x \in (C +_{𝑜} D) \land C \subseteq x))$
57	53 55 56	syl2anc	$⊢ (C \in On \land D \in On) \to (x \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (x \in (C +_{𝑜} D) \land C \subseteq x))$
58	57	adantl	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to (x \in ((C +_{𝑜} D) ∖ C) \leftrightarrow (x \in (C +_{𝑜} D) \land C \subseteq x))$
59	58	biimpa	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to (x \in (C +_{𝑜} D) \land C \subseteq x)$
60	59	ancomd	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to (C \subseteq x \land x \in (C +_{𝑜} D))$
61	51 60	jca	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to ((C \in On \land D \in On) \land (C \subseteq x \land x \in (C +_{𝑜} D)))$
62	61	adantr	$⊢ (((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \to ((C \in On \land D \in On) \land (C \subseteq x \land x \in (C +_{𝑜} D)))$
63		oawordex2	$⊢ ((C \in On \land D \in On) \land (C \subseteq x \land x \in (C +_{𝑜} D))) \to \exists z \in D C +_{𝑜} z = x$
64	62 63	syl	$⊢ (((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \to \exists z \in D C +_{𝑜} z = x$
65		simpr	$⊢ (((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \land z \in D) \land C +_{𝑜} z = x) \to C +_{𝑜} z = x$
66	65	eqcomd	$⊢ (((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \land z \in D) \land C +_{𝑜} z = x) \to x = C +_{𝑜} z$
67	65	fveq2d	$⊢ (((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \land z \in D) \land C +_{𝑜} z = x) \to F (C +_{𝑜} z) = F (x)$
68	42	ad2antlr	$⊢ (((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \land z \in D) \land C +_{𝑜} z = x) \to (d \in D ⟼ F (C +_{𝑜} d)) (z) = F (C +_{𝑜} z)$
69		simpllr	$⊢ (((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \land z \in D) \land C +_{𝑜} z = x) \to y = F (x)$
70	67 68 69	3eqtr4rd	$⊢ (((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \land z \in D) \land C +_{𝑜} z = x) \to y = (d \in D ⟼ F (C +_{𝑜} d)) (z)$
71	66 70	jca	$⊢ (((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \land z \in D) \land C +_{𝑜} z = x) \to (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z))$
72	71	ex	$⊢ ((((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \land z \in D) \to (C +_{𝑜} z = x \to (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z)))$
73	72	reximdva	$⊢ (((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \to (\exists z \in D C +_{𝑜} z = x \to \exists z \in D (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z)))$
74	64 73	mpd	$⊢ (((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \land y = F (x)) \to \exists z \in D (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z))$
75	74	ex	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to (y = F (x) \to \exists z \in D (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z)))$
76	50 75	impbid	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to (\exists z \in D (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z)) \leftrightarrow y = F (x))$
77		eldifi	$⊢ x \in ((C +_{𝑜} D) ∖ C) \to x \in (C +_{𝑜} D)$
78		eqcom	$⊢ y = F (x) \leftrightarrow F (x) = y$
79		fnbrfvb	$⊢ (F Fn (C +_{𝑜} D) \land x \in (C +_{𝑜} D)) \to (F (x) = y \leftrightarrow x F y)$
80	78 79	bitrid	$⊢ (F Fn (C +_{𝑜} D) \land x \in (C +_{𝑜} D)) \to (y = F (x) \leftrightarrow x F y)$
81	20 77 80	syl2an	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to (y = F (x) \leftrightarrow x F y)$
82	76 81	bitrd	$⊢ ((F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \land x \in ((C +_{𝑜} D) ∖ C)) \to (\exists z \in D (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z)) \leftrightarrow x F y)$
83	82	pm5.32da	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to ((x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z))) \leftrightarrow (x \in ((C +_{𝑜} D) ∖ C) \land x F y))$
84	83	opabbidv	$⊢ (F Fn (C +_{𝑜} 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 = (d \in D ⟼ F (C +_{𝑜} d)) (z)))\} = \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land x F y)\}$
85		dfres2	$⊢ {F ↾}_{((C +_{𝑜} D) ∖ C)} = \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land x F y)\}$
86	84 85	eqtr4di	$⊢ (F Fn (C +_{𝑜} 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 = (d \in D ⟼ F (C +_{𝑜} d)) (z)))\} = {F ↾}_{((C +_{𝑜} D) ∖ C)}$
87	86	uneq2d	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to ({F ↾}_{C}) \cup \{⟨x, y⟩ \| (x \in ((C +_{𝑜} D) ∖ C) \land \exists z \in D (x = C +_{𝑜} z \land y = (d \in D ⟼ F (C +_{𝑜} d)) (z)))\} = ({F ↾}_{C}) \cup ({F ↾}_{((C +_{𝑜} D) ∖ C)})$
88	38 87	eqtrd	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to ({F ↾}_{C}) \underset{˙}{+} (d \in D ⟼ F (C +_{𝑜} d)) = ({F ↾}_{C}) \cup ({F ↾}_{((C +_{𝑜} D) ∖ C)})$
89		resundi	$⊢ {F ↾}_{(C \cup ((C +_{𝑜} D) ∖ C))} = ({F ↾}_{C}) \cup ({F ↾}_{((C +_{𝑜} D) ∖ C)})$
90	89	a1i	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to {F ↾}_{(C \cup ((C +_{𝑜} D) ∖ C))} = ({F ↾}_{C}) \cup ({F ↾}_{((C +_{𝑜} D) ∖ C)})$
91		undif	$⊢ C \subseteq C +_{𝑜} D \leftrightarrow C \cup ((C +_{𝑜} D) ∖ C) = C +_{𝑜} D$
92	16 91	sylib	$⊢ (C \in On \land D \in On) \to C \cup ((C +_{𝑜} D) ∖ C) = C +_{𝑜} D$
93	92	adantl	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to C \cup ((C +_{𝑜} D) ∖ C) = C +_{𝑜} D$
94	93	reseq2d	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to {F ↾}_{(C \cup ((C +_{𝑜} D) ∖ C))} = {F ↾}_{(C +_{𝑜} D)}$
95		fnresdm	$⊢ F Fn (C +_{𝑜} D) \to {F ↾}_{(C +_{𝑜} D)} = F$
96	95	adantr	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to {F ↾}_{(C +_{𝑜} D)} = F$
97	94 96	eqtrd	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to {F ↾}_{(C \cup ((C +_{𝑜} D) ∖ C))} = F$
98	88 90 97	3eqtr2d	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to ({F ↾}_{C}) \underset{˙}{+} (d \in D ⟼ F (C +_{𝑜} d)) = F$
99		dmres	$⊢ dom ({F ↾}_{C}) = C \cap dom F$
100	17 6	sseqtrrd	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to C \subseteq dom F$
101		dfss2	$⊢ C \subseteq dom F \leftrightarrow C \cap dom F = C$
102	100 101	sylib	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to C \cap dom F = C$
103	99 102	eqtrid	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to dom ({F ↾}_{C}) = C$
104	32 33	dmmpti	$⊢ dom (d \in D ⟼ F (C +_{𝑜} d)) = D$
105	104	a1i	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to dom (d \in D ⟼ F (C +_{𝑜} d)) = D$
106		oveq1	$⊢ u = {F ↾}_{C} \to u \underset{˙}{+} v = ({F ↾}_{C}) \underset{˙}{+} v$
107	106	eqeq1d	$⊢ u = {F ↾}_{C} \to (u \underset{˙}{+} v = F \leftrightarrow ({F ↾}_{C}) \underset{˙}{+} v = F)$
108		dmeq	$⊢ u = {F ↾}_{C} \to dom u = dom ({F ↾}_{C})$
109	108	eqeq1d	$⊢ u = {F ↾}_{C} \to (dom u = C \leftrightarrow dom ({F ↾}_{C}) = C)$
110	107 109	3anbi12d	$⊢ u = {F ↾}_{C} \to ((u \underset{˙}{+} v = F \land dom u = C \land dom v = D) \leftrightarrow (({F ↾}_{C}) \underset{˙}{+} v = F \land dom ({F ↾}_{C}) = C \land dom v = D))$
111		oveq2	$⊢ v = (d \in D ⟼ F (C +_{𝑜} d)) \to ({F ↾}_{C}) \underset{˙}{+} v = ({F ↾}_{C}) \underset{˙}{+} (d \in D ⟼ F (C +_{𝑜} d))$
112	111	eqeq1d	$⊢ v = (d \in D ⟼ F (C +_{𝑜} d)) \to (({F ↾}_{C}) \underset{˙}{+} v = F \leftrightarrow ({F ↾}_{C}) \underset{˙}{+} (d \in D ⟼ F (C +_{𝑜} d)) = F)$
113		dmeq	$⊢ v = (d \in D ⟼ F (C +_{𝑜} d)) \to dom v = dom (d \in D ⟼ F (C +_{𝑜} d))$
114	113	eqeq1d	$⊢ v = (d \in D ⟼ F (C +_{𝑜} d)) \to (dom v = D \leftrightarrow dom (d \in D ⟼ F (C +_{𝑜} d)) = D)$
115	112 114	3anbi13d	$⊢ v = (d \in D ⟼ F (C +_{𝑜} d)) \to ((({F ↾}_{C}) \underset{˙}{+} v = F \land dom ({F ↾}_{C}) = C \land dom v = D) \leftrightarrow (({F ↾}_{C}) \underset{˙}{+} (d \in D ⟼ F (C +_{𝑜} d)) = F \land dom ({F ↾}_{C}) = C \land dom (d \in D ⟼ F (C +_{𝑜} d)) = D))$
116	110 115	rspc2ev	$⊢ ({F ↾}_{C} \in ({ran F}^{C}) \land (d \in D ⟼ F (C +_{𝑜} d)) \in ({ran F}^{D}) \land (({F ↾}_{C}) \underset{˙}{+} (d \in D ⟼ F (C +_{𝑜} d)) = F \land dom ({F ↾}_{C}) = C \land dom (d \in D ⟼ F (C +_{𝑜} d)) = D)) \to \exists u \in ({ran F}^{C}) \exists v \in ({ran F}^{D}) (u \underset{˙}{+} v = F \land dom u = C \land dom v = D)$
117	19 30 98 103 105 116	syl113anc	$⊢ (F Fn (C +_{𝑜} D) \land (C \in On \land D \in On)) \to \exists u \in ({ran F}^{C}) \exists v \in ({ran F}^{D}) (u \underset{˙}{+} v = F \land dom u = C \land dom v = D)$

Metamath Proof Explorer

Theorem tfsconcatrev

Proof