Metamath Proof Explorer

Theorem nosupbnd1lem5

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

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 3 adantl 
 |-  ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  S e. No )
5 nodmord 
 |-  ( S e. No -> Ord dom S )
6 ordirr 
 |-  ( Ord dom S -> -. dom S e. dom S )
7 4 5 6 3syl 
 |-  ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  -. dom S e. dom S )
8 simpr3l 
 |-  ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  U e. A )
9 8 adantr 
 |-  ( ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  U e. A )
10 ndmfv 
 |-  ( -. dom S e. dom U -> ( U ` dom S ) = (/) )
11 1oex 
 |-  1o e. _V
12 11 prid1 
 |-  1o e. { 1o , 2o }
13 12 nosgnn0i 
 |-  (/) =/= 1o
14 neeq1 
 |-  ( ( U ` dom S ) = (/) -> ( ( U ` dom S ) =/= 1o <-> (/) =/= 1o ) )
15 13 14 mpbiri 
 |-  ( ( U ` dom S ) = (/) -> ( U ` dom S ) =/= 1o )
16 15 neneqd 
 |-  ( ( U ` dom S ) = (/) -> -. ( U ` dom S ) = 1o )
17 10 16 syl 
 |-  ( -. dom S e. dom U -> -. ( U ` dom S ) = 1o )
18 17 con4i 
 |-  ( ( U ` dom S ) = 1o -> dom S e. dom U )
19 18 adantl 
 |-  ( ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  dom S e. dom U )
20 simp2l 
 |-  ( ( -. E. x e. A A. y e. A -. x  A C_ No )
21 simp3l 
 |-  ( ( -. 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 22 adantr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  U e. No )
24 23 adantr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  U e. No )
25 nofun 
 |-  ( U e. No -> Fun U )
26 24 25 syl 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  Fun U )
27 simpl2l 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  A C_ No )
28 simpll 
 |-  ( ( ( z e. A /\ -. z  z e. A )
29 ssel2 
 |-  ( ( A C_ No /\ z e. A ) -> z e. No )
30 27 28 29 syl2an 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  z e. No )
31 nofun 
 |-  ( z e. No -> Fun z )
32 30 31 syl 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  Fun z )
33 simpl3r 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) = S )
34 33 adantr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) = S )
35 simpll1 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  -. E. x e. A A. y e. A -. x
36 simpll2 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( A C_ No /\ A e. _V ) )
37 simpll3 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U e. A /\ ( U |` dom S ) = S ) )
38 simprl 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( z e. A /\ -. z
39 1 nosupbnd1lem2 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( z |` dom S ) = S )
40 35 36 37 38 39 syl112anc 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( z |` dom S ) = S )
41 34 40 eqtr4d 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) = ( z |` dom S ) )
42 18 adantl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  dom S e. dom U )
43 42 adantr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  dom S e. dom U )
44 ndmfv 
 |-  ( -. dom S e. dom z -> ( z ` dom S ) = (/) )
45 neeq1 
 |-  ( ( z ` dom S ) = (/) -> ( ( z ` dom S ) =/= 1o <-> (/) =/= 1o ) )
46 13 45 mpbiri 
 |-  ( ( z ` dom S ) = (/) -> ( z ` dom S ) =/= 1o )
47 46 neneqd 
 |-  ( ( z ` dom S ) = (/) -> -. ( z ` dom S ) = 1o )
48 44 47 syl 
 |-  ( -. dom S e. dom z -> -. ( z ` dom S ) = 1o )
49 48 con4i 
 |-  ( ( z ` dom S ) = 1o -> dom S e. dom z )
50 49 adantl 
 |-  ( ( ( z e. A /\ -. z  dom S e. dom z )
51 50 adantl 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  dom S e. dom z )
52 simplr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) = 1o )
53 simprr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( z ` dom S ) = 1o )
54 52 53 eqtr4d 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) = ( z ` dom S ) )
55 eqfunressuc 
 |-  ( ( ( Fun U /\ Fun z ) /\ ( U |` dom S ) = ( z |` dom S ) /\ ( dom S e. dom U /\ dom S e. dom z /\ ( U ` dom S ) = ( z ` dom S ) ) ) -> ( U |` suc dom S ) = ( z |` suc dom S ) )
56 26 32 41 43 51 54 55 syl213anc 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc dom S ) = ( z |` suc dom S ) )
57 56 expr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( ( z ` dom S ) = 1o -> ( U |` suc dom S ) = ( z |` suc dom S ) ) )
58 57 expr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( -. z  ( ( z ` dom S ) = 1o -> ( U |` suc dom S ) = ( z |` suc dom S ) ) ) )
59 58 a2d 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( ( -. z  ( z ` dom S ) = 1o ) -> ( -. z  ( U |` suc dom S ) = ( z |` suc dom S ) ) ) )
60 59 ralimdva 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) -> A. z e. A ( -. z  ( U |` suc dom S ) = ( z |` suc dom S ) ) ) )
61 60 impcom 
 |-  ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( ( -. E. x e. A A. y e. A -. x  A. z e. A ( -. z  ( U |` suc dom S ) = ( z |` suc dom S ) ) )
62 61 anassrs 
 |-  ( ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  A. z e. A ( -. z  ( U |` suc dom S ) = ( z |` suc dom S ) ) )
63 dmeq 
 |-  ( p = U -> dom p = dom U )
64 63 eleq2d 
 |-  ( p = U -> ( dom S e. dom p <-> dom S e. dom U ) )
65 breq2 
 |-  ( p = U -> ( z  z
66 65 notbid 
 |-  ( p = U -> ( -. z  -. z
67 reseq1 
 |-  ( p = U -> ( p |` suc dom S ) = ( U |` suc dom S ) )
68 67 eqeq1d 
 |-  ( p = U -> ( ( p |` suc dom S ) = ( z |` suc dom S ) <-> ( U |` suc dom S ) = ( z |` suc dom S ) ) )
69 66 68 imbi12d 
 |-  ( p = U -> ( ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) <-> ( -. z  ( U |` suc dom S ) = ( z |` suc dom S ) ) ) )
70 69 ralbidv 
 |-  ( p = U -> ( A. z e. A ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) <-> A. z e. A ( -. z  ( U |` suc dom S ) = ( z |` suc dom S ) ) ) )
71 64 70 anbi12d 
 |-  ( p = U -> ( ( dom S e. dom p /\ A. z e. A ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) ) <-> ( dom S e. dom U /\ A. z e. A ( -. z  ( U |` suc dom S ) = ( z |` suc dom S ) ) ) ) )
72 71 rspcev 
 |-  ( ( U e. A /\ ( dom S e. dom U /\ A. z e. A ( -. z  ( U |` suc dom S ) = ( z |` suc dom S ) ) ) ) -> E. p e. A ( dom S e. dom p /\ A. z e. A ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) ) )
73 9 19 62 72 syl12anc 
 |-  ( ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  E. p e. A ( dom S e. dom p /\ A. z e. A ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) ) )
74 simplr1 
 |-  ( ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  -. E. x e. A A. y e. A -. x
75 1 nosupdm 
 |-  ( -. E. x e. A A. y e. A -. x  dom S = { a | E. p e. A ( a e. dom p /\ A. z e. A ( -. z  ( p |` suc a ) = ( z |` suc a ) ) ) } )
76 75 eleq2d 
 |-  ( -. E. x e. A A. y e. A -. x  ( dom S e. dom S <-> dom S e. { a | E. p e. A ( a e. dom p /\ A. z e. A ( -. z  ( p |` suc a ) = ( z |` suc a ) ) ) } ) )
77 74 76 syl 
 |-  ( ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  ( dom S e. dom S <-> dom S e. { a | E. p e. A ( a e. dom p /\ A. z e. A ( -. z  ( p |` suc a ) = ( z |` suc a ) ) ) } ) )
78 4 adantr 
 |-  ( ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  S e. No )
79 nodmon 
 |-  ( S e. No -> dom S e. On )
80 eleq1 
 |-  ( a = dom S -> ( a e. dom p <-> dom S e. dom p ) )
81 suceq 
 |-  ( a = dom S -> suc a = suc dom S )
82 81 reseq2d 
 |-  ( a = dom S -> ( p |` suc a ) = ( p |` suc dom S ) )
83 81 reseq2d 
 |-  ( a = dom S -> ( z |` suc a ) = ( z |` suc dom S ) )
84 82 83 eqeq12d 
 |-  ( a = dom S -> ( ( p |` suc a ) = ( z |` suc a ) <-> ( p |` suc dom S ) = ( z |` suc dom S ) ) )
85 84 imbi2d 
 |-  ( a = dom S -> ( ( -. z  ( p |` suc a ) = ( z |` suc a ) ) <-> ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) ) )
86 85 ralbidv 
 |-  ( a = dom S -> ( A. z e. A ( -. z  ( p |` suc a ) = ( z |` suc a ) ) <-> A. z e. A ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) ) )
87 80 86 anbi12d 
 |-  ( a = dom S -> ( ( a e. dom p /\ A. z e. A ( -. z  ( p |` suc a ) = ( z |` suc a ) ) ) <-> ( dom S e. dom p /\ A. z e. A ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) ) ) )
88 87 rexbidv 
 |-  ( a = dom S -> ( E. p e. A ( a e. dom p /\ A. z e. A ( -. z  ( p |` suc a ) = ( z |` suc a ) ) ) <-> E. p e. A ( dom S e. dom p /\ A. z e. A ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) ) ) )
89 88 elabg 
 |-  ( dom S e. On -> ( dom S e. { a | E. p e. A ( a e. dom p /\ A. z e. A ( -. z  ( p |` suc a ) = ( z |` suc a ) ) ) } <-> E. p e. A ( dom S e. dom p /\ A. z e. A ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) ) ) )
90 78 79 89 3syl 
 |-  ( ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  ( dom S e. { a | E. p e. A ( a e. dom p /\ A. z e. A ( -. z  ( p |` suc a ) = ( z |` suc a ) ) ) } <-> E. p e. A ( dom S e. dom p /\ A. z e. A ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) ) ) )
91 77 90 bitrd 
 |-  ( ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  ( dom S e. dom S <-> E. p e. A ( dom S e. dom p /\ A. z e. A ( -. z  ( p |` suc dom S ) = ( z |` suc dom S ) ) ) ) )
92 73 91 mpbird 
 |-  ( ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  dom S e. dom S )
93 7 92 mtand 
 |-  ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  -. ( U ` dom S ) = 1o )
94 93 neqned 
 |-  ( ( A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 1o )
95 rexanali 
 |-  ( E. z e. A ( -. z  -. A. z e. A ( -. z  ( z ` dom S ) = 1o ) )
96 simpl 
 |-  ( ( z e. A /\ -. z  z e. A )
97 20 96 29 syl2an 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  z e. No )
98 nofv 
 |-  ( z e. No -> ( ( z ` dom S ) = (/) \/ ( z ` dom S ) = 1o \/ ( z ` dom S ) = 2o ) )
99 97 98 syl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( z ` dom S ) = (/) \/ ( z ` dom S ) = 1o \/ ( z ` dom S ) = 2o ) )
100 3orel2 
 |-  ( -. ( z ` dom S ) = 1o -> ( ( ( z ` dom S ) = (/) \/ ( z ` dom S ) = 1o \/ ( z ` dom S ) = 2o ) -> ( ( z ` dom S ) = (/) \/ ( z ` dom S ) = 2o ) ) )
101 99 100 syl5com 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( -. ( z ` dom S ) = 1o -> ( ( z ` dom S ) = (/) \/ ( z ` dom S ) = 2o ) ) )
102 101 imdistanda 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( ( ( z e. A /\ -. z  ( ( z e. A /\ -. z
103 simpl1 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. E. x e. A A. y e. A -. x
104 simpl2 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( A C_ No /\ A e. _V ) )
105 simprl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  z e. A )
106 simpl3 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U e. A /\ ( U |` dom S ) = S ) )
107 simpr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( z e. A /\ -. z
108 103 104 106 107 39 syl112anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( z |` dom S ) = S )
109 1 nosupbnd1lem4 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( z ` dom S ) =/= (/) )
110 103 104 105 108 109 syl112anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( z ` dom S ) =/= (/) )
111 110 neneqd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( z ` dom S ) = (/) )
112 111 pm2.21d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( z ` dom S ) = (/) -> ( U ` dom S ) =/= 1o ) )
113 1 nosupbnd1lem3 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( z ` dom S ) =/= 2o )
114 103 104 105 108 113 syl112anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( z ` dom S ) =/= 2o )
115 114 neneqd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( z ` dom S ) = 2o )
116 115 pm2.21d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( z ` dom S ) = 2o -> ( U ` dom S ) =/= 1o ) )
117 112 116 jaod 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( ( z ` dom S ) = (/) \/ ( z ` dom S ) = 2o ) -> ( U ` dom S ) =/= 1o ) )
118 117 expimpd 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( ( ( z e. A /\ -. z  ( U ` dom S ) =/= 1o ) )
119 102 118 syldc 
 |-  ( ( ( z e. A /\ -. z  ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 1o ) )
120 119 anasss 
 |-  ( ( z e. A /\ ( -. z  ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 1o ) )
121 120 rexlimiva 
 |-  ( E. z e. A ( -. z  ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 1o ) )
122 121 imp 
 |-  ( ( E. z e. A ( -. z  ( U ` dom S ) =/= 1o )
123 95 122 sylanbr 
 |-  ( ( -. A. z e. A ( -. z  ( z ` dom S ) = 1o ) /\ ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 1o )
124 94 123 pm2.61ian 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= 1o )