Metamath Proof Explorer

Theorem noinfbnd1lem5

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

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 1 noinfno 
 |-  ( ( B C_ No /\ B e. V ) -> T e. No )
3 2 3ad2ant2 
 |-  ( ( -. E. x e. B A. y e. B -. y  T e. No )
4 3 adantl 
 |-  ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  T e. No )
5 nodmord 
 |-  ( T e. No -> Ord dom T )
6 4 5 syl 
 |-  ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  Ord dom T )
7 ordirr 
 |-  ( Ord dom T -> -. dom T e. dom T )
8 6 7 syl 
 |-  ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  -. dom T e. dom T )
9 simpr3l 
 |-  ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  U e. B )
10 9 adantr 
 |-  ( ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  U e. B )
11 ndmfv 
 |-  ( -. dom T e. dom U -> ( U ` dom T ) = (/) )
12 2on0 
 |-  2o =/= (/)
13 12 necomi 
 |-  (/) =/= 2o
14 neeq1 
 |-  ( ( U ` dom T ) = (/) -> ( ( U ` dom T ) =/= 2o <-> (/) =/= 2o ) )
15 13 14 mpbiri 
 |-  ( ( U ` dom T ) = (/) -> ( U ` dom T ) =/= 2o )
16 11 15 syl 
 |-  ( -. dom T e. dom U -> ( U ` dom T ) =/= 2o )
17 16 neneqd 
 |-  ( -. dom T e. dom U -> -. ( U ` dom T ) = 2o )
18 17 con4i 
 |-  ( ( U ` dom T ) = 2o -> dom T e. dom U )
19 18 adantl 
 |-  ( ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  dom T e. dom U )
20 simpl2l 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  B C_ No )
21 20 adantr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  B C_ No )
22 simpl3l 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  U e. B )
23 22 adantr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  U e. B )
24 21 23 sseldd 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  U e. No )
25 nofun 
 |-  ( U e. No -> Fun U )
26 24 25 syl 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  Fun U )
27 simprll 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  z e. B )
28 21 27 sseldd 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  z e. No )
29 nofun 
 |-  ( z e. No -> Fun z )
30 28 29 syl 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  Fun z )
31 simpl3r 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` dom T ) = T )
32 31 adantr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( U |` dom T ) = T )
33 simpll1 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  -. E. x e. B A. y e. B -. y
34 simpll2 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( B C_ No /\ B e. V ) )
35 simpll3 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( U e. B /\ ( U |` dom T ) = T ) )
36 simprl 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( z e. B /\ -. U
37 1 noinfbnd1lem2 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( z |` dom T ) = T )
38 33 34 35 36 37 syl112anc 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( z |` dom T ) = T )
39 32 38 eqtr4d 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( U |` dom T ) = ( z |` dom T ) )
40 simplr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( U ` dom T ) = 2o )
41 40 18 syl 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  dom T e. dom U )
42 simprr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( z ` dom T ) = 2o )
43 ndmfv 
 |-  ( -. dom T e. dom z -> ( z ` dom T ) = (/) )
44 neeq1 
 |-  ( ( z ` dom T ) = (/) -> ( ( z ` dom T ) =/= 2o <-> (/) =/= 2o ) )
45 13 44 mpbiri 
 |-  ( ( z ` dom T ) = (/) -> ( z ` dom T ) =/= 2o )
46 43 45 syl 
 |-  ( -. dom T e. dom z -> ( z ` dom T ) =/= 2o )
47 46 neneqd 
 |-  ( -. dom T e. dom z -> -. ( z ` dom T ) = 2o )
48 47 con4i 
 |-  ( ( z ` dom T ) = 2o -> dom T e. dom z )
49 42 48 syl 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  dom T e. dom z )
50 40 42 eqtr4d 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( U ` dom T ) = ( z ` dom T ) )
51 eqfunressuc 
 |-  ( ( ( Fun U /\ Fun z ) /\ ( U |` dom T ) = ( z |` dom T ) /\ ( dom T e. dom U /\ dom T e. dom z /\ ( U ` dom T ) = ( z ` dom T ) ) ) -> ( U |` suc dom T ) = ( z |` suc dom T ) )
52 26 30 39 41 49 50 51 syl213anc 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( U |` suc dom T ) = ( z |` suc dom T ) )
53 52 expr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( ( z ` dom T ) = 2o -> ( U |` suc dom T ) = ( z |` suc dom T ) ) )
54 53 expr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( -. U  ( ( z ` dom T ) = 2o -> ( U |` suc dom T ) = ( z |` suc dom T ) ) ) )
55 54 a2d 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( ( -. U  ( z ` dom T ) = 2o ) -> ( -. U  ( U |` suc dom T ) = ( z |` suc dom T ) ) ) )
56 55 ralimdva 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) -> A. z e. B ( -. U  ( U |` suc dom T ) = ( z |` suc dom T ) ) ) )
57 56 impcom 
 |-  ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( ( -. E. x e. B A. y e. B -. y  A. z e. B ( -. U  ( U |` suc dom T ) = ( z |` suc dom T ) ) )
58 57 anassrs 
 |-  ( ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  A. z e. B ( -. U  ( U |` suc dom T ) = ( z |` suc dom T ) ) )
59 dmeq 
 |-  ( p = U -> dom p = dom U )
60 59 eleq2d 
 |-  ( p = U -> ( dom T e. dom p <-> dom T e. dom U ) )
61 breq1 
 |-  ( p = U -> ( p  U
62 61 notbid 
 |-  ( p = U -> ( -. p  -. U
63 reseq1 
 |-  ( p = U -> ( p |` suc dom T ) = ( U |` suc dom T ) )
64 63 eqeq1d 
 |-  ( p = U -> ( ( p |` suc dom T ) = ( z |` suc dom T ) <-> ( U |` suc dom T ) = ( z |` suc dom T ) ) )
65 62 64 imbi12d 
 |-  ( p = U -> ( ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) <-> ( -. U  ( U |` suc dom T ) = ( z |` suc dom T ) ) ) )
66 65 ralbidv 
 |-  ( p = U -> ( A. z e. B ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) <-> A. z e. B ( -. U  ( U |` suc dom T ) = ( z |` suc dom T ) ) ) )
67 60 66 anbi12d 
 |-  ( p = U -> ( ( dom T e. dom p /\ A. z e. B ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) ) <-> ( dom T e. dom U /\ A. z e. B ( -. U  ( U |` suc dom T ) = ( z |` suc dom T ) ) ) ) )
68 67 rspcev 
 |-  ( ( U e. B /\ ( dom T e. dom U /\ A. z e. B ( -. U  ( U |` suc dom T ) = ( z |` suc dom T ) ) ) ) -> E. p e. B ( dom T e. dom p /\ A. z e. B ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) ) )
69 10 19 58 68 syl12anc 
 |-  ( ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  E. p e. B ( dom T e. dom p /\ A. z e. B ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) ) )
70 nodmon 
 |-  ( T e. No -> dom T e. On )
71 4 70 syl 
 |-  ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  dom T e. On )
72 71 adantr 
 |-  ( ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  dom T e. On )
73 eleq1 
 |-  ( a = dom T -> ( a e. dom p <-> dom T e. dom p ) )
74 suceq 
 |-  ( a = dom T -> suc a = suc dom T )
75 74 reseq2d 
 |-  ( a = dom T -> ( p |` suc a ) = ( p |` suc dom T ) )
76 74 reseq2d 
 |-  ( a = dom T -> ( z |` suc a ) = ( z |` suc dom T ) )
77 75 76 eqeq12d 
 |-  ( a = dom T -> ( ( p |` suc a ) = ( z |` suc a ) <-> ( p |` suc dom T ) = ( z |` suc dom T ) ) )
78 77 imbi2d 
 |-  ( a = dom T -> ( ( -. p  ( p |` suc a ) = ( z |` suc a ) ) <-> ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) ) )
79 78 ralbidv 
 |-  ( a = dom T -> ( A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) <-> A. z e. B ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) ) )
80 73 79 anbi12d 
 |-  ( a = dom T -> ( ( a e. dom p /\ A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) ) <-> ( dom T e. dom p /\ A. z e. B ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) ) ) )
81 80 rexbidv 
 |-  ( a = dom T -> ( E. p e. B ( a e. dom p /\ A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) ) <-> E. p e. B ( dom T e. dom p /\ A. z e. B ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) ) ) )
82 81 elabg 
 |-  ( dom T e. On -> ( dom T e. { a | E. p e. B ( a e. dom p /\ A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) ) } <-> E. p e. B ( dom T e. dom p /\ A. z e. B ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) ) ) )
83 72 82 syl 
 |-  ( ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  ( dom T e. { a | E. p e. B ( a e. dom p /\ A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) ) } <-> E. p e. B ( dom T e. dom p /\ A. z e. B ( -. p  ( p |` suc dom T ) = ( z |` suc dom T ) ) ) ) )
84 69 83 mpbird 
 |-  ( ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  dom T e. { a | E. p e. B ( a e. dom p /\ A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) ) } )
85 1 noinfdm 
 |-  ( -. E. x e. B A. y e. B -. y  dom T = { a | E. p e. B ( a e. dom p /\ A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) ) } )
86 85 3ad2ant1 
 |-  ( ( -. E. x e. B A. y e. B -. y  dom T = { a | E. p e. B ( a e. dom p /\ A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) ) } )
87 86 adantl 
 |-  ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  dom T = { a | E. p e. B ( a e. dom p /\ A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) ) } )
88 87 adantr 
 |-  ( ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  dom T = { a | E. p e. B ( a e. dom p /\ A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) ) } )
89 88 eleq2d 
 |-  ( ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  ( dom T e. dom T <-> dom T e. { a | E. p e. B ( a e. dom p /\ A. z e. B ( -. p  ( p |` suc a ) = ( z |` suc a ) ) ) } ) )
90 84 89 mpbird 
 |-  ( ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  dom T e. dom T )
91 8 90 mtand 
 |-  ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  -. ( U ` dom T ) = 2o )
92 91 neqned 
 |-  ( ( A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  ( U ` dom T ) =/= 2o )
93 rexanali 
 |-  ( E. z e. B ( -. U  -. A. z e. B ( -. U  ( z ` dom T ) = 2o ) )
94 simpr1 
 |-  ( ( ( ( z e. B /\ -. U  -. E. x e. B A. y e. B -. y
95 simpr2 
 |-  ( ( ( ( z e. B /\ -. U  ( B C_ No /\ B e. V ) )
96 simplll 
 |-  ( ( ( ( z e. B /\ -. U  z e. B )
97 simpr3 
 |-  ( ( ( ( z e. B /\ -. U  ( U e. B /\ ( U |` dom T ) = T ) )
98 simpll 
 |-  ( ( ( ( z e. B /\ -. U  ( z e. B /\ -. U
99 94 95 97 98 37 syl112anc 
 |-  ( ( ( ( z e. B /\ -. U  ( z |` dom T ) = T )
100 1 noinfbnd1lem4 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( z ` dom T ) =/= (/) )
101 94 95 96 99 100 syl112anc 
 |-  ( ( ( ( z e. B /\ -. U  ( z ` dom T ) =/= (/) )
102 101 neneqd 
 |-  ( ( ( ( z e. B /\ -. U  -. ( z ` dom T ) = (/) )
103 102 pm2.21d 
 |-  ( ( ( ( z e. B /\ -. U  ( ( z ` dom T ) = (/) -> ( U ` dom T ) =/= 2o ) )
104 1 noinfbnd1lem3 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( z ` dom T ) =/= 1o )
105 94 95 96 99 104 syl112anc 
 |-  ( ( ( ( z e. B /\ -. U  ( z ` dom T ) =/= 1o )
106 105 neneqd 
 |-  ( ( ( ( z e. B /\ -. U  -. ( z ` dom T ) = 1o )
107 106 pm2.21d 
 |-  ( ( ( ( z e. B /\ -. U  ( ( z ` dom T ) = 1o -> ( U ` dom T ) =/= 2o ) )
108 simplr 
 |-  ( ( ( ( z e. B /\ -. U  -. ( z ` dom T ) = 2o )
109 simpr2l 
 |-  ( ( ( ( z e. B /\ -. U  B C_ No )
110 109 96 sseldd 
 |-  ( ( ( ( z e. B /\ -. U  z e. No )
111 nofv 
 |-  ( z e. No -> ( ( z ` dom T ) = (/) \/ ( z ` dom T ) = 1o \/ ( z ` dom T ) = 2o ) )
112 110 111 syl 
 |-  ( ( ( ( z e. B /\ -. U  ( ( z ` dom T ) = (/) \/ ( z ` dom T ) = 1o \/ ( z ` dom T ) = 2o ) )
113 3orel3 
 |-  ( -. ( z ` dom T ) = 2o -> ( ( ( z ` dom T ) = (/) \/ ( z ` dom T ) = 1o \/ ( z ` dom T ) = 2o ) -> ( ( z ` dom T ) = (/) \/ ( z ` dom T ) = 1o ) ) )
114 108 112 113 sylc 
 |-  ( ( ( ( z e. B /\ -. U  ( ( z ` dom T ) = (/) \/ ( z ` dom T ) = 1o ) )
115 103 107 114 mpjaod 
 |-  ( ( ( ( z e. B /\ -. U  ( U ` dom T ) =/= 2o )
116 115 ex 
 |-  ( ( ( z e. B /\ -. U  ( ( -. E. x e. B A. y e. B -. y  ( U ` dom T ) =/= 2o ) )
117 116 anasss 
 |-  ( ( z e. B /\ ( -. U  ( ( -. E. x e. B A. y e. B -. y  ( U ` dom T ) =/= 2o ) )
118 117 rexlimiva 
 |-  ( E. z e. B ( -. U  ( ( -. E. x e. B A. y e. B -. y  ( U ` dom T ) =/= 2o ) )
119 118 imp 
 |-  ( ( E. z e. B ( -. U  ( U ` dom T ) =/= 2o )
120 93 119 sylanbr 
 |-  ( ( -. A. z e. B ( -. U  ( z ` dom T ) = 2o ) /\ ( -. E. x e. B A. y e. B -. y  ( U ` dom T ) =/= 2o )
121 92 120 pm2.61ian 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U ` dom T ) =/= 2o )