nosupres

Description: A restriction law for surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021)

		Ref	Expression
	Hypothesis	nosupres.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	nosupres	$⊢ (\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 ↾}_{suc G} = {U ↾}_{suc G}$

Proof

Step	Hyp	Ref	Expression
1		nosupres.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		dmres	$⊢ dom ({S ↾}_{suc G}) = suc G \cap dom S$
3	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
4	3	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 S \in No$
5		nodmord	$⊢ S \in No \to Ord dom S$
6	4 5	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 Ord dom S$
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		eleq1	$⊢ y = G \to (y \in dom u \leftrightarrow G \in dom u)$
30		suceq	$⊢ y = G \to suc y = suc G$
31	30	reseq2d	$⊢ y = G \to {u ↾}_{suc y} = {u ↾}_{suc G}$
32	30	reseq2d	$⊢ y = G \to {v ↾}_{suc y} = {v ↾}_{suc G}$
33	31 32	eqeq12d	$⊢ y = G \to ({u ↾}_{suc y} = {v ↾}_{suc y} \leftrightarrow {u ↾}_{suc G} = {v ↾}_{suc G})$
34	33	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}))$
35	34	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}))$
36	29 35	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})))$
37	36	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})))$
38	37	elabg	$⊢ G \in dom U \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}))\} \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	38	3ad2ant2	$⊢ (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}))\} \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})))$
40	28 39	mpbird	$⊢ (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}))\}$
41	40	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 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}))\}$
42		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)))$
43	1 42	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)))$
44	43	dmeqd	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = dom (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)))$
45		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$
46		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)))$
47	45 46	dmmpti	$⊢ dom (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))) = \{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}))\}$
48	44 47	eqtrdi	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = \{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}))\}$
49	48	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 dom S = \{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}))\}$
50	41 49	eleqtrrd	$⊢ (\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 S$
51		ordsucss	$⊢ Ord dom S \to (G \in dom S \to suc G \subseteq dom S)$
52	6 50 51	sylc	$⊢ (\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 suc G \subseteq dom S$
53		df-ss	$⊢ suc G \subseteq dom S \leftrightarrow suc G \cap dom S = suc G$
54	52 53	sylib	$⊢ (\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 suc G \cap dom S = suc G$
55	2 54	syl5eq	$⊢ (\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 dom ({S ↾}_{suc G}) = suc G$
56		dmres	$⊢ dom ({U ↾}_{suc G}) = suc G \cap dom U$
57		simp2l	$⊢ (\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 A \subseteq No$
58		simp31	$⊢ (\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 U \in A$
59	57 58	sseldd	$⊢ (\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 U \in No$
60		nodmord	$⊢ U \in No \to Ord dom U$
61	59 60	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 Ord dom U$
62		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$
63		ordsucss	$⊢ Ord dom U \to (G \in dom U \to suc G \subseteq dom U)$
64	61 62 63	sylc	$⊢ (\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 suc G \subseteq dom U$
65		df-ss	$⊢ suc G \subseteq dom U \leftrightarrow suc G \cap dom U = suc G$
66	64 65	sylib	$⊢ (\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 suc G \cap dom U = suc G$
67	56 66	syl5eq	$⊢ (\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 dom ({U ↾}_{suc G}) = suc G$
68	55 67	eqtr4d	$⊢ (\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 dom ({S ↾}_{suc G}) = dom ({U ↾}_{suc G})$
69	55	eleq2d	$⊢ (\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 (a \in dom ({S ↾}_{suc G}) \leftrightarrow a \in suc G)$
70		simpl1	$⊢ ((\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}))) \land a \in suc G) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
71		simpl2	$⊢ ((\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}))) \land a \in suc G) \to (A \subseteq No \land A \in V)$
72		simpl31	$⊢ ((\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}))) \land a \in suc G) \to U \in A$
73	64	sselda	$⊢ ((\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}))) \land a \in suc G) \to a \in dom U$
74		nodmon	$⊢ U \in No \to dom U \in On$
75	59 74	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 dom U \in On$
76		onelon	$⊢ (dom U \in On \land G \in dom U) \to G \in On$
77	75 62 76	syl2anc	$⊢ (\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 On$
78		eloni	$⊢ G \in On \to Ord G$
79	77 78	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 Ord G$
80		ordsuc	$⊢ Ord G \leftrightarrow Ord suc G$
81	79 80	sylib	$⊢ (\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 Ord suc G$
82		ordsucss	$⊢ Ord suc G \to (a \in suc G \to suc a \subseteq suc G)$
83	81 82	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 (a \in suc G \to suc a \subseteq suc G)$
84	83	imp	$⊢ ((\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}))) \land a \in suc G) \to suc a \subseteq suc G$
85		simpl33	$⊢ ((\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}))) \land a \in suc G) \to \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G})$
86		reseq1	$⊢ {U ↾}_{suc G} = {v ↾}_{suc G} \to {({U ↾}_{suc G}) ↾}_{suc a} = {({v ↾}_{suc G}) ↾}_{suc a}$
87		resabs1	$⊢ suc a \subseteq suc G \to {({U ↾}_{suc G}) ↾}_{suc a} = {U ↾}_{suc a}$
88		resabs1	$⊢ suc a \subseteq suc G \to {({v ↾}_{suc G}) ↾}_{suc a} = {v ↾}_{suc a}$
89	87 88	eqeq12d	$⊢ suc a \subseteq suc G \to ({({U ↾}_{suc G}) ↾}_{suc a} = {({v ↾}_{suc G}) ↾}_{suc a} \leftrightarrow {U ↾}_{suc a} = {v ↾}_{suc a})$
90	86 89	syl5ib	$⊢ suc a \subseteq suc G \to ({U ↾}_{suc G} = {v ↾}_{suc G} \to {U ↾}_{suc a} = {v ↾}_{suc a})$
91	90	imim2d	$⊢ suc a \subseteq suc G \to ((\neg v <_{s} U \to {U ↾}_{suc G} = {v ↾}_{suc G}) \to (\neg v <_{s} U \to {U ↾}_{suc a} = {v ↾}_{suc a}))$
92	91	ralimdv	$⊢ suc a \subseteq suc G \to (\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 a} = {v ↾}_{suc a}))$
93	84 85 92	sylc	$⊢ ((\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}))) \land a \in suc G) \to \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc a} = {v ↾}_{suc a})$
94	1	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 a \in dom U \land \forall v \in A (\neg v <_{s} U \to {U ↾}_{suc a} = {v ↾}_{suc a}))) \to S (a) = U (a)$
95	70 71 72 73 93 94	syl113anc	$⊢ ((\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}))) \land a \in suc G) \to S (a) = U (a)$
96		simpr	$⊢ ((\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}))) \land a \in suc G) \to a \in suc G$
97	96	fvresd	$⊢ ((\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}))) \land a \in suc G) \to ({S ↾}_{suc G}) (a) = S (a)$
98	96	fvresd	$⊢ ((\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}))) \land a \in suc G) \to ({U ↾}_{suc G}) (a) = U (a)$
99	95 97 98	3eqtr4d	$⊢ ((\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}))) \land a \in suc G) \to ({S ↾}_{suc G}) (a) = ({U ↾}_{suc G}) (a)$
100	99	ex	$⊢ (\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 (a \in suc G \to ({S ↾}_{suc G}) (a) = ({U ↾}_{suc G}) (a))$
101	69 100	sylbid	$⊢ (\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 (a \in dom ({S ↾}_{suc G}) \to ({S ↾}_{suc G}) (a) = ({U ↾}_{suc G}) (a))$
102	101	ralrimiv	$⊢ (\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 \forall a \in dom ({S ↾}_{suc G}) ({S ↾}_{suc G}) (a) = ({U ↾}_{suc G}) (a)$
103		nofun	$⊢ S \in No \to Fun S$
104		funres	$⊢ Fun S \to Fun ({S ↾}_{suc G})$
105	4 103 104	3syl	$⊢ (\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 Fun ({S ↾}_{suc G})$
106		nofun	$⊢ U \in No \to Fun U$
107		funres	$⊢ Fun U \to Fun ({U ↾}_{suc G})$
108	59 106 107	3syl	$⊢ (\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 Fun ({U ↾}_{suc G})$
109		eqfunfv	$⊢ (Fun ({S ↾}_{suc G}) \land Fun ({U ↾}_{suc G})) \to ({S ↾}_{suc G} = {U ↾}_{suc G} \leftrightarrow (dom ({S ↾}_{suc G}) = dom ({U ↾}_{suc G}) \land \forall a \in dom ({S ↾}_{suc G}) ({S ↾}_{suc G}) (a) = ({U ↾}_{suc G}) (a)))$
110	105 108 109	syl2anc	$⊢ (\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 ↾}_{suc G} = {U ↾}_{suc G} \leftrightarrow (dom ({S ↾}_{suc G}) = dom ({U ↾}_{suc G}) \land \forall a \in dom ({S ↾}_{suc G}) ({S ↾}_{suc G}) (a) = ({U ↾}_{suc G}) (a)))$
111	68 102 110	mpbir2and	$⊢ (\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 ↾}_{suc G} = {U ↾}_{suc G}$

Metamath Proof Explorer

Theorem nosupres

Proof