Theorem nosupbnd1

Description: Bounding law from below for the surreal supremum. Proposition 4.2 of Lipparini p. 6. (Contributed by Scott Fenton, 6-Dec-2021)

	Ref	Expression
Hypothesis	nosupbnd1.1	|- S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
Assertion	nosupbnd1	|- ( ( A C_ No /\ A e. _V /\ U e. A ) -> ( U |` dom S )

Proof

Step	Hyp	Ref	Expression
1		nosupbnd1.1	|- S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
2		simpr3	|- ( ( E. x e. A A. y e. A -. x U e. A )
3		nfv	|- F/ x ( A C_ No /\ A e. _V /\ U e. A )
4		nfcv	|- F/_ x A
5		nfriota1	|- F/_ x ( iota_ x e. A A. y e. A -. x
6		nfcv	|- F/_ x
7		nfcv	|- F/_ x y
8	5 6 7	nfbr	|- F/ x ( iota_ x e. A A. y e. A -. x
9	8	nfn	|- F/ x -. ( iota_ x e. A A. y e. A -. x
10	4 9	nfralw	|- F/ x A. y e. A -. ( iota_ x e. A A. y e. A -. x
11	3 10	nfim	|- F/ x ( ( A C_ No /\ A e. _V /\ U e. A ) -> A. y e. A -. ( iota_ x e. A A. y e. A -. x
12		simpl	|- ( ( ( x e. A /\ A. y e. A -. x ( x e. A /\ A. y e. A -. x
13		rspe	|- ( ( x e. A /\ A. y e. A -. x E. x e. A A. y e. A -. x
14	13	adantr	|- ( ( ( x e. A /\ A. y e. A -. x E. x e. A A. y e. A -. x
15		nomaxmo	|- ( A C_ No -> E* x e. A A. y e. A -. x
16	15	3ad2ant1	|- ( ( A C_ No /\ A e. _V /\ U e. A ) -> E* x e. A A. y e. A -. x
17	16	adantl	|- ( ( ( x e. A /\ A. y e. A -. x E* x e. A A. y e. A -. x
18		reu5	|- ( E! x e. A A. y e. A -. x ( E. x e. A A. y e. A -. x
19	14 17 18	sylanbrc	|- ( ( ( x e. A /\ A. y e. A -. x E! x e. A A. y e. A -. x
20		riota1	|- ( E! x e. A A. y e. A -. x ( ( x e. A /\ A. y e. A -. x ( iota_ x e. A A. y e. A -. x
21	19 20	syl	|- ( ( ( x e. A /\ A. y e. A -. x ( ( x e. A /\ A. y e. A -. x ( iota_ x e. A A. y e. A -. x
22	12 21	mpbid	|- ( ( ( x e. A /\ A. y e. A -. x ( iota_ x e. A A. y e. A -. x
23		simplr	|- ( ( ( x e. A /\ A. y e. A -. x A. y e. A -. x
24		nfra1	|- F/ y A. y e. A -. x
25		nfcv	|- F/_ y A
26	24 25	nfriota	|- F/_ y ( iota_ x e. A A. y e. A -. x
27		nfcv	|- F/_ y x
28	26 27	nfeq	|- F/ y ( iota_ x e. A A. y e. A -. x
29		breq1	|- ( ( iota_ x e. A A. y e. A -. x ( ( iota_ x e. A A. y e. A -. x x
30	29	notbid	|- ( ( iota_ x e. A A. y e. A -. x ( -. ( iota_ x e. A A. y e. A -. x -. x
31	28 30	ralbid	|- ( ( iota_ x e. A A. y e. A -. x ( A. y e. A -. ( iota_ x e. A A. y e. A -. x A. y e. A -. x
32	31	biimprd	|- ( ( iota_ x e. A A. y e. A -. x ( A. y e. A -. x A. y e. A -. ( iota_ x e. A A. y e. A -. x
33	22 23 32	sylc	|- ( ( ( x e. A /\ A. y e. A -. x A. y e. A -. ( iota_ x e. A A. y e. A -. x
34	33	exp31	|- ( x e. A -> ( A. y e. A -. x ( ( A C_ No /\ A e. _V /\ U e. A ) -> A. y e. A -. ( iota_ x e. A A. y e. A -. x
35	11 34	rexlimi	|- ( E. x e. A A. y e. A -. x ( ( A C_ No /\ A e. _V /\ U e. A ) -> A. y e. A -. ( iota_ x e. A A. y e. A -. x
36	35	imp	|- ( ( E. x e. A A. y e. A -. x A. y e. A -. ( iota_ x e. A A. y e. A -. x
37		nfcv	|- F/_ y
38		nfcv	|- F/_ y U
39	26 37 38	nfbr	|- F/ y ( iota_ x e. A A. y e. A -. x
40	39	nfn	|- F/ y -. ( iota_ x e. A A. y e. A -. x
41		breq2	|- ( y = U -> ( ( iota_ x e. A A. y e. A -. x ( iota_ x e. A A. y e. A -. x
42	41	notbid	|- ( y = U -> ( -. ( iota_ x e. A A. y e. A -. x -. ( iota_ x e. A A. y e. A -. x
43	40 42	rspc	|- ( U e. A -> ( A. y e. A -. ( iota_ x e. A A. y e. A -. x -. ( iota_ x e. A A. y e. A -. x
44	2 36 43	sylc	|- ( ( E. x e. A A. y e. A -. x -. ( iota_ x e. A A. y e. A -. x
45		simpr1	|- ( ( E. x e. A A. y e. A -. x A C_ No )
46		simpl	|- ( ( E. x e. A A. y e. A -. x E. x e. A A. y e. A -. x
47	16	adantl	|- ( ( E. x e. A A. y e. A -. x E* x e. A A. y e. A -. x
48	46 47 18	sylanbrc	|- ( ( E. x e. A A. y e. A -. x E! x e. A A. y e. A -. x
49		riotacl	|- ( E! x e. A A. y e. A -. x ( iota_ x e. A A. y e. A -. x
50	48 49	syl	|- ( ( E. x e. A A. y e. A -. x ( iota_ x e. A A. y e. A -. x
51	45 50	sseldd	|- ( ( E. x e. A A. y e. A -. x ( iota_ x e. A A. y e. A -. x
52		nofun	|- ( ( iota_ x e. A A. y e. A -. x Fun ( iota_ x e. A A. y e. A -. x
53		funrel	|- ( Fun ( iota_ x e. A A. y e. A -. x Rel ( iota_ x e. A A. y e. A -. x
54	51 52 53	3syl	|- ( ( E. x e. A A. y e. A -. x Rel ( iota_ x e. A A. y e. A -. x
55		sssucid	|- dom ( iota_ x e. A A. y e. A -. x
56		relssres	|- ( ( Rel ( iota_ x e. A A. y e. A -. x ( ( iota_ x e. A A. y e. A -. x
57	54 55 56	sylancl	|- ( ( E. x e. A A. y e. A -. x ( ( iota_ x e. A A. y e. A -. x
58	57	breq1d	|- ( ( E. x e. A A. y e. A -. x ( ( ( iota_ x e. A A. y e. A -. x ( iota_ x e. A A. y e. A -. x
59	45 2	sseldd	|- ( ( E. x e. A A. y e. A -. x U e. No )
60		nodmon	|- ( ( iota_ x e. A A. y e. A -. x dom ( iota_ x e. A A. y e. A -. x
61	51 60	syl	|- ( ( E. x e. A A. y e. A -. x dom ( iota_ x e. A A. y e. A -. x
62		sucelon	|- ( dom ( iota_ x e. A A. y e. A -. x suc dom ( iota_ x e. A A. y e. A -. x
63	61 62	sylib	|- ( ( E. x e. A A. y e. A -. x suc dom ( iota_ x e. A A. y e. A -. x
64		sltres	|- ( ( ( iota_ x e. A A. y e. A -. x ( ( ( iota_ x e. A A. y e. A -. x ( iota_ x e. A A. y e. A -. x
65	51 59 63 64	syl3anc	|- ( ( E. x e. A A. y e. A -. x ( ( ( iota_ x e. A A. y e. A -. x ( iota_ x e. A A. y e. A -. x
66	58 65	sylbird	|- ( ( E. x e. A A. y e. A -. x ( ( iota_ x e. A A. y e. A -. x ( iota_ x e. A A. y e. A -. x
67	44 66	mtod	|- ( ( E. x e. A A. y e. A -. x -. ( iota_ x e. A A. y e. A -. x
68		noextendgt	|- ( ( iota_ x e. A A. y e. A -. x ( iota_ x e. A A. y e. A -. x . } ) )
69	51 68	syl	|- ( ( E. x e. A A. y e. A -. x ( iota_ x e. A A. y e. A -. x . } ) )
70		noreson	|- ( ( U e. No /\ suc dom ( iota_ x e. A A. y e. A -. x ( U |` suc dom ( iota_ x e. A A. y e. A -. x
71	59 63 70	syl2anc	|- ( ( E. x e. A A. y e. A -. x ( U |` suc dom ( iota_ x e. A A. y e. A -. x
72		2on	|- 2o e. On
73	72	elexi	|- 2o e. _V
74	73	prid2	|- 2o e. { 1o , 2o }
75	74	noextend	|- ( ( iota_ x e. A A. y e. A -. x ( ( iota_ x e. A A. y e. A -. x . } ) e. No )
76	51 75	syl	|- ( ( E. x e. A A. y e. A -. x ( ( iota_ x e. A A. y e. A -. x . } ) e. No )
77		sltso	|-
78		sotr2	|- ( ( . } ) e. No ) ) -> ( ( -. ( iota_ x e. A A. y e. A -. x . } ) ) -> ( U |` suc dom ( iota_ x e. A A. y e. A -. x . } ) ) )
79	77 78	mpan	|- ( ( ( U |` suc dom ( iota_ x e. A A. y e. A -. x . } ) e. No ) -> ( ( -. ( iota_ x e. A A. y e. A -. x . } ) ) -> ( U |` suc dom ( iota_ x e. A A. y e. A -. x . } ) ) )
80	71 51 76 79	syl3anc	|- ( ( E. x e. A A. y e. A -. x ( ( -. ( iota_ x e. A A. y e. A -. x . } ) ) -> ( U |` suc dom ( iota_ x e. A A. y e. A -. x . } ) ) )
81	67 69 80	mp2and	|- ( ( E. x e. A A. y e. A -. x ( U |` suc dom ( iota_ x e. A A. y e. A -. x . } ) )
82		iftrue	|- ( E. x e. A A. y e. A -. x if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ) = ( ( iota_ x e. A A. y e. A -. x . } ) )
83	1 82	syl5eq	|- ( E. x e. A A. y e. A -. x S = ( ( iota_ x e. A A. y e. A -. x . } ) )
84	83	dmeqd	|- ( E. x e. A A. y e. A -. x dom S = dom ( ( iota_ x e. A A. y e. A -. x . } ) )
85	73	dmsnop	|- dom { <. dom ( iota_ x e. A A. y e. A -. x . } = { dom ( iota_ x e. A A. y e. A -. x
86	85	uneq2i	|- ( dom ( iota_ x e. A A. y e. A -. x . } ) = ( dom ( iota_ x e. A A. y e. A -. x
87		dmun	|- dom ( ( iota_ x e. A A. y e. A -. x . } ) = ( dom ( iota_ x e. A A. y e. A -. x . } )
88		df-suc	|- suc dom ( iota_ x e. A A. y e. A -. x
89	86 87 88	3eqtr4i	|- dom ( ( iota_ x e. A A. y e. A -. x . } ) = suc dom ( iota_ x e. A A. y e. A -. x
90	84 89	eqtrdi	|- ( E. x e. A A. y e. A -. x dom S = suc dom ( iota_ x e. A A. y e. A -. x
91	90	adantr	|- ( ( E. x e. A A. y e. A -. x dom S = suc dom ( iota_ x e. A A. y e. A -. x
92	91	reseq2d	|- ( ( E. x e. A A. y e. A -. x ( U |` dom S ) = ( U |` suc dom ( iota_ x e. A A. y e. A -. x
93	83	adantr	|- ( ( E. x e. A A. y e. A -. x S = ( ( iota_ x e. A A. y e. A -. x . } ) )
94	81 92 93	3brtr4d	|- ( ( E. x e. A A. y e. A -. x ( U |` dom S )
95		simpl	|- ( ( -. E. x e. A A. y e. A -. x -. E. x e. A A. y e. A -. x
96		simpr1	|- ( ( -. E. x e. A A. y e. A -. x A C_ No )
97		simpr2	|- ( ( -. E. x e. A A. y e. A -. x A e. _V )
98		simpr3	|- ( ( -. E. x e. A A. y e. A -. x U e. A )
99	1	nosupbnd1lem6	|- ( ( -. E. x e. A A. y e. A -. x ( U |` dom S )
100	95 96 97 98 99	syl121anc	|- ( ( -. E. x e. A A. y e. A -. x ( U |` dom S )
101	94 100	pm2.61ian	|- ( ( A C_ No /\ A e. _V /\ U e. A ) -> ( U |` dom S )