nosupbnd1lem6

Description: Lemma for nosupbnd1 . Establish a hard upper bound when there is no maximum. (Contributed by Scott Fenton, 6-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	nosupbnd1lem6	$⊢ (\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}) <_{s} 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		nofv	$⊢ U \in No \to (U (dom S) = \emptyset \lor U (dom S) = 1_{𝑜} \lor U (dom S) = 2_{𝑜})$
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) \to (U (dom S) = \emptyset \lor U (dom S) = 1_{𝑜} \lor U (dom S) = 2_{𝑜})$
7		3oran	$⊢ (U (dom S) = \emptyset \lor U (dom S) = 1_{𝑜} \lor U (dom S) = 2_{𝑜}) \leftrightarrow \neg (\neg U (dom S) = \emptyset \land \neg U (dom S) = 1_{𝑜} \land \neg U (dom S) = 2_{𝑜})$
8	6 7	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) \to \neg (\neg U (dom S) = \emptyset \land \neg U (dom S) = 1_{𝑜} \land \neg U (dom S) = 2_{𝑜})$
9		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 {U ↾}_{dom S} = S) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
10		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 {U ↾}_{dom S} = S) \to (A \subseteq No \land A \in V)$
11		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 {U ↾}_{dom S} = S) \to U \in A$
12		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 {U ↾}_{dom S} = S) \to {U ↾}_{dom S} = S$
13	1	nosupbnd1lem4	$⊢ (\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 {U ↾}_{dom S} = S)) \to U (dom S) \neq \emptyset$
14	9 10 11 12 13	syl112anc	$⊢ ((\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 {U ↾}_{dom S} = S) \to U (dom S) \neq \emptyset$
15	14	neneqd	$⊢ ((\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 {U ↾}_{dom S} = S) \to \neg U (dom S) = \emptyset$
16	1	nosupbnd1lem5	$⊢ (\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 {U ↾}_{dom S} = S)) \to U (dom S) \neq 1_{𝑜}$
17	9 10 11 12 16	syl112anc	$⊢ ((\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 {U ↾}_{dom S} = S) \to U (dom S) \neq 1_{𝑜}$
18	17	neneqd	$⊢ ((\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 {U ↾}_{dom S} = S) \to \neg U (dom S) = 1_{𝑜}$
19	1	nosupbnd1lem3	$⊢ (\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 {U ↾}_{dom S} = S)) \to U (dom S) \neq 2_{𝑜}$
20	9 10 11 12 19	syl112anc	$⊢ ((\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 {U ↾}_{dom S} = S) \to U (dom S) \neq 2_{𝑜}$
21	20	neneqd	$⊢ ((\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 {U ↾}_{dom S} = S) \to \neg U (dom S) = 2_{𝑜}$
22	15 18 21	3jca	$⊢ ((\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 {U ↾}_{dom S} = S) \to (\neg U (dom S) = \emptyset \land \neg U (dom S) = 1_{𝑜} \land \neg U (dom S) = 2_{𝑜})$
23	8 22	mtand	$⊢ (\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 {U ↾}_{dom S} = S$
24	1	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})$
25	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
26	25	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$
27		nodmon	$⊢ S \in No \to dom S \in On$
28	26 27	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$
29		noreson	$⊢ (U \in No \land dom S \in On) \to {U ↾}_{dom S} \in No$
30	4 28 29	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$
31		sltso	$⊢ <_{s} Or No$
32		solin	$⊢ (<_{s} Or No \land ({U ↾}_{dom S} \in No \land S \in No)) \to (({U ↾}_{dom S}) <_{s} S \lor {U ↾}_{dom S} = S \lor S <_{s} ({U ↾}_{dom S}))$
33	31 32	mpan	$⊢ ({U ↾}_{dom S} \in No \land S \in No) \to (({U ↾}_{dom S}) <_{s} S \lor {U ↾}_{dom S} = S \lor S <_{s} ({U ↾}_{dom S}))$
34	30 26 33	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}) <_{s} S \lor {U ↾}_{dom S} = S \lor S <_{s} ({U ↾}_{dom S}))$
35	23 24 34	ecase23d	$⊢ (\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}) <_{s} S$

Metamath Proof Explorer

Theorem nosupbnd1lem6

Proof