Theorem noinfbnd1lem6

Description: Lemma for noinfbnd1 . Establish a hard lower bound when there is no minimum. (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	noinfbnd1lem6	|- ( ( -. E. x e. B A. y e. B -. y 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		simp2l	|- ( ( -. E. x e. B A. y e. B -. y B C_ No )
3		simp3	|- ( ( -. E. x e. B A. y e. B -. y U e. B )
4	2 3	sseldd	|- ( ( -. E. x e. B A. y e. B -. y U e. No )
5		nofv	|- ( U e. No -> ( ( U ` dom T ) = (/) \/ ( U ` dom T ) = 1o \/ ( U ` dom T ) = 2o ) )
6	4 5	syl	|- ( ( -. E. x e. B A. y e. B -. y ( ( U ` dom T ) = (/) \/ ( U ` dom T ) = 1o \/ ( U ` dom T ) = 2o ) )
7		3oran	|- ( ( ( U ` dom T ) = (/) \/ ( U ` dom T ) = 1o \/ ( U ` dom T ) = 2o ) <-> -. ( -. ( U ` dom T ) = (/) /\ -. ( U ` dom T ) = 1o /\ -. ( U ` dom T ) = 2o ) )
8	6 7	sylib	|- ( ( -. E. x e. B A. y e. B -. y -. ( -. ( U ` dom T ) = (/) /\ -. ( U ` dom T ) = 1o /\ -. ( U ` dom T ) = 2o ) )
9		simpl1	|- ( ( ( -. E. x e. B A. y e. B -. y -. E. x e. B A. y e. B -. y
10		simpl2	|- ( ( ( -. E. x e. B A. y e. B -. y ( B C_ No /\ B e. V ) )
11		simpl3	|- ( ( ( -. E. x e. B A. y e. B -. y U e. B )
12		simpr	|- ( ( ( -. E. x e. B A. y e. B -. y T = ( U |` dom T ) )
13	12	eqcomd	|- ( ( ( -. E. x e. B A. y e. B -. y ( U |` dom T ) = T )
14	1	noinfbnd1lem4	|- ( ( -. E. x e. B A. y e. B -. y ( U ` dom T ) =/= (/) )
15	9 10 11 13 14	syl112anc	|- ( ( ( -. E. x e. B A. y e. B -. y ( U ` dom T ) =/= (/) )
16	15	neneqd	|- ( ( ( -. E. x e. B A. y e. B -. y -. ( U ` dom T ) = (/) )
17	1	noinfbnd1lem3	|- ( ( -. E. x e. B A. y e. B -. y ( U ` dom T ) =/= 1o )
18	9 10 11 13 17	syl112anc	|- ( ( ( -. E. x e. B A. y e. B -. y ( U ` dom T ) =/= 1o )
19	18	neneqd	|- ( ( ( -. E. x e. B A. y e. B -. y -. ( U ` dom T ) = 1o )
20	1	noinfbnd1lem5	|- ( ( -. E. x e. B A. y e. B -. y ( U ` dom T ) =/= 2o )
21	9 10 11 13 20	syl112anc	|- ( ( ( -. E. x e. B A. y e. B -. y ( U ` dom T ) =/= 2o )
22	21	neneqd	|- ( ( ( -. E. x e. B A. y e. B -. y -. ( U ` dom T ) = 2o )
23	16 19 22	3jca	|- ( ( ( -. E. x e. B A. y e. B -. y ( -. ( U ` dom T ) = (/) /\ -. ( U ` dom T ) = 1o /\ -. ( U ` dom T ) = 2o ) )
24	8 23	mtand	|- ( ( -. E. x e. B A. y e. B -. y -. T = ( U |` dom T ) )
25	1	noinfbnd1lem1	|- ( ( -. E. x e. B A. y e. B -. y -. ( U |` dom T )
26	1	noinfno	|- ( ( B C_ No /\ B e. V ) -> T e. No )
27	26	3ad2ant2	|- ( ( -. E. x e. B A. y e. B -. y T e. No )
28		nodmon	|- ( T e. No -> dom T e. On )
29	27 28	syl	|- ( ( -. E. x e. B A. y e. B -. y dom T e. On )
30		noreson	|- ( ( U e. No /\ dom T e. On ) -> ( U |` dom T ) e. No )
31	4 29 30	syl2anc	|- ( ( -. E. x e. B A. y e. B -. y ( U |` dom T ) e. No )
32		sltso	|-
33		solin	|- ( ( ( T
34	32 33	mpan	|- ( ( T e. No /\ ( U |` dom T ) e. No ) -> ( T
35	27 31 34	syl2anc	|- ( ( -. E. x e. B A. y e. B -. y ( T
36	24 25 35	ecase23d	|- ( ( -. E. x e. B A. y e. B -. y T