Metamath Proof Explorer

Theorem nosupbnd1lem6

Description: Lemma for nosupbnd1 . Establish a hard upper bound when there is no maximum. (Contributed by Scott Fenton, 6-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 nosupbnd1lem6 
|- ( ( -. E. x e. A A. y e. A -. x  ( U |` dom 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 simp2l 
 |-  ( ( -. E. x e. A A. y e. A -. x  A C_ No )
3 simp3 
 |-  ( ( -. E. x e. A A. y e. A -. x  U e. A )
4 2 3 sseldd 
 |-  ( ( -. E. x e. A A. y e. A -. x  U e. No )
5 nofv 
 |-  ( U e. No -> ( ( U ` dom S ) = (/) \/ ( U ` dom S ) = 1o \/ ( U ` dom S ) = 2o ) )
6 4 5 syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( ( U ` dom S ) = (/) \/ ( U ` dom S ) = 1o \/ ( U ` dom S ) = 2o ) )
7 3oran 
 |-  ( ( ( U ` dom S ) = (/) \/ ( U ` dom S ) = 1o \/ ( U ` dom S ) = 2o ) <-> -. ( -. ( U ` dom S ) = (/) /\ -. ( U ` dom S ) = 1o /\ -. ( U ` dom S ) = 2o ) )
8 6 7 sylib 
 |-  ( ( -. E. x e. A A. y e. A -. x  -. ( -. ( U ` dom S ) = (/) /\ -. ( U ` dom S ) = 1o /\ -. ( U ` dom S ) = 2o ) )
9 simpl1 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. E. x e. A A. y e. A -. x
10 simpl2 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( A C_ No /\ A e. _V ) )
11 simpl3 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  U e. A )
12 simpr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) = S )
13 1 nosupbnd1lem4 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= (/) )
14 9 10 11 12 13 syl112anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= (/) )
15 14 neneqd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( U ` dom S ) = (/) )
16 1 nosupbnd1lem5 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 1o )
17 9 10 11 12 16 syl112anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 1o )
18 17 neneqd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( U ` dom S ) = 1o )
19 1 nosupbnd1lem3 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 2o )
20 9 10 11 12 19 syl112anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 2o )
21 20 neneqd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( U ` dom S ) = 2o )
22 15 18 21 3jca 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( -. ( U ` dom S ) = (/) /\ -. ( U ` dom S ) = 1o /\ -. ( U ` dom S ) = 2o ) )
23 8 22 mtand 
 |-  ( ( -. E. x e. A A. y e. A -. x  -. ( U |` dom S ) = S )
24 1 nosupbnd1lem1 
 |-  ( ( -. E. x e. A A. y e. A -. x  -. S
25 1 nosupno 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
26 25 3ad2ant2 
 |-  ( ( -. E. x e. A A. y e. A -. x  S e. No )
27 nodmon 
 |-  ( S e. No -> dom S e. On )
28 26 27 syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  dom S e. On )
29 noreson 
 |-  ( ( U e. No /\ dom S e. On ) -> ( U |` dom S ) e. No )
30 4 28 29 syl2anc 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) e. No )
31 sltso 
 |-
32 solin 
 |-  ( (  ( ( U |` dom S )
33 31 32 mpan 
 |-  ( ( ( U |` dom S ) e. No /\ S e. No ) -> ( ( U |` dom S )
34 30 26 33 syl2anc 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( ( U |` dom S )
35 23 24 34 ecase23d 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S )