noresle

Description: Restriction law for surreals. Lemma 2.1.4 of Lipparini p. 3. (Contributed by Scott Fenton, 5-Dec-2021)

		Ref	Expression
	Assertion	noresle	$⊢ ((U \in No \land S \in No) \land (dom U \subseteq A \land dom S \subseteq A \land \forall g \in A \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to \neg S <_{s} U$

Proof

Step	Hyp	Ref	Expression
1		unss	$⊢ (dom U \subseteq A \land dom S \subseteq A) \leftrightarrow dom U \cup dom S \subseteq A$
2		ssralv	$⊢ dom U \cup dom S \subseteq A \to (\forall g \in A \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}) \to \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))$
3	1 2	sylbi	$⊢ (dom U \subseteq A \land dom S \subseteq A) \to (\forall g \in A \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}) \to \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))$
4	3	3impia	$⊢ (dom U \subseteq A \land dom S \subseteq A \land \forall g \in A \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g})) \to \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g})$
5		breq1	$⊢ U = S \to (U <_{s} U \leftrightarrow S <_{s} U)$
6	5	notbid	$⊢ U = S \to (\neg U <_{s} U \leftrightarrow \neg S <_{s} U)$
7	6	biimpd	$⊢ U = S \to (\neg U <_{s} U \to \neg S <_{s} U)$
8		sltso	$⊢ <_{s} Or No$
9		sonr	$⊢ (<_{s} Or No \land U \in No) \to \neg U <_{s} U$
10	8 9	mpan	$⊢ U \in No \to \neg U <_{s} U$
11	10	adantr	$⊢ (U \in No \land S \in No) \to \neg U <_{s} U$
12	7 11	impel	$⊢ (U = S \land (U \in No \land S \in No)) \to \neg S <_{s} U$
13	12	adantrr	$⊢ (U = S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to \neg S <_{s} U$
14	13	ex	$⊢ U = S \to (((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g})) \to \neg S <_{s} U)$
15		simprl	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to (U \in No \land S \in No)$
16		simprll	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to U \in No$
17		simprlr	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to S \in No$
18		simpl	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to U \neq S$
19		nosepne	$⊢ (U \in No \land S \in No \land U \neq S) \to U (⋂ \{x \in On \| U (x) \neq S (x)\}) \neq S (⋂ \{x \in On \| U (x) \neq S (x)\})$
20	16 17 18 19	syl3anc	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to U (⋂ \{x \in On \| U (x) \neq S (x)\}) \neq S (⋂ \{x \in On \| U (x) \neq S (x)\})$
21		nosepon	$⊢ (U \in No \land S \in No \land U \neq S) \to ⋂ \{x \in On \| U (x) \neq S (x)\} \in On$
22	16 17 18 21	syl3anc	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to ⋂ \{x \in On \| U (x) \neq S (x)\} \in On$
23		sucidg	$⊢ ⋂ \{x \in On \| U (x) \neq S (x)\} \in On \to ⋂ \{x \in On \| U (x) \neq S (x)\} \in suc ⋂ \{x \in On \| U (x) \neq S (x)\}$
24	22 23	syl	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to ⋂ \{x \in On \| U (x) \neq S (x)\} \in suc ⋂ \{x \in On \| U (x) \neq S (x)\}$
25	24	fvresd	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) (⋂ \{x \in On \| U (x) \neq S (x)\}) = U (⋂ \{x \in On \| U (x) \neq S (x)\})$
26	24	fvresd	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) (⋂ \{x \in On \| U (x) \neq S (x)\}) = S (⋂ \{x \in On \| U (x) \neq S (x)\})$
27	20 25 26	3netr4d	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) (⋂ \{x \in On \| U (x) \neq S (x)\}) \neq ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) (⋂ \{x \in On \| U (x) \neq S (x)\})$
28	27	neneqd	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to \neg ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) (⋂ \{x \in On \| U (x) \neq S (x)\}) = ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) (⋂ \{x \in On \| U (x) \neq S (x)\})$
29		fveq1	$⊢ {U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} = {S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \to ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) (⋂ \{x \in On \| U (x) \neq S (x)\}) = ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) (⋂ \{x \in On \| U (x) \neq S (x)\})$
30	28 29	nsyl	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to \neg {U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} = {S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}$
31		nosepdm	$⊢ (U \in No \land S \in No \land U \neq S) \to ⋂ \{x \in On \| U (x) \neq S (x)\} \in (dom U \cup dom S)$
32	16 17 18 31	syl3anc	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to ⋂ \{x \in On \| U (x) \neq S (x)\} \in (dom U \cup dom S)$
33		simprr	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g})$
34		suceq	$⊢ g = ⋂ \{x \in On \| U (x) \neq S (x)\} \to suc g = suc ⋂ \{x \in On \| U (x) \neq S (x)\}$
35	34	reseq2d	$⊢ g = ⋂ \{x \in On \| U (x) \neq S (x)\} \to {S ↾}_{suc g} = {S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}$
36	34	reseq2d	$⊢ g = ⋂ \{x \in On \| U (x) \neq S (x)\} \to {U ↾}_{suc g} = {U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}$
37	35 36	breq12d	$⊢ g = ⋂ \{x \in On \| U (x) \neq S (x)\} \to (({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}) \leftrightarrow ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}))$
38	37	notbid	$⊢ g = ⋂ \{x \in On \| U (x) \neq S (x)\} \to (\neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}) \leftrightarrow \neg ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}))$
39	38	rspcv	$⊢ ⋂ \{x \in On \| U (x) \neq S (x)\} \in (dom U \cup dom S) \to (\forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}) \to \neg ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}))$
40	32 33 39	sylc	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to \neg ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}})$
41		suceloni	$⊢ ⋂ \{x \in On \| U (x) \neq S (x)\} \in On \to suc ⋂ \{x \in On \| U (x) \neq S (x)\} \in On$
42	22 41	syl	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to suc ⋂ \{x \in On \| U (x) \neq S (x)\} \in On$
43		noreson	$⊢ (U \in No \land suc ⋂ \{x \in On \| U (x) \neq S (x)\} \in On) \to {U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \in No$
44	16 42 43	syl2anc	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to {U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \in No$
45		noreson	$⊢ (S \in No \land suc ⋂ \{x \in On \| U (x) \neq S (x)\} \in On) \to {S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \in No$
46	17 42 45	syl2anc	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to {S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \in No$
47		solin	$⊢ (<_{s} Or No \land ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \in No \land {S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \in No)) \to (({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) \lor {U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} = {S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \lor ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}))$
48	8 47	mpan	$⊢ ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \in No \land {S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \in No) \to (({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) \lor {U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} = {S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \lor ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}))$
49	44 46 48	syl2anc	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to (({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) \lor {U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} = {S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}} \lor ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}))$
50	30 40 49	ecase23d	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to ({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}})$
51		sltres	$⊢ (U \in No \land S \in No \land suc ⋂ \{x \in On \| U (x) \neq S (x)\} \in On) \to (({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) \to U <_{s} S)$
52	16 17 42 51	syl3anc	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to (({U ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) <_{s} ({S ↾}_{suc ⋂ \{x \in On \| U (x) \neq S (x)\}}) \to U <_{s} S)$
53	50 52	mpd	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to U <_{s} S$
54		soasym	$⊢ (<_{s} Or No \land (U \in No \land S \in No)) \to (U <_{s} S \to \neg S <_{s} U)$
55	8 54	mpan	$⊢ (U \in No \land S \in No) \to (U <_{s} S \to \neg S <_{s} U)$
56	15 53 55	sylc	$⊢ (U \neq S \land ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to \neg S <_{s} U$
57	56	ex	$⊢ U \neq S \to (((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g})) \to \neg S <_{s} U)$
58	14 57	pm2.61ine	$⊢ ((U \in No \land S \in No) \land \forall g \in (dom U \cup dom S) \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g})) \to \neg S <_{s} U$
59	4 58	sylan2	$⊢ ((U \in No \land S \in No) \land (dom U \subseteq A \land dom S \subseteq A \land \forall g \in A \neg ({S ↾}_{suc g}) <_{s} ({U ↾}_{suc g}))) \to \neg S <_{s} U$

Metamath Proof Explorer

Theorem noresle

Proof