nosupbnd1lem4

Description: Lemma for nosupbnd1 . If U is a prolongment of S and in A , then ( Udom S ) is not undefined. (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	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$

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		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)) \land (w \in A \land U <_{s} w)) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
3		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)) \land (w \in A \land U <_{s} w)) \to (A \subseteq No \land A \in V)$
4		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 {U ↾}_{dom S} = S)) \land (w \in A \land U <_{s} w)) \to w \in A$
5		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)) \land (w \in A \land U <_{s} w)) \to (U \in A \land {U ↾}_{dom S} = S)$
6		simprr	$⊢ ((\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)) \land (w \in A \land U <_{s} w)) \to U <_{s} w$
7		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 {U ↾}_{dom S} = S)) \to A \subseteq No$
8		simp3l	$⊢ (\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$
9	7 8	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 {U ↾}_{dom S} = S)) \to U \in No$
10		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 {U ↾}_{dom S} = S)) \land (w \in A \land U <_{s} w)) \to A \subseteq No$
11	10 4	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 {U ↾}_{dom S} = S)) \land (w \in A \land U <_{s} w)) \to w \in No$
12		ltsso	$⊢ <_{s} Or No$
13		soasym	$⊢ (<_{s} Or No \land (U \in No \land w \in No)) \to (U <_{s} w \to \neg w <_{s} U)$
14	12 13	mpan	$⊢ (U \in No \land w \in No) \to (U <_{s} w \to \neg w <_{s} U)$
15	9 11 14	syl2an2r	$⊢ ((\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)) \land (w \in A \land U <_{s} w)) \to (U <_{s} w \to \neg w <_{s} U)$
16	6 15	mpd	$⊢ ((\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)) \land (w \in A \land U <_{s} w)) \to \neg w <_{s} U$
17	4 16	jca	$⊢ ((\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)) \land (w \in A \land U <_{s} w)) \to (w \in A \land \neg w <_{s} U)$
18	1	nosupbnd1lem2	$⊢ (\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) \land (w \in A \land \neg w <_{s} U))) \to {w ↾}_{dom S} = S$
19	2 3 5 17 18	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)) \land (w \in A \land U <_{s} w)) \to {w ↾}_{dom S} = S$
20	1	nosupbnd1lem3	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (w \in A \land {w ↾}_{dom S} = S)) \to w (dom S) \neq 2_{𝑜}$
21	2 3 4 19 20	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)) \land (w \in A \land U <_{s} w)) \to w (dom S) \neq 2_{𝑜}$
22	21	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)) \land (w \in A \land U <_{s} w)) \to \neg w (dom S) = 2_{𝑜}$
23	22	expr	$⊢ ((\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)) \land w \in A) \to (U <_{s} w \to \neg w (dom S) = 2_{𝑜})$
24		imnan	$⊢ (U <_{s} w \to \neg w (dom S) = 2_{𝑜}) \leftrightarrow \neg (U <_{s} w \land w (dom S) = 2_{𝑜})$
25	23 24	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 {U ↾}_{dom S} = S)) \land w \in A) \to \neg (U <_{s} w \land w (dom S) = 2_{𝑜})$
26	25	nrexdv	$⊢ (\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 w \in A (U <_{s} w \land w (dom S) = 2_{𝑜})$
27		simpl3l	$⊢ ((\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)) \land U (dom S) = \emptyset) \to U \in A$
28		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)) \land U (dom S) = \emptyset) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
29		breq2	$⊢ w = y \to (u <_{s} w \leftrightarrow u <_{s} y)$
30	29	cbvrexvw	$⊢ \exists w \in A u <_{s} w \leftrightarrow \exists y \in A u <_{s} y$
31		breq1	$⊢ u = x \to (u <_{s} y \leftrightarrow x <_{s} y)$
32	31	rexbidv	$⊢ u = x \to (\exists y \in A u <_{s} y \leftrightarrow \exists y \in A x <_{s} y)$
33	30 32	bitrid	$⊢ u = x \to (\exists w \in A u <_{s} w \leftrightarrow \exists y \in A x <_{s} y)$
34	33	cbvralvw	$⊢ \forall u \in A \exists w \in A u <_{s} w \leftrightarrow \forall x \in A \exists y \in A x <_{s} y$
35		dfrex2	$⊢ \exists y \in A x <_{s} y \leftrightarrow \neg \forall y \in A \neg x <_{s} y$
36	35	ralbii	$⊢ \forall x \in A \exists y \in A x <_{s} y \leftrightarrow \forall x \in A \neg \forall y \in A \neg x <_{s} y$
37		ralnex	$⊢ \forall x \in A \neg \forall y \in A \neg x <_{s} y \leftrightarrow \neg \exists x \in A \forall y \in A \neg x <_{s} y$
38	34 36 37	3bitri	$⊢ \forall u \in A \exists w \in A u <_{s} w \leftrightarrow \neg \exists x \in A \forall y \in A \neg x <_{s} y$
39	28 38	sylibr	$⊢ ((\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)) \land U (dom S) = \emptyset) \to \forall u \in A \exists w \in A u <_{s} w$
40		breq1	$⊢ u = U \to (u <_{s} w \leftrightarrow U <_{s} w)$
41	40	rexbidv	$⊢ u = U \to (\exists w \in A u <_{s} w \leftrightarrow \exists w \in A U <_{s} w)$
42	41	rspcv	$⊢ U \in A \to (\forall u \in A \exists w \in A u <_{s} w \to \exists w \in A U <_{s} w)$
43	27 39 42	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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \to \exists w \in A U <_{s} w$
44		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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \to A \subseteq No$
45	44 27	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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \to U \in No$
46	45	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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to U \in No$
47	44	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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to A \subseteq No$
48		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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to w \in A$
49	47 48	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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to w \in No$
50	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
51	50	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 {U ↾}_{dom S} = S)) \to S \in No$
52	51	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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \to S \in No$
53	52	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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to S \in No$
54		nodmon	$⊢ S \in No \to dom S \in On$
55	53 54	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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to dom S \in On$
56		simpl3r	$⊢ ((\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)) \land U (dom S) = \emptyset) \to {U ↾}_{dom S} = S$
57	56	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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to {U ↾}_{dom S} = S$
58		simpll1	$⊢ (((\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)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
59		simpll2	$⊢ (((\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)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to (A \subseteq No \land A \in V)$
60		simpll3	$⊢ (((\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)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to (U \in A \land {U ↾}_{dom S} = S)$
61		simprr	$⊢ (((\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)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to U <_{s} w$
62	45 49 14	syl2an2r	$⊢ (((\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)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to (U <_{s} w \to \neg w <_{s} U)$
63	61 62	mpd	$⊢ (((\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)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to \neg w <_{s} U$
64	48 63	jca	$⊢ (((\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)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to (w \in A \land \neg w <_{s} U)$
65	58 59 60 64 18	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)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to {w ↾}_{dom S} = S$
66	57 65	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 {U ↾}_{dom S} = S)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to {U ↾}_{dom S} = {w ↾}_{dom S}$
67		simplr	$⊢ (((\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)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to U (dom S) = \emptyset$
68		nolt02o	$⊢ ((U \in No \land w \in No \land dom S \in On) \land ({U ↾}_{dom S} = {w ↾}_{dom S} \land U <_{s} w) \land U (dom S) = \emptyset) \to w (dom S) = 2_{𝑜}$
69	46 49 55 66 61 67 68	syl321anc	$⊢ (((\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)) \land U (dom S) = \emptyset) \land (w \in A \land U <_{s} w)) \to w (dom S) = 2_{𝑜}$
70	69	expr	$⊢ (((\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)) \land U (dom S) = \emptyset) \land w \in A) \to (U <_{s} w \to w (dom S) = 2_{𝑜})$
71	70	ancld	$⊢ (((\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)) \land U (dom S) = \emptyset) \land w \in A) \to (U <_{s} w \to (U <_{s} w \land w (dom S) = 2_{𝑜}))$
72	71	reximdva	$⊢ ((\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)) \land U (dom S) = \emptyset) \to (\exists w \in A U <_{s} w \to \exists w \in A (U <_{s} w \land w (dom S) = 2_{𝑜}))$
73	43 72	mpd	$⊢ ((\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)) \land U (dom S) = \emptyset) \to \exists w \in A (U <_{s} w \land w (dom S) = 2_{𝑜})$
74	26 73	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 \land {U ↾}_{dom S} = S)) \to \neg U (dom S) = \emptyset$
75	74	neqned	$⊢ (\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$

Metamath Proof Explorer

Theorem nosupbnd1lem4

Proof