Metamath Proof Explorer

Theorem noinfbnd1lem4

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

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 simpl1 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  -. E. x e. B A. y e. B -. y
3 simpl2 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( B C_ No /\ B e. V ) )
4 simprl 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  w e. B )
5 simpl3 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U e. B /\ ( U |` dom T ) = T ) )
6 simp2l 
 |-  ( ( -. E. x e. B A. y e. B -. y  B C_ No )
7 6 sselda 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  w e. No )
8 simp3l 
 |-  ( ( -. E. x e. B A. y e. B -. y  U e. B )
9 6 8 sseldd 
 |-  ( ( -. E. x e. B A. y e. B -. y  U e. No )
10 9 adantr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  U e. No )
11 sltso 
 |-
12 soasym 
 |-  ( (  ( w  -. U
13 11 12 mpan 
 |-  ( ( w e. No /\ U e. No ) -> ( w  -. U
14 7 10 13 syl2anc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( w  -. U
15 14 impr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  -. U
16 4 15 jca 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( w e. B /\ -. U
17 1 noinfbnd1lem2 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( w |` dom T ) = T )
18 2 3 5 16 17 syl112anc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( w |` dom T ) = T )
19 1 noinfbnd1lem3 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( w ` dom T ) =/= 1o )
20 2 3 4 18 19 syl112anc 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( w ` dom T ) =/= 1o )
21 20 neneqd 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  -. ( w ` dom T ) = 1o )
22 21 expr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( w  -. ( w ` dom T ) = 1o ) )
23 imnan 
 |-  ( ( w  -. ( w ` dom T ) = 1o ) <-> -. ( w
24 22 23 sylib 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  -. ( w
25 24 nrexdv 
 |-  ( ( -. E. x e. B A. y e. B -. y  -. E. w e. B ( w
26 breq2 
 |-  ( x = U -> ( y  y
27 26 rexbidv 
 |-  ( x = U -> ( E. y e. B y  E. y e. B y
28 simpl1 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  -. E. x e. B A. y e. B -. y
29 dfral2 
 |-  ( A. x e. B E. y e. B y  -. E. x e. B -. E. y e. B y
30 ralnex 
 |-  ( A. y e. B -. y  -. E. y e. B y
31 30 rexbii 
 |-  ( E. x e. B A. y e. B -. y  E. x e. B -. E. y e. B y
32 29 31 xchbinxr 
 |-  ( A. x e. B E. y e. B y  -. E. x e. B A. y e. B -. y
33 28 32 sylibr 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  A. x e. B E. y e. B y
34 simpl3l 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  U e. B )
35 27 33 34 rspcdva 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  E. y e. B y
36 breq1 
 |-  ( y = w -> ( y  w
37 36 cbvrexvw 
 |-  ( E. y e. B y  E. w e. B w
38 35 37 sylib 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  E. w e. B w
39 simpl2l 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  B C_ No )
40 39 adantr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  B C_ No )
41 simprl 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  w e. B )
42 40 41 sseldd 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  w e. No )
43 34 adantr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  U e. B )
44 40 43 sseldd 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  U e. No )
45 simpl2 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( B C_ No /\ B e. V ) )
46 1 noinfno 
 |-  ( ( B C_ No /\ B e. V ) -> T e. No )
47 45 46 syl 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  T e. No )
48 47 adantr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  T e. No )
49 nodmon 
 |-  ( T e. No -> dom T e. On )
50 48 49 syl 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  dom T e. On )
51 simpll1 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  -. E. x e. B A. y e. B -. y
52 simpll2 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( B C_ No /\ B e. V ) )
53 simpll3 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( U e. B /\ ( U |` dom T ) = T ) )
54 simprr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  w
55 42 44 13 syl2anc 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( w  -. U
56 54 55 mpd 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  -. U
57 41 56 jca 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( w e. B /\ -. U
58 51 52 53 57 17 syl112anc 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( w |` dom T ) = T )
59 simpl3r 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( U |` dom T ) = T )
60 59 adantr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( U |` dom T ) = T )
61 58 60 eqtr4d 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( w |` dom T ) = ( U |` dom T ) )
62 simplr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( U ` dom T ) = (/) )
63 nogt01o 
 |-  ( ( ( w e. No /\ U e. No /\ dom T e. On ) /\ ( ( w |` dom T ) = ( U |` dom T ) /\ w  ( w ` dom T ) = 1o )
64 42 44 50 61 54 62 63 syl321anc 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( w ` dom T ) = 1o )
65 64 expr 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( w  ( w ` dom T ) = 1o ) )
66 65 ancld 
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( w  ( w
67 66 reximdva 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( E. w e. B w  E. w e. B ( w
68 38 67 mpd 
 |-  ( ( ( -. E. x e. B A. y e. B -. y  E. w e. B ( w
69 25 68 mtand 
 |-  ( ( -. E. x e. B A. y e. B -. y  -. ( U ` dom T ) = (/) )
70 69 neqned 
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U ` dom T ) =/= (/) )