Theorem noinfbnd1

Description: Bounding law from above for the surreal infimum. Analagous to proposition 4.2 of Lipparini p. 6. (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

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