nosupfv

Description: The value of surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021)

		Ref	Expression
	Hypothesis	nosupfv.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
	Assertion	nosupfv	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to S (G) = U (G)$

Proof

Step	Hyp	Ref	Expression
1		nosupfv.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
2		iffalse	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))) = (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
3	1 2	syl5eq	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to S = (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
4	3	fveq1d	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to S (G) = (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))) (G)$
5	4	3ad2ant1	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to S (G) = (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))) (G)$
6		simp32	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to G \in dom U$
7		dmeq	$⊢ p = U \to dom p = dom U$
8	7	eleq2d	$⊢ p = U \to (G \in dom p \leftrightarrow G \in dom U)$
9		breq2	$⊢ p = U \to (v <_{s} p \leftrightarrow v <_{s} U)$
10	9	notbid	$⊢ p = U \to (\neg v <_{s} p \leftrightarrow \neg v <_{s} U)$
11		reseq1	$⊢ p = U \to {p ↾}_{suc G} = {U ↾}_{suc G}$
12	11	eqeq1d	$⊢ p = U \to ({p ↾}_{suc G} = {v ↾}_{suc G} \leftrightarrow {U ↾}_{suc G} = {v ↾}_{suc G})$
13	10 12	imbi12d	$⊢ p = U \to ((\neg v <_{s} p \to {p ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))$
14	13	ralbidv	$⊢ p = U \to (\forall v \in A (\neg v <_{s} p \to {p ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))$
15	8 14	anbi12d	$⊢ p = U \to ((G \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc G} = {v ↾}_{suc G})) \leftrightarrow (G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})))$
16	15	rspcev	$⊢ (U \in A \land (G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists p \in A (G \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc G} = {v ↾}_{suc G}))$
17	16	3impb	$⊢ (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to \exists p \in A (G \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc G} = {v ↾}_{suc G}))$
18		dmeq	$⊢ u = p \to dom u = dom p$
19	18	eleq2d	$⊢ u = p \to (G \in dom u \leftrightarrow G \in dom p)$
20		breq2	$⊢ u = p \to (v <_{s} u \leftrightarrow v <_{s} p)$
21	20	notbid	$⊢ u = p \to (\neg v <_{s} u \leftrightarrow \neg v <_{s} p)$
22		reseq1	$⊢ u = p \to {u ↾}_{suc G} = {p ↾}_{suc G}$
23	22	eqeq1d	$⊢ u = p \to ({u ↾}_{suc G} = {v ↾}_{suc G} \leftrightarrow {p ↾}_{suc G} = {v ↾}_{suc G})$
24	21 23	imbi12d	$⊢ u = p \to ((\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow (\neg v <_{s} p \to {p ↾}_{suc G} = {v ↾}_{suc G}))$
25	24	ralbidv	$⊢ u = p \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc G} = {v ↾}_{suc G}))$
26	19 25	anbi12d	$⊢ u = p \to ((G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G})) \leftrightarrow (G \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc G} = {v ↾}_{suc G})))$
27	26	cbvrexvw	$⊢ \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G})) \leftrightarrow \exists p \in A (G \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc G} = {v ↾}_{suc G}))$
28	17 27	sylibr	$⊢ (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
29	28	3ad2ant3	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
30		eleq1	$⊢ y = G \to (y \in dom u \leftrightarrow G \in dom u)$
31		suceq	$⊢ y = G \to suc y = suc G$
32	31	reseq2d	$⊢ y = G \to {u ↾}_{suc y} = {u ↾}_{suc G}$
33	31	reseq2d	$⊢ y = G \to {v ↾}_{suc y} = {v ↾}_{suc G}$
34	32 33	eqeq12d	$⊢ y = G \to ({u ↾}_{suc y} = {v ↾}_{suc y} \leftrightarrow {u ↾}_{suc G} = {v ↾}_{suc G})$
35	34	imbi2d	$⊢ y = G \to ((\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
36	35	ralbidv	$⊢ y = G \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
37	30 36	anbi12d	$⊢ y = G \to ((y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G})))$
38	37	rexbidv	$⊢ y = G \to (\exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G})))$
39	6 29 38	elabd	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to G \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\}$
40		eleq1	$⊢ g = G \to (g \in dom u \leftrightarrow G \in dom u)$
41		suceq	$⊢ g = G \to suc g = suc G$
42	41	reseq2d	$⊢ g = G \to {u ↾}_{suc g} = {u ↾}_{suc G}$
43	41	reseq2d	$⊢ g = G \to {v ↾}_{suc g} = {v ↾}_{suc G}$
44	42 43	eqeq12d	$⊢ g = G \to ({u ↾}_{suc g} = {v ↾}_{suc g} \leftrightarrow {u ↾}_{suc G} = {v ↾}_{suc G})$
45	44	imbi2d	$⊢ g = G \to ((\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \leftrightarrow (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
46	45	ralbidv	$⊢ g = G \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \leftrightarrow \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}))$
47		fveqeq2	$⊢ g = G \to (u (g) = x \leftrightarrow u (G) = x)$
48	40 46 47	3anbi123d	$⊢ g = G \to ((g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x) \leftrightarrow (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x))$
49	48	rexbidv	$⊢ g = G \to (\exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \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 v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x))$
50	49	iotabidv	$⊢ g = G \to (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)) = (ι x \| \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x))$
51		eqid	$⊢ (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))) = (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x)))$
52		iotaex	$⊢ (ι x \| \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)) \in V$
53	50 51 52	fvmpt	$⊢ G \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} \to (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))) (G) = (ι x \| \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x))$
54	39 53	syl	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))) (G) = (ι x \| \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x))$
55		simp1	$⊢ (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to U \in A$
56		simp2	$⊢ (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to G \in dom U$
57		simp3	$⊢ (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})$
58		eqidd	$⊢ (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to U (G) = U (G)$
59		dmeq	$⊢ u = U \to dom u = dom U$
60	59	eleq2d	$⊢ u = U \to (G \in dom u \leftrightarrow G \in dom U)$
61		breq2	$⊢ u = U \to (v <_{s} u \leftrightarrow v <_{s} U)$
62	61	notbid	$⊢ u = U \to (\neg v <_{s} u \leftrightarrow \neg v <_{s} U)$
63		reseq1	$⊢ u = U \to {u ↾}_{suc G} = {U ↾}_{suc G}$
64	63	eqeq1d	$⊢ u = U \to ({u ↾}_{suc G} = {v ↾}_{suc G} \leftrightarrow {U ↾}_{suc G} = {v ↾}_{suc G})$
65	62 64	imbi12d	$⊢ u = U \to ((\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))$
66	65	ralbidv	$⊢ u = U \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \leftrightarrow \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))$
67		fveq1	$⊢ u = U \to u (G) = U (G)$
68	67	eqeq1d	$⊢ u = U \to (u (G) = U (G) \leftrightarrow U (G) = U (G))$
69	60 66 68	3anbi123d	$⊢ u = U \to ((G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = U (G)) \leftrightarrow (G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}) \land U (G) = U (G)))$
70	69	rspcev	$⊢ (U \in A \land (G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}) \land U (G) = U (G))) \to \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = U (G))$
71	55 56 57 58 70	syl13anc	$⊢ (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = U (G))$
72	71	3ad2ant3	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = U (G))$
73		fvex	$⊢ U (G) \in V$
74		eqid	$⊢ u (G) = u (G)$
75		fvex	$⊢ u (G) \in V$
76		eqeq2	$⊢ x = u (G) \to (u (G) = x \leftrightarrow u (G) = u (G))$
77	76	3anbi3d	$⊢ x = u (G) \to ((G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = u (G)))$
78	75 77	spcev	$⊢ (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = u (G)) \to \exists x (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
79	74 78	mp3an3	$⊢ (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G})) \to \exists x (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
80	79	reximi	$⊢ \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G})) \to \exists u \in A \exists x (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
81		rexcom4	$⊢ \exists u \in A \exists x (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow \exists x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
82	80 81	sylib	$⊢ \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G})) \to \exists x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
83	28 82	syl	$⊢ (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})) \to \exists x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
84	83	3ad2ant3	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
85		nosupprefixmo	$⊢ A \subseteq No \to \exists^{*} x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
86	85	adantr	$⊢ (A \subseteq No \land A \in V) \to \exists^{*} x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
87	86	3ad2ant2	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists^{*} x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
88		df-eu	$⊢ \exists! x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow (\exists x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \land \exists^{*} x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x))$
89	84 87 88	sylanbrc	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to \exists! x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)$
90		eqeq2	$⊢ x = U (G) \to (u (G) = x \leftrightarrow u (G) = U (G))$
91	90	3anbi3d	$⊢ x = U (G) \to ((G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x) \leftrightarrow (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = U (G)))$
92	91	rexbidv	$⊢ x = U (G) \to (\exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \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 v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = U (G)))$
93	92	iota2	$⊢ (U (G) \in V \land \exists! x \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)) \to (\exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = U (G)) \leftrightarrow (ι x \| \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)) = U (G))$
94	73 89 93	sylancr	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to (\exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = U (G)) \leftrightarrow (ι x \| \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)) = U (G))$
95	72 94	mpbid	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to (ι x \| \exists u \in A (G \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc G} = {v ↾}_{suc G}) \land u (G) = x)) = U (G)$
96	5 54 95	3eqtrd	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (U \in A \land G \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}))) \to S (G) = U (G)$

Metamath Proof Explorer

Theorem nosupfv

Proof