Metamath Proof Explorer

Theorem nosupbnd1lem2

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