nosupbnd1lem1

Description: Lemma for nosupbnd1 . Establish a soft upper bound. (Contributed by Scott Fenton, 5-Dec-2021)

		Ref	Expression
	Hypothesis	nosupbnd1.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	nosupbnd1lem1	$⊢ (\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) \to \neg S <_{s} ({U ↾}_{dom S})$

Proof

Step	Hyp	Ref	Expression
1		nosupbnd1.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		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) \to A \subseteq No$
3		simp3	$⊢ (\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) \to U \in A$
4	2 3	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) \to U \in No$
5	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
6	5	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) \to S \in No$
7		nodmon	$⊢ S \in No \to dom S \in On$
8	6 7	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) \to dom S \in On$
9		noreson	$⊢ (U \in No \land dom S \in On) \to {U ↾}_{dom S} \in No$
10	4 8 9	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) \to {U ↾}_{dom S} \in No$
11		dmres	$⊢ dom ({U ↾}_{dom S}) = dom S \cap dom U$
12		inss1	$⊢ dom S \cap dom U \subseteq dom S$
13	11 12	eqsstri	$⊢ dom ({U ↾}_{dom S}) \subseteq dom S$
14	13	a1i	$⊢ (\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) \to dom ({U ↾}_{dom S}) \subseteq dom S$
15		ssidd	$⊢ (\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) \to dom S \subseteq dom S$
16		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)))$
17	1 16	eqtrid	$⊢ \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)))$
18	17	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)))$
19		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$
20		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)))$
21	19 20	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}))\}$
22	18 21	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}))\}$
23	22	eleq2d	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to (h \in dom S \leftrightarrow h \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}))\})$
24		vex	$⊢ h \in V$
25		eleq1w	$⊢ y = h \to (y \in dom u \leftrightarrow h \in dom u)$
26		suceq	$⊢ y = h \to suc y = suc h$
27	26	reseq2d	$⊢ y = h \to {u ↾}_{suc y} = {u ↾}_{suc h}$
28	26	reseq2d	$⊢ y = h \to {v ↾}_{suc y} = {v ↾}_{suc h}$
29	27 28	eqeq12d	$⊢ y = h \to ({u ↾}_{suc y} = {v ↾}_{suc y} \leftrightarrow {u ↾}_{suc h} = {v ↾}_{suc h})$
30	29	imbi2d	$⊢ y = h \to ((\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}) \leftrightarrow (\neg v <_{s} u \to {u ↾}_{suc h} = {v ↾}_{suc h}))$
31	30	ralbidv	$⊢ y = h \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 h} = {v ↾}_{suc h}))$
32	25 31	anbi12d	$⊢ y = h \to ((y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y})) \leftrightarrow (h \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc h} = {v ↾}_{suc h})))$
33	32	rexbidv	$⊢ y = h \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 (h \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc h} = {v ↾}_{suc h})))$
34		dmeq	$⊢ u = p \to dom u = dom p$
35	34	eleq2d	$⊢ u = p \to (h \in dom u \leftrightarrow h \in dom p)$
36		breq2	$⊢ u = p \to (v <_{s} u \leftrightarrow v <_{s} p)$
37	36	notbid	$⊢ u = p \to (\neg v <_{s} u \leftrightarrow \neg v <_{s} p)$
38		reseq1	$⊢ u = p \to {u ↾}_{suc h} = {p ↾}_{suc h}$
39	38	eqeq1d	$⊢ u = p \to ({u ↾}_{suc h} = {v ↾}_{suc h} \leftrightarrow {p ↾}_{suc h} = {v ↾}_{suc h})$
40	37 39	imbi12d	$⊢ u = p \to ((\neg v <_{s} u \to {u ↾}_{suc h} = {v ↾}_{suc h}) \leftrightarrow (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h}))$
41	40	ralbidv	$⊢ u = p \to (\forall v \in A (\neg v <_{s} u \to {u ↾}_{suc h} = {v ↾}_{suc h}) \leftrightarrow \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h}))$
42	35 41	anbi12d	$⊢ u = p \to ((h \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc h} = {v ↾}_{suc h})) \leftrightarrow (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))$
43	42	cbvrexvw	$⊢ \exists u \in A (h \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc h} = {v ↾}_{suc h})) \leftrightarrow \exists p \in A (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h}))$
44	33 43	bitrdi	$⊢ y = h \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 p \in A (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))$
45	24 44	elab	$⊢ h \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 p \in A (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h}))$
46	23 45	bitrdi	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to (h \in dom S \leftrightarrow \exists p \in A (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))$
47	46	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) \to (h \in dom S \leftrightarrow \exists p \in A (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))$
48		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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
49		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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (A \subseteq No \land A \in V)$
50		simprl	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to p \in A$
51		simprrl	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to h \in dom p$
52		simprrr	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})$
53	1	nosupres	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (p \in A \land h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h}))) \to {S ↾}_{suc h} = {p ↾}_{suc h}$
54	48 49 50 51 52 53	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to {S ↾}_{suc h} = {p ↾}_{suc h}$
55		simpl2l	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to A \subseteq No$
56	55 50	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to p \in No$
57	4	adantr	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to U \in No$
58		ltsso	$⊢ <_{s} Or No$
59		soasym	$⊢ (<_{s} Or No \land (p \in No \land U \in No)) \to (p <_{s} U \to \neg U <_{s} p)$
60	58 59	mpan	$⊢ (p \in No \land U \in No) \to (p <_{s} U \to \neg U <_{s} p)$
61	56 57 60	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (p <_{s} U \to \neg U <_{s} p)$
62		simpl3	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to U \in A$
63		breq1	$⊢ v = U \to (v <_{s} p \leftrightarrow U <_{s} p)$
64	63	notbid	$⊢ v = U \to (\neg v <_{s} p \leftrightarrow \neg U <_{s} p)$
65		reseq1	$⊢ v = U \to {v ↾}_{suc h} = {U ↾}_{suc h}$
66	65	eqeq2d	$⊢ v = U \to ({p ↾}_{suc h} = {v ↾}_{suc h} \leftrightarrow {p ↾}_{suc h} = {U ↾}_{suc h})$
67	64 66	imbi12d	$⊢ v = U \to ((\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h}) \leftrightarrow (\neg U <_{s} p \to {p ↾}_{suc h} = {U ↾}_{suc h}))$
68	67	rspcv	$⊢ U \in A \to (\forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h}) \to (\neg U <_{s} p \to {p ↾}_{suc h} = {U ↾}_{suc h}))$
69	62 52 68	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (\neg U <_{s} p \to {p ↾}_{suc h} = {U ↾}_{suc h})$
70	61 69	syld	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (p <_{s} U \to {p ↾}_{suc h} = {U ↾}_{suc h})$
71	70	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \land p <_{s} U) \to {p ↾}_{suc h} = {U ↾}_{suc h}$
72		nodmon	$⊢ p \in No \to dom p \in On$
73	56 72	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to dom p \in On$
74		onelon	$⊢ (dom p \in On \land h \in dom p) \to h \in On$
75	73 51 74	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to h \in On$
76		onsucb	$⊢ h \in On \leftrightarrow suc h \in On$
77	75 76	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to suc h \in On$
78		noreson	$⊢ (U \in No \land suc h \in On) \to {U ↾}_{suc h} \in No$
79	57 77 78	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to {U ↾}_{suc h} \in No$
80		sonr	$⊢ (<_{s} Or No \land {U ↾}_{suc h} \in No) \to \neg ({U ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
81	58 80	mpan	$⊢ {U ↾}_{suc h} \in No \to \neg ({U ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
82	79 81	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to \neg ({U ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
83	82	adantr	$⊢ (((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \land p <_{s} U) \to \neg ({U ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
84	71 83	eqnbrtrd	$⊢ (((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \land p <_{s} U) \to \neg ({p ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
85	84	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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (p <_{s} U \to \neg ({p ↾}_{suc h}) <_{s} ({U ↾}_{suc h}))$
86		ltsres	$⊢ (p \in No \land U \in No \land suc h \in On) \to (({p ↾}_{suc h}) <_{s} ({U ↾}_{suc h}) \to p <_{s} U)$
87	56 57 77 86	syl3anc	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (({p ↾}_{suc h}) <_{s} ({U ↾}_{suc h}) \to p <_{s} U)$
88	87	con3d	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (\neg p <_{s} U \to \neg ({p ↾}_{suc h}) <_{s} ({U ↾}_{suc h}))$
89	85 88	pm2.61d	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to \neg ({p ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
90	54 89	eqnbrtrd	$⊢ ((\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 (p \in A \land (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to \neg ({S ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
91	90	rexlimdvaa	$⊢ (\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) \to (\exists p \in A (h \in dom p \land \forall v \in A (\neg v <_{s} p \to {p ↾}_{suc h} = {v ↾}_{suc h})) \to \neg ({S ↾}_{suc h}) <_{s} ({U ↾}_{suc h}))$
92	47 91	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) \to (h \in dom S \to \neg ({S ↾}_{suc h}) <_{s} ({U ↾}_{suc h}))$
93	92	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 h \in dom S) \to \neg ({S ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
94		nodmord	$⊢ S \in No \to Ord dom S$
95		ordsucss	$⊢ Ord dom S \to (h \in dom S \to suc h \subseteq dom S)$
96	6 94 95	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) \to (h \in dom S \to suc h \subseteq dom S)$
97	96	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 h \in dom S) \to suc h \subseteq dom S$
98	97	resabs1d	$⊢ ((\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 h \in dom S) \to {({U ↾}_{dom S}) ↾}_{suc h} = {U ↾}_{suc h}$
99	98	breq2d	$⊢ ((\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 h \in dom S) \to (({S ↾}_{suc h}) <_{s} ({({U ↾}_{dom S}) ↾}_{suc h}) \leftrightarrow ({S ↾}_{suc h}) <_{s} ({U ↾}_{suc h}))$
100	93 99	mtbird	$⊢ ((\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 h \in dom S) \to \neg ({S ↾}_{suc h}) <_{s} ({({U ↾}_{dom S}) ↾}_{suc h})$
101	100	ralrimiva	$⊢ (\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) \to \forall h \in dom S \neg ({S ↾}_{suc h}) <_{s} ({({U ↾}_{dom S}) ↾}_{suc h})$
102		noresle	$⊢ (({U ↾}_{dom S} \in No \land S \in No) \land (dom ({U ↾}_{dom S}) \subseteq dom S \land dom S \subseteq dom S \land \forall h \in dom S \neg ({S ↾}_{suc h}) <_{s} ({({U ↾}_{dom S}) ↾}_{suc h}))) \to \neg S <_{s} ({U ↾}_{dom S})$
103	10 6 14 15 101 102	syl23anc	$⊢ (\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) \to \neg S <_{s} ({U ↾}_{dom S})$

Metamath Proof Explorer

Theorem nosupbnd1lem1

Proof