nosupbnd1lem5

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

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	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
3	2	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$
4	3	adantl	$⊢ (\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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$
5		nodmord	$⊢ S \in No \to Ord dom S$
6		ordirr	$⊢ Ord dom S \to \neg dom S \in dom S$
7	4 5 6	3syl	$⊢ (\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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 dom S \in dom S$
8		simpr3l	$⊢ (\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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	8	adantr	$⊢ ((\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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) = 1_{𝑜}) \to U \in A$
10		ndmfv	$⊢ \neg dom S \in dom U \to U (dom S) = \emptyset$
11		1oex	$⊢ 1_{𝑜} \in V$
12	11	prid1	$⊢ 1_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
13	12	nosgnn0i	$⊢ \emptyset \neq 1_{𝑜}$
14		neeq1	$⊢ U (dom S) = \emptyset \to (U (dom S) \neq 1_{𝑜} \leftrightarrow \emptyset \neq 1_{𝑜})$
15	13 14	mpbiri	$⊢ U (dom S) = \emptyset \to U (dom S) \neq 1_{𝑜}$
16	15	neneqd	$⊢ U (dom S) = \emptyset \to \neg U (dom S) = 1_{𝑜}$
17	10 16	syl	$⊢ \neg dom S \in dom U \to \neg U (dom S) = 1_{𝑜}$
18	17	con4i	$⊢ U (dom S) = 1_{𝑜} \to dom S \in dom U$
19	18	adantl	$⊢ ((\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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) = 1_{𝑜}) \to dom S \in dom U$
20		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$
21		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$
22	20 21	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$
23	22	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) = 1_{𝑜}) \to U \in No$
24	23	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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to U \in No$
25		nofun	$⊢ U \in No \to Fun U$
26	24 25	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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to Fun U$
27		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) = 1_{𝑜}) \to A \subseteq No$
28		simpll	$⊢ ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜}) \to z \in A$
29		ssel2	$⊢ (A \subseteq No \land z \in A) \to z \in No$
30	27 28 29	syl2an	$⊢ (((\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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to z \in No$
31		nofun	$⊢ z \in No \to Fun z$
32	30 31	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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to Fun z$
33		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) = 1_{𝑜}) \to {U ↾}_{dom S} = S$
34	33	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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to {U ↾}_{dom S} = S$
35		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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
36		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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to (A \subseteq No \land A \in V)$
37		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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to (U \in A \land {U ↾}_{dom S} = S)$
38		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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to (z \in A \land \neg z <_{s} U)$
39	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 (z \in A \land \neg z <_{s} U))) \to {z ↾}_{dom S} = S$
40	35 36 37 38 39	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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to {z ↾}_{dom S} = S$
41	34 40	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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to {U ↾}_{dom S} = {z ↾}_{dom S}$
42	18	adantl	$⊢ ((\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) = 1_{𝑜}) \to dom S \in dom U$
43	42	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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to dom S \in dom U$
44		ndmfv	$⊢ \neg dom S \in dom z \to z (dom S) = \emptyset$
45		neeq1	$⊢ z (dom S) = \emptyset \to (z (dom S) \neq 1_{𝑜} \leftrightarrow \emptyset \neq 1_{𝑜})$
46	13 45	mpbiri	$⊢ z (dom S) = \emptyset \to z (dom S) \neq 1_{𝑜}$
47	46	neneqd	$⊢ z (dom S) = \emptyset \to \neg z (dom S) = 1_{𝑜}$
48	44 47	syl	$⊢ \neg dom S \in dom z \to \neg z (dom S) = 1_{𝑜}$
49	48	con4i	$⊢ z (dom S) = 1_{𝑜} \to dom S \in dom z$
50	49	adantl	$⊢ ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜}) \to dom S \in dom z$
51	50	adantl	$⊢ (((\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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to dom S \in dom z$
52		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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to U (dom S) = 1_{𝑜}$
53		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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to z (dom S) = 1_{𝑜}$
54	52 53	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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to U (dom S) = z (dom S)$
55		eqfunressuc	$⊢ ((Fun U \land Fun z) \land {U ↾}_{dom S} = {z ↾}_{dom S} \land (dom S \in dom U \land dom S \in dom z \land U (dom S) = z (dom S))) \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S}$
56	26 32 41 43 51 54 55	syl213anc	$⊢ (((\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) = 1_{𝑜}) \land ((z \in A \land \neg z <_{s} U) \land z (dom S) = 1_{𝑜})) \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S}$
57	56	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) = 1_{𝑜}) \land (z \in A \land \neg z <_{s} U)) \to (z (dom S) = 1_{𝑜} \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S})$
58	57	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) = 1_{𝑜}) \land z \in A) \to (\neg z <_{s} U \to (z (dom S) = 1_{𝑜} \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S}))$
59	58	a2d	$⊢ (((\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) = 1_{𝑜}) \land z \in A) \to ((\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \to (\neg z <_{s} U \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S}))$
60	59	ralimdva	$⊢ ((\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) = 1_{𝑜}) \to (\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \to \forall z \in A (\neg z <_{s} U \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S}))$
61	60	impcom	$⊢ (\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land ((\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) = 1_{𝑜})) \to \forall z \in A (\neg z <_{s} U \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S})$
62	61	anassrs	$⊢ ((\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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) = 1_{𝑜}) \to \forall z \in A (\neg z <_{s} U \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S})$
63		dmeq	$⊢ p = U \to dom p = dom U$
64	63	eleq2d	$⊢ p = U \to (dom S \in dom p \leftrightarrow dom S \in dom U)$
65		breq2	$⊢ p = U \to (z <_{s} p \leftrightarrow z <_{s} U)$
66	65	notbid	$⊢ p = U \to (\neg z <_{s} p \leftrightarrow \neg z <_{s} U)$
67		reseq1	$⊢ p = U \to {p ↾}_{suc dom S} = {U ↾}_{suc dom S}$
68	67	eqeq1d	$⊢ p = U \to ({p ↾}_{suc dom S} = {z ↾}_{suc dom S} \leftrightarrow {U ↾}_{suc dom S} = {z ↾}_{suc dom S})$
69	66 68	imbi12d	$⊢ p = U \to ((\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S}) \leftrightarrow (\neg z <_{s} U \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S}))$
70	69	ralbidv	$⊢ p = U \to (\forall z \in A (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S}) \leftrightarrow \forall z \in A (\neg z <_{s} U \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S}))$
71	64 70	anbi12d	$⊢ p = U \to ((dom S \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S})) \leftrightarrow (dom S \in dom U \land \forall z \in A (\neg z <_{s} U \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S})))$
72	71	rspcev	$⊢ (U \in A \land (dom S \in dom U \land \forall z \in A (\neg z <_{s} U \to {U ↾}_{suc dom S} = {z ↾}_{suc dom S}))) \to \exists p \in A (dom S \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S}))$
73	9 19 62 72	syl12anc	$⊢ ((\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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) = 1_{𝑜}) \to \exists p \in A (dom S \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S}))$
74		simplr1	$⊢ ((\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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) = 1_{𝑜}) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
75	1	nosupdm	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to dom S = \{a \| \exists p \in A (a \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc a} = {z ↾}_{suc a}))\}$
76	75	eleq2d	$⊢ \neg \exists x \in A \forall y \in A \neg x <_{s} y \to (dom S \in dom S \leftrightarrow dom S \in \{a \| \exists p \in A (a \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc a} = {z ↾}_{suc a}))\})$
77	74 76	syl	$⊢ ((\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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) = 1_{𝑜}) \to (dom S \in dom S \leftrightarrow dom S \in \{a \| \exists p \in A (a \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc a} = {z ↾}_{suc a}))\})$
78	4	adantr	$⊢ ((\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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) = 1_{𝑜}) \to S \in No$
79		nodmon	$⊢ S \in No \to dom S \in On$
80		eleq1	$⊢ a = dom S \to (a \in dom p \leftrightarrow dom S \in dom p)$
81		suceq	$⊢ a = dom S \to suc a = suc dom S$
82	81	reseq2d	$⊢ a = dom S \to {p ↾}_{suc a} = {p ↾}_{suc dom S}$
83	81	reseq2d	$⊢ a = dom S \to {z ↾}_{suc a} = {z ↾}_{suc dom S}$
84	82 83	eqeq12d	$⊢ a = dom S \to ({p ↾}_{suc a} = {z ↾}_{suc a} \leftrightarrow {p ↾}_{suc dom S} = {z ↾}_{suc dom S})$
85	84	imbi2d	$⊢ a = dom S \to ((\neg z <_{s} p \to {p ↾}_{suc a} = {z ↾}_{suc a}) \leftrightarrow (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S}))$
86	85	ralbidv	$⊢ a = dom S \to (\forall z \in A (\neg z <_{s} p \to {p ↾}_{suc a} = {z ↾}_{suc a}) \leftrightarrow \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S}))$
87	80 86	anbi12d	$⊢ a = dom S \to ((a \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc a} = {z ↾}_{suc a})) \leftrightarrow (dom S \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S})))$
88	87	rexbidv	$⊢ a = dom S \to (\exists p \in A (a \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc a} = {z ↾}_{suc a})) \leftrightarrow \exists p \in A (dom S \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S})))$
89	88	elabg	$⊢ dom S \in On \to (dom S \in \{a \| \exists p \in A (a \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc a} = {z ↾}_{suc a}))\} \leftrightarrow \exists p \in A (dom S \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S})))$
90	78 79 89	3syl	$⊢ ((\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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) = 1_{𝑜}) \to (dom S \in \{a \| \exists p \in A (a \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc a} = {z ↾}_{suc a}))\} \leftrightarrow \exists p \in A (dom S \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S})))$
91	77 90	bitrd	$⊢ ((\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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) = 1_{𝑜}) \to (dom S \in dom S \leftrightarrow \exists p \in A (dom S \in dom p \land \forall z \in A (\neg z <_{s} p \to {p ↾}_{suc dom S} = {z ↾}_{suc dom S})))$
92	73 91	mpbird	$⊢ ((\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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) = 1_{𝑜}) \to dom S \in dom S$
93	7 92	mtand	$⊢ (\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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_{𝑜}$
94	93	neqned	$⊢ (\forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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_{𝑜}$
95		rexanali	$⊢ \exists z \in A (\neg z <_{s} U \land \neg z (dom S) = 1_{𝑜}) \leftrightarrow \neg \forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜})$
96		simpl	$⊢ (z \in A \land \neg z <_{s} U) \to z \in A$
97	20 96 29	syl2an	$⊢ ((\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 (z \in A \land \neg z <_{s} U)) \to z \in No$
98		nofv	$⊢ z \in No \to (z (dom S) = \emptyset \lor z (dom S) = 1_{𝑜} \lor z (dom S) = 2_{𝑜})$
99	97 98	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 (z \in A \land \neg z <_{s} U)) \to (z (dom S) = \emptyset \lor z (dom S) = 1_{𝑜} \lor z (dom S) = 2_{𝑜})$
100		3orel2	$⊢ \neg z (dom S) = 1_{𝑜} \to ((z (dom S) = \emptyset \lor z (dom S) = 1_{𝑜} \lor z (dom S) = 2_{𝑜}) \to (z (dom S) = \emptyset \lor z (dom S) = 2_{𝑜}))$
101	99 100	syl5com	$⊢ ((\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 (z \in A \land \neg z <_{s} U)) \to (\neg z (dom S) = 1_{𝑜} \to (z (dom S) = \emptyset \lor z (dom S) = 2_{𝑜}))$
102	101	imdistanda	$⊢ (\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 (((z \in A \land \neg z <_{s} U) \land \neg z (dom S) = 1_{𝑜}) \to ((z \in A \land \neg z <_{s} U) \land (z (dom S) = \emptyset \lor z (dom S) = 2_{𝑜})))$
103		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 (z \in A \land \neg z <_{s} U)) \to \neg \exists x \in A \forall y \in A \neg x <_{s} y$
104		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 (z \in A \land \neg z <_{s} U)) \to (A \subseteq No \land A \in V)$
105		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 (z \in A \land \neg z <_{s} U)) \to z \in A$
106		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 (z \in A \land \neg z <_{s} U)) \to (U \in A \land {U ↾}_{dom S} = S)$
107		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)) \land (z \in A \land \neg z <_{s} U)) \to (z \in A \land \neg z <_{s} U)$
108	103 104 106 107 39	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 (z \in A \land \neg z <_{s} U)) \to {z ↾}_{dom S} = S$
109	1	nosupbnd1lem4	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (z \in A \land {z ↾}_{dom S} = S)) \to z (dom S) \neq \emptyset$
110	103 104 105 108 109	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 (z \in A \land \neg z <_{s} U)) \to z (dom S) \neq \emptyset$
111	110	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 (z \in A \land \neg z <_{s} U)) \to \neg z (dom S) = \emptyset$
112	111	pm2.21d	$⊢ ((\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 (z \in A \land \neg z <_{s} U)) \to (z (dom S) = \emptyset \to U (dom S) \neq 1_{𝑜})$
113	1	nosupbnd1lem3	$⊢ (\neg \exists x \in A \forall y \in A \neg x <_{s} y \land (A \subseteq No \land A \in V) \land (z \in A \land {z ↾}_{dom S} = S)) \to z (dom S) \neq 2_{𝑜}$
114	103 104 105 108 113	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 (z \in A \land \neg z <_{s} U)) \to z (dom S) \neq 2_{𝑜}$
115	114	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 (z \in A \land \neg z <_{s} U)) \to \neg z (dom S) = 2_{𝑜}$
116	115	pm2.21d	$⊢ ((\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 (z \in A \land \neg z <_{s} U)) \to (z (dom S) = 2_{𝑜} \to U (dom S) \neq 1_{𝑜})$
117	112 116	jaod	$⊢ ((\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 (z \in A \land \neg z <_{s} U)) \to ((z (dom S) = \emptyset \lor z (dom S) = 2_{𝑜}) \to U (dom S) \neq 1_{𝑜})$
118	117	expimpd	$⊢ (\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 (((z \in A \land \neg z <_{s} U) \land (z (dom S) = \emptyset \lor z (dom S) = 2_{𝑜})) \to U (dom S) \neq 1_{𝑜})$
119	102 118	syldc	$⊢ ((z \in A \land \neg z <_{s} U) \land \neg z (dom S) = 1_{𝑜}) \to ((\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_{𝑜})$
120	119	anasss	$⊢ (z \in A \land (\neg z <_{s} U \land \neg z (dom S) = 1_{𝑜})) \to ((\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_{𝑜})$
121	120	rexlimiva	$⊢ \exists z \in A (\neg z <_{s} U \land \neg z (dom S) = 1_{𝑜}) \to ((\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_{𝑜})$
122	121	imp	$⊢ (\exists z \in A (\neg z <_{s} U \land \neg z (dom S) = 1_{𝑜}) \land (\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_{𝑜}$
123	95 122	sylanbr	$⊢ (\neg \forall z \in A (\neg z <_{s} U \to z (dom S) = 1_{𝑜}) \land (\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_{𝑜}$
124	94 123	pm2.61ian	$⊢ (\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_{𝑜}$

Metamath Proof Explorer

Theorem nosupbnd1lem5

Proof