tfsconcatlem

		Ref	Expression
	Assertion	tfsconcatlem	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists! x \exists y \in B (C = A +_{𝑜} y \land x = F (y))$

Proof

Step	Hyp	Ref	Expression
1		onss	$⊢ B \in On \to B \subseteq On$
2	1	3ad2ant2	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to B \subseteq On$
3		oacl	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B \in On$
4		eloni	$⊢ A +_{𝑜} B \in On \to Ord (A +_{𝑜} B)$
5	3 4	syl	$⊢ (A \in On \land B \in On) \to Ord (A +_{𝑜} B)$
6		eloni	$⊢ A \in On \to Ord A$
7	6	adantr	$⊢ (A \in On \land B \in On) \to Ord A$
8		ordeldif	$⊢ (Ord (A +_{𝑜} B) \land Ord A) \to (C \in ((A +_{𝑜} B) ∖ A) \leftrightarrow (C \in (A +_{𝑜} B) \land A \subseteq C))$
9	5 7 8	syl2anc	$⊢ (A \in On \land B \in On) \to (C \in ((A +_{𝑜} B) ∖ A) \leftrightarrow (C \in (A +_{𝑜} B) \land A \subseteq C))$
10	9	biimpa	$⊢ ((A \in On \land B \in On) \land C \in ((A +_{𝑜} B) ∖ A)) \to (C \in (A +_{𝑜} B) \land A \subseteq C)$
11	10	ancomd	$⊢ ((A \in On \land B \in On) \land C \in ((A +_{𝑜} B) ∖ A)) \to (A \subseteq C \land C \in (A +_{𝑜} B))$
12	11	ex	$⊢ (A \in On \land B \in On) \to (C \in ((A +_{𝑜} B) ∖ A) \to (A \subseteq C \land C \in (A +_{𝑜} B)))$
13	12	imdistani	$⊢ ((A \in On \land B \in On) \land C \in ((A +_{𝑜} B) ∖ A)) \to ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B)))$
14	13	3impa	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B)))$
15		oawordex2	$⊢ ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \to \exists y \in B A +_{𝑜} y = C$
16	14 15	syl	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists y \in B A +_{𝑜} y = C$
17		simp1	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to A \in On$
18		onss	$⊢ A +_{𝑜} B \in On \to A +_{𝑜} B \subseteq On$
19	3 18	syl	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B \subseteq On$
20	19	ssdifd	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B) ∖ A \subseteq On ∖ A$
21	20	sselda	$⊢ ((A \in On \land B \in On) \land C \in ((A +_{𝑜} B) ∖ A)) \to C \in (On ∖ A)$
22	21	3impa	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to C \in (On ∖ A)$
23		ordon	$⊢ Ord On$
24	17 6	syl	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to Ord A$
25		ordeldif	$⊢ (Ord On \land Ord A) \to (C \in (On ∖ A) \leftrightarrow (C \in On \land A \subseteq C))$
26	23 24 25	sylancr	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to (C \in (On ∖ A) \leftrightarrow (C \in On \land A \subseteq C))$
27	22 26	mpbid	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to (C \in On \land A \subseteq C)$
28		anass	$⊢ ((A \in On \land C \in On) \land A \subseteq C) \leftrightarrow (A \in On \land (C \in On \land A \subseteq C))$
29	17 27 28	sylanbrc	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to ((A \in On \land C \in On) \land A \subseteq C)$
30		oawordeu	$⊢ ((A \in On \land C \in On) \land A \subseteq C) \to \exists! y \in On A +_{𝑜} y = C$
31	29 30	syl	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists! y \in On A +_{𝑜} y = C$
32		reuss	$⊢ (B \subseteq On \land \exists y \in B A +_{𝑜} y = C \land \exists! y \in On A +_{𝑜} y = C) \to \exists! y \in B A +_{𝑜} y = C$
33	2 16 31 32	syl3anc	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists! y \in B A +_{𝑜} y = C$
34		reurmo	$⊢ \exists! y \in B A +_{𝑜} y = C \to \exists^{*} y \in B A +_{𝑜} y = C$
35	33 34	syl	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists^{*} y \in B A +_{𝑜} y = C$
36		df-rmo	$⊢ \exists^{} y \in B A +_{𝑜} y = C \leftrightarrow \exists^{} y (y \in B \land A +_{𝑜} y = C)$
37	35 36	sylib	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists^{*} y (y \in B \land A +_{𝑜} y = C)$
38		moeq	$⊢ \exists^{*} x x = F (y)$
39	38	ax-gen	$⊢ \forall y \exists^{*} x x = F (y)$
40		moexexvw	$⊢ (\exists^{} y (y \in B \land A +_{𝑜} y = C) \land \forall y \exists^{} x x = F (y)) \to \exists^{*} x \exists y ((y \in B \land A +_{𝑜} y = C) \land x = F (y))$
41	37 39 40	sylancl	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists^{*} x \exists y ((y \in B \land A +_{𝑜} y = C) \land x = F (y))$
42		df-rex	$⊢ \exists y \in B (A +_{𝑜} y = C \land x = F (y)) \leftrightarrow \exists y (y \in B \land (A +_{𝑜} y = C \land x = F (y)))$
43		anass	$⊢ ((y \in B \land A +_{𝑜} y = C) \land x = F (y)) \leftrightarrow (y \in B \land (A +_{𝑜} y = C \land x = F (y)))$
44	43	exbii	$⊢ \exists y ((y \in B \land A +_{𝑜} y = C) \land x = F (y)) \leftrightarrow \exists y (y \in B \land (A +_{𝑜} y = C \land x = F (y)))$
45	42 44	bitr4i	$⊢ \exists y \in B (A +_{𝑜} y = C \land x = F (y)) \leftrightarrow \exists y ((y \in B \land A +_{𝑜} y = C) \land x = F (y))$
46	45	mobii	$⊢ \exists^{} x \exists y \in B (A +_{𝑜} y = C \land x = F (y)) \leftrightarrow \exists^{} x \exists y ((y \in B \land A +_{𝑜} y = C) \land x = F (y))$
47	41 46	sylibr	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists^{*} x \exists y \in B (A +_{𝑜} y = C \land x = F (y))$
48		fvex	$⊢ F (y) \in V$
49	48	isseti	$⊢ \exists x x = F (y)$
50	49	jctr	$⊢ A +_{𝑜} y = C \to (A +_{𝑜} y = C \land \exists x x = F (y))$
51	50	a1i	$⊢ ((A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \land y \in B) \to (A +_{𝑜} y = C \to (A +_{𝑜} y = C \land \exists x x = F (y)))$
52	51	reximdva	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to (\exists y \in B A +_{𝑜} y = C \to \exists y \in B (A +_{𝑜} y = C \land \exists x x = F (y)))$
53	16 52	mpd	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists y \in B (A +_{𝑜} y = C \land \exists x x = F (y))$
54		rexcom4a	$⊢ \exists x \exists y \in B (A +_{𝑜} y = C \land x = F (y)) \leftrightarrow \exists y \in B (A +_{𝑜} y = C \land \exists x x = F (y))$
55		exmoeu	$⊢ \exists x \exists y \in B (A +_{𝑜} y = C \land x = F (y)) \leftrightarrow (\exists^{*} x \exists y \in B (A +_{𝑜} y = C \land x = F (y)) \to \exists! x \exists y \in B (A +_{𝑜} y = C \land x = F (y)))$
56	54 55	bitr3i	$⊢ \exists y \in B (A +_{𝑜} y = C \land \exists x x = F (y)) \leftrightarrow (\exists^{*} x \exists y \in B (A +_{𝑜} y = C \land x = F (y)) \to \exists! x \exists y \in B (A +_{𝑜} y = C \land x = F (y)))$
57	53 56	sylib	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to (\exists^{*} x \exists y \in B (A +_{𝑜} y = C \land x = F (y)) \to \exists! x \exists y \in B (A +_{𝑜} y = C \land x = F (y)))$
58	47 57	mpd	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists! x \exists y \in B (A +_{𝑜} y = C \land x = F (y))$
59		eqcom	$⊢ A +_{𝑜} y = C \leftrightarrow C = A +_{𝑜} y$
60	59	anbi1i	$⊢ (A +_{𝑜} y = C \land x = F (y)) \leftrightarrow (C = A +_{𝑜} y \land x = F (y))$
61	60	rexbii	$⊢ \exists y \in B (A +_{𝑜} y = C \land x = F (y)) \leftrightarrow \exists y \in B (C = A +_{𝑜} y \land x = F (y))$
62	61	eubii	$⊢ \exists! x \exists y \in B (A +_{𝑜} y = C \land x = F (y)) \leftrightarrow \exists! x \exists y \in B (C = A +_{𝑜} y \land x = F (y))$
63	58 62	sylib	$⊢ (A \in On \land B \in On \land C \in ((A +_{𝑜} B) ∖ A)) \to \exists! x \exists y \in B (C = A +_{𝑜} y \land x = F (y))$

Metamath Proof Explorer

Theorem tfsconcatlem

Proof