Theorem noinfbday

Description: Birthday bounding law for surreal infimum. (Contributed by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Hypothesis	noinfbday.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	noinfbday	|- ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) -> ( bday ` T ) C_ O )

Proof

Step	Hyp	Ref	Expression
1		noinfbday.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	1	noinfno	|- ( ( B C_ No /\ B e. V ) -> T e. No )
3		bdayval	|- ( T e. No -> ( bday ` T ) = dom T )
4	2 3	syl	|- ( ( B C_ No /\ B e. V ) -> ( bday ` T ) = dom T )
5	4	adantr	|- ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) -> ( bday ` T ) = dom T )
6		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 . } ) )
7	1 6	eqtrid	|- ( E. x e. B A. y e. B -. y T = ( ( iota_ x e. B A. y e. B -. y . } ) )
8	7	dmeqd	|- ( E. x e. B A. y e. B -. y dom T = dom ( ( iota_ x e. B A. y e. B -. y . } ) )
9		1oex	|- 1o e. _V
10	9	dmsnop	|- dom { <. dom ( iota_ x e. B A. y e. B -. y . } = { dom ( iota_ x e. B A. y e. B -. y
11	10	uneq2i	|- ( dom ( iota_ x e. B A. y e. B -. y . } ) = ( dom ( iota_ x e. B A. y e. B -. y
12		dmun	|- dom ( ( iota_ x e. B A. y e. B -. y . } ) = ( dom ( iota_ x e. B A. y e. B -. y . } )
13		df-suc	|- suc dom ( iota_ x e. B A. y e. B -. y
14	11 12 13	3eqtr4i	|- dom ( ( iota_ x e. B A. y e. B -. y . } ) = suc dom ( iota_ x e. B A. y e. B -. y
15	8 14	eqtrdi	|- ( E. x e. B A. y e. B -. y dom T = suc dom ( iota_ x e. B A. y e. B -. y
16	15	adantr	|- ( ( E. x e. B A. y e. B -. y dom T = suc dom ( iota_ x e. B A. y e. B -. y
17		simprrl	|- ( ( E. x e. B A. y e. B -. y O e. On )
18		eloni	|- ( O e. On -> Ord O )
19	17 18	syl	|- ( ( E. x e. B A. y e. B -. y Ord O )
20		simprll	|- ( ( E. x e. B A. y e. B -. y B C_ No )
21		simpl	|- ( ( E. x e. B A. y e. B -. y E. x e. B A. y e. B -. y
22		nominmo	|- ( B C_ No -> E* x e. B A. y e. B -. y
23	20 22	syl	|- ( ( E. x e. B A. y e. B -. y E* x e. B A. y e. B -. y
24		reu5	|- ( E! x e. B A. y e. B -. y ( E. x e. B A. y e. B -. y
25	21 23 24	sylanbrc	|- ( ( E. x e. B A. y e. B -. y E! x e. B A. y e. B -. y
26		riotacl	|- ( E! x e. B A. y e. B -. y ( iota_ x e. B A. y e. B -. y
27	25 26	syl	|- ( ( E. x e. B A. y e. B -. y ( iota_ x e. B A. y e. B -. y
28	20 27	sseldd	|- ( ( E. x e. B A. y e. B -. y ( iota_ x e. B A. y e. B -. y
29		bdayval	|- ( ( iota_ x e. B A. y e. B -. y ( bday ` ( iota_ x e. B A. y e. B -. y
30	28 29	syl	|- ( ( E. x e. B A. y e. B -. y ( bday ` ( iota_ x e. B A. y e. B -. y
31		simprrr	|- ( ( E. x e. B A. y e. B -. y ( bday " B ) C_ O )
32		bdayfo	|- bday : No -onto-> On
33		fofn	|- ( bday : No -onto-> On -> bday Fn No )
34	32 33	ax-mp	|- bday Fn No
35		fnfvima	|- ( ( bday Fn No /\ B C_ No /\ ( iota_ x e. B A. y e. B -. y ( bday ` ( iota_ x e. B A. y e. B -. y
36	34 20 27 35	mp3an2i	|- ( ( E. x e. B A. y e. B -. y ( bday ` ( iota_ x e. B A. y e. B -. y
37	31 36	sseldd	|- ( ( E. x e. B A. y e. B -. y ( bday ` ( iota_ x e. B A. y e. B -. y
38	30 37	eqeltrrd	|- ( ( E. x e. B A. y e. B -. y dom ( iota_ x e. B A. y e. B -. y
39		ordsucss	|- ( Ord O -> ( dom ( iota_ x e. B A. y e. B -. y suc dom ( iota_ x e. B A. y e. B -. y
40	19 38 39	sylc	|- ( ( E. x e. B A. y e. B -. y suc dom ( iota_ x e. B A. y e. B -. y
41	16 40	eqsstrd	|- ( ( E. x e. B A. y e. B -. y dom T C_ O )
42	1	noinfdm	|- ( -. E. x e. B A. y e. B -. y dom T = { z | E. p e. B ( z e. dom p /\ A. q e. B ( -. p ( p |` suc z ) = ( q |` suc z ) ) ) } )
43	42	adantr	|- ( ( -. E. x e. B A. y e. B -. y dom T = { z | E. p e. B ( z e. dom p /\ A. q e. B ( -. p ( p |` suc z ) = ( q |` suc z ) ) ) } )
44		simplrl	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> O e. On )
45	44 18	syl	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> Ord O )
46		ssel2	|- ( ( B C_ No /\ p e. B ) -> p e. No )
47	46	ad4ant14	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> p e. No )
48		bdayval	|- ( p e. No -> ( bday ` p ) = dom p )
49	47 48	syl	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> ( bday ` p ) = dom p )
50		simplrr	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> ( bday " B ) C_ O )
51		fnfvima	|- ( ( bday Fn No /\ B C_ No /\ p e. B ) -> ( bday ` p ) e. ( bday " B ) )
52	34 51	mp3an1	|- ( ( B C_ No /\ p e. B ) -> ( bday ` p ) e. ( bday " B ) )
53	52	ad4ant14	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> ( bday ` p ) e. ( bday " B ) )
54	50 53	sseldd	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> ( bday ` p ) e. O )
55	49 54	eqeltrrd	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> dom p e. O )
56		ordelss	|- ( ( Ord O /\ dom p e. O ) -> dom p C_ O )
57	45 55 56	syl2anc	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> dom p C_ O )
58	57	sseld	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> ( z e. dom p -> z e. O ) )
59	58	adantrd	|- ( ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) /\ p e. B ) -> ( ( z e. dom p /\ A. q e. B ( -. p ( p |` suc z ) = ( q |` suc z ) ) ) -> z e. O ) )
60	59	rexlimdva	|- ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) -> ( E. p e. B ( z e. dom p /\ A. q e. B ( -. p ( p |` suc z ) = ( q |` suc z ) ) ) -> z e. O ) )
61	60	abssdv	|- ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) -> { z | E. p e. B ( z e. dom p /\ A. q e. B ( -. p ( p |` suc z ) = ( q |` suc z ) ) ) } C_ O )
62	61	adantl	|- ( ( -. E. x e. B A. y e. B -. y { z | E. p e. B ( z e. dom p /\ A. q e. B ( -. p ( p |` suc z ) = ( q |` suc z ) ) ) } C_ O )
63	43 62	eqsstrd	|- ( ( -. E. x e. B A. y e. B -. y dom T C_ O )
64	41 63	pm2.61ian	|- ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) -> dom T C_ O )
65	5 64	eqsstrd	|- ( ( ( B C_ No /\ B e. V ) /\ ( O e. On /\ ( bday " B ) C_ O ) ) -> ( bday ` T ) C_ O )