Theorem noinfbnd1lem2

Description: Lemma for noinfbnd1 . When there is no minimum, if any member of B is a prolongment of T , then so are all elements below it. (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	noinfbnd1lem2	|- ( ( -. E. x e. B A. y e. B -. y ( W |` dom T ) = 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		simp3rl	|- ( ( -. E. x e. B A. y e. B -. y W e. B )
3	1	noinfbnd1lem1	|- ( ( -. E. x e. B A. y e. B -. y -. ( W |` dom T )
4	2 3	syld3an3	|- ( ( -. E. x e. B A. y e. B -. y -. ( W |` dom T )
5		simp3rr	|- ( ( -. E. x e. B A. y e. B -. y -. U
6		simp2l	|- ( ( -. E. x e. B A. y e. B -. y B C_ No )
7		simp3ll	|- ( ( -. E. x e. B A. y e. B -. y U e. B )
8	6 7	sseldd	|- ( ( -. E. x e. B A. y e. B -. y U e. No )
9	6 2	sseldd	|- ( ( -. E. x e. B A. y e. B -. y W e. No )
10	1	noinfno	|- ( ( B C_ No /\ B e. V ) -> T e. No )
11	10	3ad2ant2	|- ( ( -. E. x e. B A. y e. B -. y T e. No )
12		nodmon	|- ( T e. No -> dom T e. On )
13	11 12	syl	|- ( ( -. E. x e. B A. y e. B -. y dom T e. On )
14		sltres	|- ( ( U e. No /\ W e. No /\ dom T e. On ) -> ( ( U |` dom T ) U
15	8 9 13 14	syl3anc	|- ( ( -. E. x e. B A. y e. B -. y ( ( U |` dom T ) U
16	5 15	mtod	|- ( ( -. E. x e. B A. y e. B -. y -. ( U |` dom T )
17		simp3lr	|- ( ( -. E. x e. B A. y e. B -. y ( U |` dom T ) = T )
18	17	breq1d	|- ( ( -. E. x e. B A. y e. B -. y ( ( U |` dom T ) T
19	16 18	mtbid	|- ( ( -. E. x e. B A. y e. B -. y -. T
20		noreson	|- ( ( W e. No /\ dom T e. On ) -> ( W |` dom T ) e. No )
21	9 13 20	syl2anc	|- ( ( -. E. x e. B A. y e. B -. y ( W |` dom T ) e. No )
22		sltso	|-
23		sotrieq2	|- ( ( ( ( W |` dom T ) = T <-> ( -. ( W |` dom T )
24	22 23	mpan	|- ( ( ( W |` dom T ) e. No /\ T e. No ) -> ( ( W |` dom T ) = T <-> ( -. ( W |` dom T )
25	21 11 24	syl2anc	|- ( ( -. E. x e. B A. y e. B -. y ( ( W |` dom T ) = T <-> ( -. ( W |` dom T )
26	4 19 25	mpbir2and	|- ( ( -. E. x e. B A. y e. B -. y ( W |` dom T ) = T )