noinfprefixmo

Description: In any class of surreals, there is at most one value of the prefix property. (Contributed by Scott Fenton, 8-Aug-2024)

		Ref	Expression
	Assertion	noinfprefixmo	$⊢ A \subseteq No \to \exists^{*} x \exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$

Proof

Step	Hyp	Ref	Expression
1		reeanv	$⊢ \exists u \in A \exists p \in A ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)) \leftrightarrow (\exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land \exists p \in A (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y))$
2		breq2	$⊢ v = p \to (u <_{s} v \leftrightarrow u <_{s} p)$
3	2	notbid	$⊢ v = p \to (\neg u <_{s} v \leftrightarrow \neg u <_{s} p)$
4		reseq1	$⊢ v = p \to {v ↾}_{suc G} = {p ↾}_{suc G}$
5	4	eqeq2d	$⊢ v = p \to ({u ↾}_{suc G} = {v ↾}_{suc G} \leftrightarrow {u ↾}_{suc G} = {p ↾}_{suc G})$
6	3 5	imbi12d	$⊢ v = p \to ((\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow (\neg u <_{s} p \to {u ↾}_{suc G} = {p ↾}_{suc G}))$
7		simprl2	$⊢ ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y))) \to \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G})$
8	7	adantl	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G})$
9		simprlr	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to p \in A$
10	6 8 9	rspcdva	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to (\neg u <_{s} p \to {u ↾}_{suc G} = {p ↾}_{suc G})$
11		breq2	$⊢ v = u \to (p <_{s} v \leftrightarrow p <_{s} u)$
12	11	notbid	$⊢ v = u \to (\neg p <_{s} v \leftrightarrow \neg p <_{s} u)$
13		reseq1	$⊢ v = u \to {v ↾}_{suc G} = {u ↾}_{suc G}$
14	13	eqeq2d	$⊢ v = u \to ({p ↾}_{suc G} = {v ↾}_{suc G} \leftrightarrow {p ↾}_{suc G} = {u ↾}_{suc G})$
15	12 14	imbi12d	$⊢ v = u \to ((\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow (\neg p <_{s} u \to {p ↾}_{suc G} = {u ↾}_{suc G}))$
16		simprr2	$⊢ ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y))) \to \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G})$
17	16	adantl	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G})$
18		simprll	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to u \in A$
19	15 17 18	rspcdva	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to (\neg p <_{s} u \to {p ↾}_{suc G} = {u ↾}_{suc G})$
20		eqcom	$⊢ {p ↾}_{suc G} = {u ↾}_{suc G} \leftrightarrow {u ↾}_{suc G} = {p ↾}_{suc G}$
21	19 20	syl6ib	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to (\neg p <_{s} u \to {u ↾}_{suc G} = {p ↾}_{suc G})$
22		simpl	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to A \subseteq No$
23	22 18	sseldd	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to u \in No$
24	22 9	sseldd	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to p \in No$
25		sltso	$⊢ <_{s} Or No$
26		soasym	$⊢ (<_{s} Or No \land (u \in No \land p \in No)) \to (u <_{s} p \to \neg p <_{s} u)$
27	25 26	mpan	$⊢ (u \in No \land p \in No) \to (u <_{s} p \to \neg p <_{s} u)$
28	23 24 27	syl2anc	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to (u <_{s} p \to \neg p <_{s} u)$
29		imor	$⊢ (u <_{s} p \to \neg p <_{s} u) \leftrightarrow (\neg u <_{s} p \lor \neg p <_{s} u)$
30	28 29	sylib	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to (\neg u <_{s} p \lor \neg p <_{s} u)$
31	10 21 30	mpjaod	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to {u ↾}_{suc G} = {p ↾}_{suc G}$
32	31	fveq1d	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to ({u ↾}_{suc G}) (G) = ({p ↾}_{suc G}) (G)$
33		simprl1	$⊢ ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y))) \to G \in dom u$
34	33	adantl	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to G \in dom u$
35		sucidg	$⊢ G \in dom u \to G \in suc G$
36	34 35	syl	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to G \in suc G$
37	36	fvresd	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to ({u ↾}_{suc G}) (G) = u (G)$
38	36	fvresd	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to ({p ↾}_{suc G}) (G) = p (G)$
39	32 37 38	3eqtr3d	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to u (G) = p (G)$
40		simprl3	$⊢ ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y))) \to u (G) = x$
41	40	adantl	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to u (G) = x$
42		simprr3	$⊢ ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y))) \to p (G) = y$
43	42	adantl	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to p (G) = y$
44	39 41 43	3eqtr3d	$⊢ (A \subseteq No \land ((u \in A \land p \in A) \land ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)))) \to x = y$
45	44	expr	$⊢ (A \subseteq No \land (u \in A \land p \in A)) \to (((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)) \to x = y)$
46	45	rexlimdvva	$⊢ A \subseteq No \to (\exists u \in A \exists p \in A ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)) \to x = y)$
47	1 46	syl5bir	$⊢ A \subseteq No \to ((\exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land \exists p \in A (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)) \to x = y)$
48	47	alrimivv	$⊢ A \subseteq No \to \forall x \forall y ((\exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land \exists p \in A (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)) \to x = y)$
49		eqeq2	$⊢ x = y \to (u (G) = x \leftrightarrow u (G) = y)$
50	49	3anbi3d	$⊢ x = y \to ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = y))$
51	50	rexbidv	$⊢ x = y \to (\exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow \exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = y))$
52		dmeq	$⊢ u = p \to dom u = dom p$
53	52	eleq2d	$⊢ u = p \to (G \in dom u \leftrightarrow G \in dom p)$
54		breq1	$⊢ u = p \to (u <_{s} v \leftrightarrow p <_{s} v)$
55	54	notbid	$⊢ u = p \to (\neg u <_{s} v \leftrightarrow \neg p <_{s} v)$
56		reseq1	$⊢ u = p \to {u ↾}_{suc G} = {p ↾}_{suc G}$
57	56	eqeq1d	$⊢ u = p \to ({u ↾}_{suc G} = {v ↾}_{suc G} \leftrightarrow {p ↾}_{suc G} = {v ↾}_{suc G})$
58	55 57	imbi12d	$⊢ u = p \to ((\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}))$
59	58	ralbidv	$⊢ u = p \to (\forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}))$
60		fveq1	$⊢ u = p \to u (G) = p (G)$
61	60	eqeq1d	$⊢ u = p \to (u (G) = y \leftrightarrow p (G) = y)$
62	53 59 61	3anbi123d	$⊢ u = p \to ((G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = y) \leftrightarrow (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y))$
63	62	cbvrexvw	$⊢ \exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = y) \leftrightarrow \exists p \in A (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)$
64	51 63	bitrdi	$⊢ x = y \to (\exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow \exists p \in A (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y))$
65	64	mo4	$⊢ \exists^{*} x \exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow \forall x \forall y ((\exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land \exists p \in A (G \in dom p \land \forall v \in A (\neg p <_{s} v \to {p ↾}_{suc G} = {v ↾}_{suc G}) \land p (G) = y)) \to x = y)$
66	48 65	sylibr	$⊢ A \subseteq No \to \exists^{*} x \exists u \in A (G \in dom u \land \forall v \in A (\neg u <_{s} v \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$

Metamath Proof Explorer

Theorem noinfprefixmo

Proof