noinfbnd1lem2

Description: Lemma for noinfbnd1 . When there is no minimum, if any member of B is a prolongment of T , then so are all elements below it. (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	noinfbnd1lem2	$⊢ (\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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to {W ↾}_{dom T} = 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		simp3rl	$⊢ (\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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to W \in B$
3	1	noinfbnd1lem1	$⊢ (\neg \exists x \in B \forall y \in B \neg y <_{s} x \land (B \subseteq No \land B \in V) \land W \in B) \to \neg ({W ↾}_{dom T}) <_{s} T$
4	2 3	syld3an3	$⊢ (\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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to \neg ({W ↾}_{dom T}) <_{s} T$
5		simp3rr	$⊢ (\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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to \neg U <_{s} W$
6		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 \land {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to B \subseteq No$
7		simp3ll	$⊢ (\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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to U \in B$
8	6 7	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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to U \in No$
9	6 2	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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to W \in No$
10	1	noinfno	$⊢ (B \subseteq No \land B \in V) \to T \in No$
11	10	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 \land {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to T \in No$
12		nodmon	$⊢ T \in No \to dom T \in On$
13	11 12	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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to dom T \in On$
14		sltres	$⊢ (U \in No \land W \in No \land dom T \in On) \to (({U ↾}_{dom T}) <_{s} ({W ↾}_{dom T}) \to U <_{s} W)$
15	8 9 13 14	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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to (({U ↾}_{dom T}) <_{s} ({W ↾}_{dom T}) \to U <_{s} W)$
16	5 15	mtod	$⊢ (\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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to \neg ({U ↾}_{dom T}) <_{s} ({W ↾}_{dom T})$
17		simp3lr	$⊢ (\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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to {U ↾}_{dom T} = T$
18	17	breq1d	$⊢ (\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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to (({U ↾}_{dom T}) <_{s} ({W ↾}_{dom T}) \leftrightarrow T <_{s} ({W ↾}_{dom T}))$
19	16 18	mtbid	$⊢ (\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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to \neg T <_{s} ({W ↾}_{dom T})$
20		noreson	$⊢ (W \in No \land dom T \in On) \to {W ↾}_{dom T} \in No$
21	9 13 20	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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to {W ↾}_{dom T} \in No$
22		sltso	$⊢ <_{s} Or No$
23		sotrieq2	$⊢ (<_{s} Or No \land ({W ↾}_{dom T} \in No \land T \in No)) \to ({W ↾}_{dom T} = T \leftrightarrow (\neg ({W ↾}_{dom T}) <_{s} T \land \neg T <_{s} ({W ↾}_{dom T})))$
24	22 23	mpan	$⊢ ({W ↾}_{dom T} \in No \land T \in No) \to ({W ↾}_{dom T} = T \leftrightarrow (\neg ({W ↾}_{dom T}) <_{s} T \land \neg T <_{s} ({W ↾}_{dom T})))$
25	21 11 24	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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to ({W ↾}_{dom T} = T \leftrightarrow (\neg ({W ↾}_{dom T}) <_{s} T \land \neg T <_{s} ({W ↾}_{dom T})))$
26	4 19 25	mpbir2and	$⊢ (\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 {U ↾}_{dom T} = T) \land (W \in B \land \neg U <_{s} W))) \to {W ↾}_{dom T} = T$

Metamath Proof Explorer

Theorem noinfbnd1lem2

Proof