noinfbnd1lem4

Description: Lemma for noinfbnd1 . If U is a prolongment of T and in B , then ( Udom T ) is not undefined. (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	noinfbnd1lem4	$⊢ (\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)) \to U (dom T) \neq \emptyset$

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		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 {U ↾}_{dom T} = T)) \land (w \in B \land w <_{s} U)) \to \neg \exists x \in B \forall y \in B \neg y <_{s} x$
3		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 {U ↾}_{dom T} = T)) \land (w \in B \land w <_{s} U)) \to (B \subseteq No \land B \in V)$
4		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 {U ↾}_{dom T} = T)) \land (w \in B \land w <_{s} U)) \to w \in B$
5		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 {U ↾}_{dom T} = T)) \land (w \in B \land w <_{s} U)) \to (U \in B \land {U ↾}_{dom T} = T)$
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)) \to B \subseteq No$
7	6	sselda	$⊢ ((\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) \to w \in No$
8		simp3l	$⊢ (\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)) \to U \in B$
9	6 8	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)) \to U \in No$
10	9	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 {U ↾}_{dom T} = T)) \land w \in B) \to U \in No$
11		sltso	$⊢ <_{s} Or No$
12		soasym	$⊢ (<_{s} Or No \land (w \in No \land U \in No)) \to (w <_{s} U \to \neg U <_{s} w)$
13	11 12	mpan	$⊢ (w \in No \land U \in No) \to (w <_{s} U \to \neg U <_{s} w)$
14	7 10 13	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) \to (w <_{s} U \to \neg U <_{s} w)$
15	14	impr	$⊢ ((\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 w <_{s} U)) \to \neg U <_{s} w$
16	4 15	jca	$⊢ ((\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 w <_{s} U)) \to (w \in B \land \neg U <_{s} w)$
17	1	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$
18	2 3 5 16 17	syl112anc	$⊢ ((\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 w <_{s} U)) \to {w ↾}_{dom T} = T$
19	1	noinfbnd1lem3	$⊢ (\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 \land {w ↾}_{dom T} = T)) \to w (dom T) \neq 1_{𝑜}$
20	2 3 4 18 19	syl112anc	$⊢ ((\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 w <_{s} U)) \to w (dom T) \neq 1_{𝑜}$
21	20	neneqd	$⊢ ((\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 w <_{s} U)) \to \neg w (dom T) = 1_{𝑜}$
22	21	expr	$⊢ ((\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) \to (w <_{s} U \to \neg w (dom T) = 1_{𝑜})$
23		imnan	$⊢ (w <_{s} U \to \neg w (dom T) = 1_{𝑜}) \leftrightarrow \neg (w <_{s} U \land w (dom T) = 1_{𝑜})$
24	22 23	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 {U ↾}_{dom T} = T)) \land w \in B) \to \neg (w <_{s} U \land w (dom T) = 1_{𝑜})$
25	24	nrexdv	$⊢ (\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)) \to \neg \exists w \in B (w <_{s} U \land w (dom T) = 1_{𝑜})$
26		breq2	$⊢ x = U \to (y <_{s} x \leftrightarrow y <_{s} U)$
27	26	rexbidv	$⊢ x = U \to (\exists y \in B y <_{s} x \leftrightarrow \exists y \in B y <_{s} U)$
28		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 {U ↾}_{dom T} = T)) \land U (dom T) = \emptyset) \to \neg \exists x \in B \forall y \in B \neg y <_{s} x$
29		dfral2	$⊢ \forall x \in B \exists y \in B y <_{s} x \leftrightarrow \neg \exists x \in B \neg \exists y \in B y <_{s} x$
30		ralnex	$⊢ \forall y \in B \neg y <_{s} x \leftrightarrow \neg \exists y \in B y <_{s} x$
31	30	rexbii	$⊢ \exists x \in B \forall y \in B \neg y <_{s} x \leftrightarrow \exists x \in B \neg \exists y \in B y <_{s} x$
32	29 31	xchbinxr	$⊢ \forall x \in B \exists y \in B y <_{s} x \leftrightarrow \neg \exists x \in B \forall y \in B \neg y <_{s} x$
33	28 32	sylibr	$⊢ ((\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 U (dom T) = \emptyset) \to \forall x \in B \exists y \in B y <_{s} x$
34		simpl3l	$⊢ ((\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 U (dom T) = \emptyset) \to U \in B$
35	27 33 34	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 {U ↾}_{dom T} = T)) \land U (dom T) = \emptyset) \to \exists y \in B y <_{s} U$
36		breq1	$⊢ y = w \to (y <_{s} U \leftrightarrow w <_{s} U)$
37	36	cbvrexvw	$⊢ \exists y \in B y <_{s} U \leftrightarrow \exists w \in B w <_{s} U$
38	35 37	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 {U ↾}_{dom T} = T)) \land U (dom T) = \emptyset) \to \exists w \in B w <_{s} U$
39		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 {U ↾}_{dom T} = T)) \land U (dom T) = \emptyset) \to B \subseteq No$
40	39	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 {U ↾}_{dom T} = T)) \land U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to B \subseteq No$
41		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 {U ↾}_{dom T} = T)) \land U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to w \in B$
42	40 41	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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to w \in No$
43	34	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 {U ↾}_{dom T} = T)) \land U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to U \in B$
44	40 43	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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to U \in No$
45		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 {U ↾}_{dom T} = T)) \land U (dom T) = \emptyset) \to (B \subseteq No \land B \in V)$
46	1	noinfno	$⊢ (B \subseteq No \land B \in V) \to T \in No$
47	45 46	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 U (dom T) = \emptyset) \to T \in No$
48	47	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 {U ↾}_{dom T} = T)) \land U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to T \in No$
49		nodmon	$⊢ T \in No \to dom T \in On$
50	48 49	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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to dom T \in On$
51		simpll1	$⊢ (((\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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to \neg \exists x \in B \forall y \in B \neg y <_{s} x$
52		simpll2	$⊢ (((\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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to (B \subseteq No \land B \in V)$
53		simpll3	$⊢ (((\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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to (U \in B \land {U ↾}_{dom T} = T)$
54		simprr	$⊢ (((\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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to w <_{s} U$
55	42 44 13	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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to (w <_{s} U \to \neg U <_{s} w)$
56	54 55	mpd	$⊢ (((\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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to \neg U <_{s} w$
57	41 56	jca	$⊢ (((\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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to (w \in B \land \neg U <_{s} w)$
58	51 52 53 57 17	syl112anc	$⊢ (((\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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to {w ↾}_{dom T} = T$
59		simpl3r	$⊢ ((\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 U (dom T) = \emptyset) \to {U ↾}_{dom T} = T$
60	59	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 {U ↾}_{dom T} = T)) \land U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to {U ↾}_{dom T} = T$
61	58 60	eqtr4d	$⊢ (((\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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to {w ↾}_{dom T} = {U ↾}_{dom T}$
62		simplr	$⊢ (((\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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to U (dom T) = \emptyset$
63		nogt01o	$⊢ ((w \in No \land U \in No \land dom T \in On) \land ({w ↾}_{dom T} = {U ↾}_{dom T} \land w <_{s} U) \land U (dom T) = \emptyset) \to w (dom T) = 1_{𝑜}$
64	42 44 50 61 54 62 63	syl321anc	$⊢ (((\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 U (dom T) = \emptyset) \land (w \in B \land w <_{s} U)) \to w (dom T) = 1_{𝑜}$
65	64	expr	$⊢ (((\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 U (dom T) = \emptyset) \land w \in B) \to (w <_{s} U \to w (dom T) = 1_{𝑜})$
66	65	ancld	$⊢ (((\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 U (dom T) = \emptyset) \land w \in B) \to (w <_{s} U \to (w <_{s} U \land w (dom T) = 1_{𝑜}))$
67	66	reximdva	$⊢ ((\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 U (dom T) = \emptyset) \to (\exists w \in B w <_{s} U \to \exists w \in B (w <_{s} U \land w (dom T) = 1_{𝑜}))$
68	38 67	mpd	$⊢ ((\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 U (dom T) = \emptyset) \to \exists w \in B (w <_{s} U \land w (dom T) = 1_{𝑜})$
69	25 68	mtand	$⊢ (\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)) \to \neg U (dom T) = \emptyset$
70	69	neqned	$⊢ (\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)) \to U (dom T) \neq \emptyset$

Metamath Proof Explorer

Theorem noinfbnd1lem4

Proof