Metamath Proof Explorer


Theorem nosupbnd1lem4

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

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 simpl1
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. E. x e. A A. y e. A -. x 
3 simpl2
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( A C_ No /\ A e. _V ) )
4 simprl
 |-  ( ( ( -. E. x e. A A. y e. A -. x  w e. A )
5 simpl3
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U e. A /\ ( U |` dom S ) = S ) )
6 simprr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  U 
7 simp2l
 |-  ( ( -. E. x e. A A. y e. A -. x  A C_ No )
8 simp3l
 |-  ( ( -. E. x e. A A. y e. A -. x  U e. A )
9 7 8 sseldd
 |-  ( ( -. E. x e. A A. y e. A -. x  U e. No )
10 simpl2l
 |-  ( ( ( -. E. x e. A A. y e. A -. x  A C_ No )
11 10 4 sseldd
 |-  ( ( ( -. E. x e. A A. y e. A -. x  w e. No )
12 sltso
 |-  
13 soasym
 |-  ( (  ( U  -. w 
14 12 13 mpan
 |-  ( ( U e. No /\ w e. No ) -> ( U  -. w 
15 9 11 14 syl2an2r
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U  -. w 
16 6 15 mpd
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. w 
17 4 16 jca
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( w e. A /\ -. w 
18 1 nosupbnd1lem2
 |-  ( ( -. E. x e. A A. y e. A -. x  ( w |` dom S ) = S )
19 2 3 5 17 18 syl112anc
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( w |` dom S ) = S )
20 1 nosupbnd1lem3
 |-  ( ( -. E. x e. A A. y e. A -. x  ( w ` dom S ) =/= 2o )
21 2 3 4 19 20 syl112anc
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( w ` dom S ) =/= 2o )
22 21 neneqd
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( w ` dom S ) = 2o )
23 22 expr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U  -. ( w ` dom S ) = 2o ) )
24 imnan
 |-  ( ( U  -. ( w ` dom S ) = 2o ) <-> -. ( U 
25 23 24 sylib
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( U 
26 25 nrexdv
 |-  ( ( -. E. x e. A A. y e. A -. x  -. E. w e. A ( U 
27 simpl3l
 |-  ( ( ( -. E. x e. A A. y e. A -. x  U e. A )
28 simpl1
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. E. x e. A A. y e. A -. x 
29 breq2
 |-  ( w = y -> ( u  u 
30 29 cbvrexvw
 |-  ( E. w e. A u  E. y e. A u 
31 breq1
 |-  ( u = x -> ( u  x 
32 31 rexbidv
 |-  ( u = x -> ( E. y e. A u  E. y e. A x 
33 30 32 syl5bb
 |-  ( u = x -> ( E. w e. A u  E. y e. A x 
34 33 cbvralvw
 |-  ( A. u e. A E. w e. A u  A. x e. A E. y e. A x 
35 dfrex2
 |-  ( E. y e. A x  -. A. y e. A -. x 
36 35 ralbii
 |-  ( A. x e. A E. y e. A x  A. x e. A -. A. y e. A -. x 
37 ralnex
 |-  ( A. x e. A -. A. y e. A -. x  -. E. x e. A A. y e. A -. x 
38 34 36 37 3bitri
 |-  ( A. u e. A E. w e. A u  -. E. x e. A A. y e. A -. x 
39 28 38 sylibr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  A. u e. A E. w e. A u 
40 breq1
 |-  ( u = U -> ( u  U 
41 40 rexbidv
 |-  ( u = U -> ( E. w e. A u  E. w e. A U 
42 41 rspcv
 |-  ( U e. A -> ( A. u e. A E. w e. A u  E. w e. A U 
43 27 39 42 sylc
 |-  ( ( ( -. E. x e. A A. y e. A -. x  E. w e. A U 
44 simpl2l
 |-  ( ( ( -. E. x e. A A. y e. A -. x  A C_ No )
45 44 27 sseldd
 |-  ( ( ( -. E. x e. A A. y e. A -. x  U e. No )
46 45 adantr
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  U e. No )
47 44 adantr
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  A C_ No )
48 simprl
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  w e. A )
49 47 48 sseldd
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  w e. No )
50 1 nosupno
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
51 50 3ad2ant2
 |-  ( ( -. E. x e. A A. y e. A -. x  S e. No )
52 51 adantr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  S e. No )
53 52 adantr
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  S e. No )
54 nodmon
 |-  ( S e. No -> dom S e. On )
55 53 54 syl
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  dom S e. On )
56 simpl3r
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) = S )
57 56 adantr
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) = S )
58 simpll1
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  -. E. x e. A A. y e. A -. x 
59 simpll2
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( A C_ No /\ A e. _V ) )
60 simpll3
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U e. A /\ ( U |` dom S ) = S ) )
61 simprr
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  U 
62 45 49 14 syl2an2r
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U  -. w 
63 61 62 mpd
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  -. w 
64 48 63 jca
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( w e. A /\ -. w 
65 58 59 60 64 18 syl112anc
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( w |` dom S ) = S )
66 57 65 eqtr4d
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) = ( w |` dom S ) )
67 simplr
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) = (/) )
68 nolt02o
 |-  ( ( ( U e. No /\ w e. No /\ dom S e. On ) /\ ( ( U |` dom S ) = ( w |` dom S ) /\ U  ( w ` dom S ) = 2o )
69 46 49 55 66 61 67 68 syl321anc
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( w ` dom S ) = 2o )
70 69 expr
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U  ( w ` dom S ) = 2o ) )
71 70 ancld
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( U  ( U 
72 71 reximdva
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( E. w e. A U  E. w e. A ( U 
73 43 72 mpd
 |-  ( ( ( -. E. x e. A A. y e. A -. x  E. w e. A ( U 
74 26 73 mtand
 |-  ( ( -. E. x e. A A. y e. A -. x  -. ( U ` dom S ) = (/) )
75 74 neqned
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U ` dom S ) =/= (/) )