noinfbnd1lem1

Description: Lemma for noinfbnd1 . Establish a soft lower bound. (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		noinfbnd1.1	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
2	1	noinfno	$⊢ (B \subseteq No \land B \in V) \to T \in No$
3	2	3ad2ant2	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to T \in No$
4		simp2l	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to B \subseteq No$
5		simp3	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to U \in B$
6	4 5	sseldd	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to U \in No$
7		nodmon	$⊢ T \in No \to dom T \in On$
8	3 7	syl	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to dom T \in On$
9		noreson	$⊢ (U \in No \land dom T \in On) \to {U ↾}_{dom T} \in No$
10	6 8 9	syl2anc	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to {U ↾}_{dom T} \in No$
11		ssidd	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to dom T \subseteq dom T$
12		dmres	$⊢ dom ({U ↾}_{dom T}) = dom T \cap dom U$
13		inss1	$⊢ dom T \cap dom U \subseteq dom T$
14	12 13	eqsstri	$⊢ dom ({U ↾}_{dom T}) \subseteq dom T$
15	14	a1i	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to dom ({U ↾}_{dom T}) \subseteq dom T$
16		nodmord	$⊢ T \in No \to Ord dom T$
17	3 16	syl	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to Ord dom T$
18		ordsucss	$⊢ Ord dom T \to (h \in dom T \to suc h \subseteq dom T)$
19	17 18	syl	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to (h \in dom T \to suc h \subseteq dom T)$
20	19	imp	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land h \in dom T) \to suc h \subseteq dom T$
21	20	resabs1d	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land h \in dom T) \to {({U ↾}_{dom T}) ↾}_{suc h} = {U ↾}_{suc h}$
22	1	noinfdm	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to dom T = \{h \| \exists p \in B (h \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc h} = {q ↾}_{suc h}))\}$
23	22	eleq2d	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to (h \in dom T \leftrightarrow h \in \{h \| \exists p \in B (h \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc h} = {q ↾}_{suc h}))\})$
24		abid	$⊢ h \in \{h \| \exists p \in B (h \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc h} = {q ↾}_{suc h}))\} \leftrightarrow \exists p \in B (h \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc h} = {q ↾}_{suc h}))$
25		breq2	$⊢ q = v \to (p <_{s} q \leftrightarrow p <_{s} v)$
26	25	notbid	$⊢ q = v \to (\neg p <_{s} q \leftrightarrow \neg p <_{s} v)$
27		reseq1	$⊢ q = v \to {q ↾}_{suc h} = {v ↾}_{suc h}$
28	27	eqeq2d	$⊢ q = v \to ({p ↾}_{suc h} = {q ↾}_{suc h} \leftrightarrow {p ↾}_{suc h} = {v ↾}_{suc h})$
29	26 28	imbi12d	$⊢ q = v \to ((\neg p <_{s} q \to {p ↾}_{suc h} = {q ↾}_{suc h}) \leftrightarrow (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h}))$
30	29	cbvralvw	$⊢ \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc h} = {q ↾}_{suc h}) \leftrightarrow \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})$
31	30	anbi2i	$⊢ (h \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc h} = {q ↾}_{suc h})) \leftrightarrow (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h}))$
32	31	rexbii	$⊢ \exists p \in B (h \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc h} = {q ↾}_{suc h})) \leftrightarrow \exists p \in B (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h}))$
33	24 32	bitri	$⊢ h \in \{h \| \exists p \in B (h \in dom p \land \forall q \in B (\neg p <_{s} q \to {p ↾}_{suc h} = {q ↾}_{suc h}))\} \leftrightarrow \exists p \in B (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h}))$
34	23 33	bitrdi	$⊢ \neg \exists x \in B \forall y \in B \neg y <_{s} x \to (h \in dom T \leftrightarrow \exists p \in B (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))$
35	34	3ad2ant1	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to (h \in dom T \leftrightarrow \exists p \in B (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))$
36		simpl2l	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to B \subseteq No$
37		simprl	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to p \in B$
38	36 37	sseldd	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to p \in No$
39	6	adantr	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to U \in No$
40		ltsso	$⊢ <_{s} Or No$
41		soasym	$⊢ (<_{s} Or No \land (p \in No \land U \in No)) \to (p <_{s} U \to \neg U <_{s} p)$
42	40 41	mpan	$⊢ (p \in No \land U \in No) \to (p <_{s} U \to \neg U <_{s} p)$
43	38 39 42	syl2anc	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (p <_{s} U \to \neg U <_{s} p)$
44		nodmon	$⊢ p \in No \to dom p \in On$
45	38 44	syl	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to dom p \in On$
46		simprrl	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to h \in dom p$
47		onelon	$⊢ (dom p \in On \land h \in dom p) \to h \in On$
48	45 46 47	syl2anc	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to h \in On$
49		onsucb	$⊢ h \in On \leftrightarrow suc h \in On$
50	48 49	sylib	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to suc h \in On$
51		ltsres	$⊢ (U \in No \land p \in No \land suc h \in On) \to (({U ↾}_{suc h}) <_{s} ({p ↾}_{suc h}) \to U <_{s} p)$
52	39 38 50 51	syl3anc	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (({U ↾}_{suc h}) <_{s} ({p ↾}_{suc h}) \to U <_{s} p)$
53	43 52	nsyld	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (p <_{s} U \to \neg ({U ↾}_{suc h}) <_{s} ({p ↾}_{suc h}))$
54		noreson	$⊢ (U \in No \land suc h \in On) \to {U ↾}_{suc h} \in No$
55	39 50 54	syl2anc	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to {U ↾}_{suc h} \in No$
56		sonr	$⊢ (<_{s} Or No \land {U ↾}_{suc h} \in No) \to \neg ({U ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
57	40 56	mpan	$⊢ {U ↾}_{suc h} \in No \to \neg ({U ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
58	55 57	syl	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to \neg ({U ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
59	58	adantr	$⊢ (((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \land \neg p <_{s} U) \to \neg ({U ↾}_{suc h}) <_{s} ({U ↾}_{suc h})$
60		breq2	$⊢ v = U \to (p <_{s} v \leftrightarrow p <_{s} U)$
61	60	notbid	$⊢ v = U \to (\neg p <_{s} v \leftrightarrow \neg p <_{s} U)$
62		reseq1	$⊢ v = U \to {v ↾}_{suc h} = {U ↾}_{suc h}$
63	62	eqeq2d	$⊢ v = U \to ({p ↾}_{suc h} = {v ↾}_{suc h} \leftrightarrow {p ↾}_{suc h} = {U ↾}_{suc h})$
64	61 63	imbi12d	$⊢ v = U \to ((\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h}) \leftrightarrow (\neg p <_{s} U \to {p ↾}_{suc h} = {U ↾}_{suc h}))$
65		simprrr	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})$
66		simpl3	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to U \in B$
67	64 65 66	rspcdva	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (\neg p <_{s} U \to {p ↾}_{suc h} = {U ↾}_{suc h})$
68	67	imp	$⊢ (((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \land \neg p <_{s} U) \to {p ↾}_{suc h} = {U ↾}_{suc h}$
69	68	breq2d	$⊢ (((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \land \neg p <_{s} U) \to (({U ↾}_{suc h}) <_{s} ({p ↾}_{suc h}) \leftrightarrow ({U ↾}_{suc h}) <_{s} ({U ↾}_{suc h}))$
70	59 69	mtbird	$⊢ (((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \land \neg p <_{s} U) \to \neg ({U ↾}_{suc h}) <_{s} ({p ↾}_{suc h})$
71	70	ex	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (\neg p <_{s} U \to \neg ({U ↾}_{suc h}) <_{s} ({p ↾}_{suc h}))$
72	53 71	pm2.61d	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to \neg ({U ↾}_{suc h}) <_{s} ({p ↾}_{suc h})$
73		simpl1	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to \neg \exists x \in B \forall y \in B \neg y <_{s} x$
74		simpl2	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (B \subseteq No \land B \in V)$
75	1	noinfres	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land (p \in B \land h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h}))) \to {T ↾}_{suc h} = {p ↾}_{suc h}$
76	73 74 37 46 65 75	syl113anc	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to {T ↾}_{suc h} = {p ↾}_{suc h}$
77	76	breq2d	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to (({U ↾}_{suc h}) <_{s} ({T ↾}_{suc h}) \leftrightarrow ({U ↾}_{suc h}) <_{s} ({p ↾}_{suc h}))$
78	72 77	mtbird	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land (p \in B \land (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})))) \to \neg ({U ↾}_{suc h}) <_{s} ({T ↾}_{suc h})$
79	78	rexlimdvaa	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to (\exists p \in B (h \in dom p \land \forall v \in B (\neg p <_{s} v \to {p ↾}_{suc h} = {v ↾}_{suc h})) \to \neg ({U ↾}_{suc h}) <_{s} ({T ↾}_{suc h}))$
80	35 79	sylbid	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to (h \in dom T \to \neg ({U ↾}_{suc h}) <_{s} ({T ↾}_{suc h}))$
81	80	imp	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land h \in dom T) \to \neg ({U ↾}_{suc h}) <_{s} ({T ↾}_{suc h})$
82	21 81	eqnbrtrd	$⊢ ((\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \land h \in dom T) \to \neg ({({U ↾}_{dom T}) ↾}_{suc h}) <_{s} ({T ↾}_{suc h})$
83	82	ralrimiva	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to \forall h \in dom T \neg ({({U ↾}_{dom T}) ↾}_{suc h}) <_{s} ({T ↾}_{suc h})$
84		noresle	$⊢ ((T \in No \land {U ↾}_{dom T} \in No) \land (dom T \subseteq dom T \land dom ({U ↾}_{dom T}) \subseteq dom T \land \forall h \in dom T \neg ({({U ↾}_{dom T}) ↾}_{suc h}) <_{s} ({T ↾}_{suc h}))) \to \neg ({U ↾}_{dom T}) <_{s} T$
85	3 10 11 15 83 84	syl23anc	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land U \in B) \to \neg ({U ↾}_{dom T}) <_{s} T$

Metamath Proof Explorer

Theorem noinfbnd1lem1

Proof