Metamath Proof Explorer

Theorem nosupbnd1lem3

Description: Lemma for nosupbnd1 . If U is a prolongment of S and in A , then ( Udom S ) is not 2o . (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 nosupbnd1lem3 
|- ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 2o )

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 1 nosupno 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
3 2 3ad2ant2 
 |-  ( ( -. E. x e. A A. y e. A -. x  S e. No )
4 nodmord 
 |-  ( S e. No -> Ord dom S )
5 ordirr 
 |-  ( Ord dom S -> -. dom S e. dom S )
6 3 4 5 3syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  -. dom S e. dom S )
7 simpl3l 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  U e. A )
8 ndmfv 
 |-  ( -. dom S e. dom U -> ( U ` dom S ) = (/) )
9 2on 
 |-  2o e. On
10 9 elexi 
 |-  2o e. _V
11 10 prid2 
 |-  2o e. { 1o , 2o }
12 11 nosgnn0i 
 |-  (/) =/= 2o
13 neeq1 
 |-  ( ( U ` dom S ) = (/) -> ( ( U ` dom S ) =/= 2o <-> (/) =/= 2o ) )
14 12 13 mpbiri 
 |-  ( ( U ` dom S ) = (/) -> ( U ` dom S ) =/= 2o )
15 14 neneqd 
 |-  ( ( U ` dom S ) = (/) -> -. ( U ` dom S ) = 2o )
16 8 15 syl 
 |-  ( -. dom S e. dom U -> -. ( U ` dom S ) = 2o )
17 16 con4i 
 |-  ( ( U ` dom S ) = 2o -> dom S e. dom U )
18 17 adantl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  dom S e. dom U )
19 simpl2l 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  A C_ No )
20 19 adantr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  A C_ No )
21 7 adantr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  U e. A )
22 20 21 sseldd 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  U e. No )
23 simprl 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  q e. A )
24 20 23 sseldd 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  q e. No )
25 3 adantr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  S e. No )
26 25 adantr 
 |-  ( ( ( ( -. 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 simpl3r 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) = S )
30 29 adantr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) = S )
31 simpll1 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  -. E. x e. A A. y e. A -. x
32 simpll2 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( A C_ No /\ A e. _V ) )
33 simpll3 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U e. A /\ ( U |` dom S ) = S ) )
34 simpr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( q e. A /\ -. q
35 1 nosupbnd1lem2 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( q |` dom S ) = S )
36 31 32 33 34 35 syl112anc 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( q |` dom S ) = S )
37 30 36 eqtr4d 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) = ( q |` dom S ) )
38 simplr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) = 2o )
39 simprr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  -. q
40 nolesgn2ores 
 |-  ( ( ( U e. No /\ q e. No /\ dom S e. On ) /\ ( ( U |` dom S ) = ( q |` dom S ) /\ ( U ` dom S ) = 2o ) /\ -. q  ( U |` suc dom S ) = ( q |` suc dom S ) )
41 22 24 28 37 38 39 40 syl321anc 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc dom S ) = ( q |` suc dom S ) )
42 41 expr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( -. q  ( U |` suc dom S ) = ( q |` suc dom S ) ) )
43 42 ralrimiva 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  A. q e. A ( -. q  ( U |` suc dom S ) = ( q |` suc dom S ) ) )
44 dmeq 
 |-  ( p = U -> dom p = dom U )
45 44 eleq2d 
 |-  ( p = U -> ( dom S e. dom p <-> dom S e. dom U ) )
46 breq2 
 |-  ( p = U -> ( q  q
47 46 notbid 
 |-  ( p = U -> ( -. q  -. q
48 reseq1 
 |-  ( p = U -> ( p |` suc dom S ) = ( U |` suc dom S ) )
49 48 eqeq1d 
 |-  ( p = U -> ( ( p |` suc dom S ) = ( q |` suc dom S ) <-> ( U |` suc dom S ) = ( q |` suc dom S ) ) )
50 47 49 imbi12d 
 |-  ( p = U -> ( ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) <-> ( -. q  ( U |` suc dom S ) = ( q |` suc dom S ) ) ) )
51 50 ralbidv 
 |-  ( p = U -> ( A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) <-> A. q e. A ( -. q  ( U |` suc dom S ) = ( q |` suc dom S ) ) ) )
52 45 51 anbi12d 
 |-  ( p = U -> ( ( dom S e. dom p /\ A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) <-> ( dom S e. dom U /\ A. q e. A ( -. q  ( U |` suc dom S ) = ( q |` suc dom S ) ) ) ) )
53 52 rspcev 
 |-  ( ( U e. A /\ ( dom S e. dom U /\ A. q e. A ( -. q  ( U |` suc dom S ) = ( q |` suc dom S ) ) ) ) -> E. p e. A ( dom S e. dom p /\ A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) )
54 7 18 43 53 syl12anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  E. p e. A ( dom S e. dom p /\ A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) )
55 1 nosupdm 
 |-  ( -. E. x e. A A. y e. A -. x  dom S = { z | E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) } )
56 55 eleq2d 
 |-  ( -. E. x e. A A. y e. A -. x  ( dom S e. dom S <-> dom S e. { z | E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) } ) )
57 56 3ad2ant1 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( dom S e. dom S <-> dom S e. { z | E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) } ) )
58 eleq1 
 |-  ( z = dom S -> ( z e. dom p <-> dom S e. dom p ) )
59 suceq 
 |-  ( z = dom S -> suc z = suc dom S )
60 59 reseq2d 
 |-  ( z = dom S -> ( p |` suc z ) = ( p |` suc dom S ) )
61 59 reseq2d 
 |-  ( z = dom S -> ( q |` suc z ) = ( q |` suc dom S ) )
62 60 61 eqeq12d 
 |-  ( z = dom S -> ( ( p |` suc z ) = ( q |` suc z ) <-> ( p |` suc dom S ) = ( q |` suc dom S ) ) )
63 62 imbi2d 
 |-  ( z = dom S -> ( ( -. q  ( p |` suc z ) = ( q |` suc z ) ) <-> ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) )
64 63 ralbidv 
 |-  ( z = dom S -> ( A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) <-> A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) )
65 58 64 anbi12d 
 |-  ( z = dom S -> ( ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) <-> ( dom S e. dom p /\ A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) ) )
66 65 rexbidv 
 |-  ( z = dom S -> ( E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) <-> E. p e. A ( dom S e. dom p /\ A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) ) )
67 66 elabg 
 |-  ( dom S e. On -> ( dom S e. { z | E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) } <-> E. p e. A ( dom S e. dom p /\ A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) ) )
68 3 27 67 3syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( dom S e. { z | E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) } <-> E. p e. A ( dom S e. dom p /\ A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) ) )
69 57 68 bitrd 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( dom S e. dom S <-> E. p e. A ( dom S e. dom p /\ A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) ) )
70 69 adantr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( dom S e. dom S <-> E. p e. A ( dom S e. dom p /\ A. q e. A ( -. q  ( p |` suc dom S ) = ( q |` suc dom S ) ) ) ) )
71 54 70 mpbird 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  dom S e. dom S )
72 6 71 mtand 
 |-  ( ( -. E. x e. A A. y e. A -. x  -. ( U ` dom S ) = 2o )
73 72 neqned 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 2o )