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