Metamath Proof Explorer

Theorem noinfbnd1lem3

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

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