Metamath Proof Explorer


Theorem nosupbnd2

Description: Bounding law from above for the surreal supremum. Proposition 4.3 of Lipparini p. 6. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Hypothesis nosupbnd2.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 nosupbnd2
|- ( ( A C_ No /\ A e. _V /\ Z e. No ) -> ( A. a e. A a  -. ( Z |` dom S ) 

Proof

Step Hyp Ref Expression
1 nosupbnd2.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 nfv
 |-  F/ x ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a 
3 nfcv
 |-  F/_ x Z
4 nfre1
 |-  F/ x E. x e. A A. y e. A -. x 
5 nfriota1
 |-  F/_ x ( iota_ x e. A A. y e. A -. x 
6 5 nfdm
 |-  F/_ x dom ( iota_ x e. A A. y e. A -. x 
7 nfcv
 |-  F/_ x 2o
8 6 7 nfop
 |-  F/_ x <. dom ( iota_ x e. A A. y e. A -. x .
9 8 nfsn
 |-  F/_ x { <. dom ( iota_ x e. A A. y e. A -. x . }
10 5 9 nfun
 |-  F/_ x ( ( iota_ x e. A A. y e. A -. x . } )
11 nfcv
 |-  F/_ x { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) }
12 nfiota1
 |-  F/_ x ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) )
13 11 12 nfmpt
 |-  F/_ 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 ) ) )
14 4 10 13 nfif
 |-  F/_ x 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 ) ) ) )
15 1 14 nfcxfr
 |-  F/_ x S
16 15 nfdm
 |-  F/_ x dom S
17 3 16 nfres
 |-  F/_ x ( Z |` dom S )
18 nfcv
 |-  F/_ x 
19 17 18 15 nfbr
 |-  F/ x ( Z |` dom S ) 
20 19 nfn
 |-  F/ x -. ( Z |` dom S ) 
21 2 20 nfim
 |-  F/ x ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a  -. ( Z |` dom S ) 
22 simpl
 |-  ( ( ( x e. A /\ A. y e. A -. x  ( x e. A /\ A. y e. A -. x 
23 rspe
 |-  ( ( x e. A /\ A. y e. A -. x  E. x e. A A. y e. A -. x 
24 23 adantr
 |-  ( ( ( x e. A /\ A. y e. A -. x  E. x e. A A. y e. A -. x 
25 nomaxmo
 |-  ( A C_ No -> E* x e. A A. y e. A -. x 
26 25 3ad2ant1
 |-  ( ( A C_ No /\ A e. _V /\ Z e. No ) -> E* x e. A A. y e. A -. x 
27 26 ad2antrl
 |-  ( ( ( x e. A /\ A. y e. A -. x  E* x e. A A. y e. A -. x 
28 reu5
 |-  ( E! x e. A A. y e. A -. x  ( E. x e. A A. y e. A -. x 
29 24 27 28 sylanbrc
 |-  ( ( ( x e. A /\ A. y e. A -. x  E! x e. A A. y e. A -. x 
30 riota1
 |-  ( E! x e. A A. y e. A -. x  ( ( x e. A /\ A. y e. A -. x  ( iota_ x e. A A. y e. A -. x 
31 29 30 syl
 |-  ( ( ( x e. A /\ A. y e. A -. x  ( ( x e. A /\ A. y e. A -. x  ( iota_ x e. A A. y e. A -. x 
32 22 31 mpbid
 |-  ( ( ( x e. A /\ A. y e. A -. x  ( iota_ x e. A A. y e. A -. x 
33 nosupbnd2lem1
 |-  ( ( ( x e. A /\ A. y e. A -. x  -. ( Z |` suc dom x ) . } ) )
34 33 3expb
 |-  ( ( ( x e. A /\ A. y e. A -. x  -. ( Z |` suc dom x ) . } ) )
35 dmeq
 |-  ( ( iota_ x e. A A. y e. A -. x  dom ( iota_ x e. A A. y e. A -. x 
36 suceq
 |-  ( dom ( iota_ x e. A A. y e. A -. x  suc dom ( iota_ x e. A A. y e. A -. x 
37 35 36 syl
 |-  ( ( iota_ x e. A A. y e. A -. x  suc dom ( iota_ x e. A A. y e. A -. x 
38 37 reseq2d
 |-  ( ( iota_ x e. A A. y e. A -. x  ( Z |` suc dom ( iota_ x e. A A. y e. A -. x 
39 id
 |-  ( ( iota_ x e. A A. y e. A -. x  ( iota_ x e. A A. y e. A -. x 
40 35 opeq1d
 |-  ( ( iota_ x e. A A. y e. A -. x  <. dom ( iota_ x e. A A. y e. A -. x . = <. dom x , 2o >. )
41 40 sneqd
 |-  ( ( iota_ x e. A A. y e. A -. x  { <. dom ( iota_ x e. A A. y e. A -. x . } = { <. dom x , 2o >. } )
42 39 41 uneq12d
 |-  ( ( iota_ x e. A A. y e. A -. x  ( ( iota_ x e. A A. y e. A -. x . } ) = ( x u. { <. dom x , 2o >. } ) )
43 38 42 breq12d
 |-  ( ( iota_ x e. A A. y e. A -. x  ( ( Z |` suc dom ( iota_ x e. A A. y e. A -. x . } ) <-> ( Z |` suc dom x ) . } ) ) )
44 43 notbid
 |-  ( ( iota_ x e. A A. y e. A -. x  ( -. ( Z |` suc dom ( iota_ x e. A A. y e. A -. x . } ) <-> -. ( Z |` suc dom x ) . } ) ) )
45 34 44 syl5ibrcom
 |-  ( ( ( x e. A /\ A. y e. A -. x  ( ( iota_ x e. A A. y e. A -. x  -. ( Z |` suc dom ( iota_ x e. A A. y e. A -. x . } ) ) )
46 32 45 mpd
 |-  ( ( ( x e. A /\ A. y e. A -. x  -. ( Z |` suc dom ( iota_ x e. A A. y e. A -. x . } ) )
47 iftrue
 |-  ( E. x e. A A. y e. A -. x  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 ) ) ) ) = ( ( iota_ x e. A A. y e. A -. x . } ) )
48 1 47 syl5eq
 |-  ( E. x e. A A. y e. A -. x  S = ( ( iota_ x e. A A. y e. A -. x . } ) )
49 23 48 syl
 |-  ( ( x e. A /\ A. y e. A -. x  S = ( ( iota_ x e. A A. y e. A -. x . } ) )
50 49 dmeqd
 |-  ( ( x e. A /\ A. y e. A -. x  dom S = dom ( ( iota_ x e. A A. y e. A -. x . } ) )
51 2on
 |-  2o e. On
52 51 elexi
 |-  2o e. _V
53 52 dmsnop
 |-  dom { <. dom ( iota_ x e. A A. y e. A -. x . } = { dom ( iota_ x e. A A. y e. A -. x 
54 53 uneq2i
 |-  ( dom ( iota_ x e. A A. y e. A -. x . } ) = ( dom ( iota_ x e. A A. y e. A -. x 
55 dmun
 |-  dom ( ( iota_ x e. A A. y e. A -. x . } ) = ( dom ( iota_ x e. A A. y e. A -. x . } )
56 df-suc
 |-  suc dom ( iota_ x e. A A. y e. A -. x 
57 54 55 56 3eqtr4i
 |-  dom ( ( iota_ x e. A A. y e. A -. x . } ) = suc dom ( iota_ x e. A A. y e. A -. x 
58 50 57 eqtrdi
 |-  ( ( x e. A /\ A. y e. A -. x  dom S = suc dom ( iota_ x e. A A. y e. A -. x 
59 58 reseq2d
 |-  ( ( x e. A /\ A. y e. A -. x  ( Z |` dom S ) = ( Z |` suc dom ( iota_ x e. A A. y e. A -. x 
60 59 adantr
 |-  ( ( ( x e. A /\ A. y e. A -. x  ( Z |` dom S ) = ( Z |` suc dom ( iota_ x e. A A. y e. A -. x 
61 49 adantr
 |-  ( ( ( x e. A /\ A. y e. A -. x  S = ( ( iota_ x e. A A. y e. A -. x . } ) )
62 60 61 breq12d
 |-  ( ( ( x e. A /\ A. y e. A -. x  ( ( Z |` dom S )  ( Z |` suc dom ( iota_ x e. A A. y e. A -. x . } ) ) )
63 46 62 mtbird
 |-  ( ( ( x e. A /\ A. y e. A -. x  -. ( Z |` dom S ) 
64 63 exp31
 |-  ( x e. A -> ( A. y e. A -. x  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a  -. ( Z |` dom S ) 
65 21 64 rexlimi
 |-  ( E. x e. A A. y e. A -. x  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a  -. ( Z |` dom S ) 
66 65 imp
 |-  ( ( E. x e. A A. y e. A -. x  -. ( Z |` dom S ) 
67 1 nosupno
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
68 67 3adant3
 |-  ( ( A C_ No /\ A e. _V /\ Z e. No ) -> S e. No )
69 68 ad2antrl
 |-  ( ( -. E. x e. A A. y e. A -. x  S e. No )
70 nodmon
 |-  ( S e. No -> dom S e. On )
71 69 70 syl
 |-  ( ( -. E. x e. A A. y e. A -. x  dom S e. On )
72 noreson
 |-  ( ( S e. No /\ dom S e. On ) -> ( S |` dom S ) e. No )
73 69 71 72 syl2anc
 |-  ( ( -. E. x e. A A. y e. A -. x  ( S |` dom S ) e. No )
74 simprl3
 |-  ( ( -. E. x e. A A. y e. A -. x  Z e. No )
75 noreson
 |-  ( ( Z e. No /\ dom S e. On ) -> ( Z |` dom S ) e. No )
76 74 71 75 syl2anc
 |-  ( ( -. E. x e. A A. y e. A -. x  ( Z |` dom S ) e. No )
77 dmres
 |-  dom ( S |` dom S ) = ( dom S i^i dom S )
78 inss2
 |-  ( dom S i^i dom S ) C_ dom S
79 77 78 eqsstri
 |-  dom ( S |` dom S ) C_ dom S
80 79 a1i
 |-  ( ( -. E. x e. A A. y e. A -. x  dom ( S |` dom S ) C_ dom S )
81 dmres
 |-  dom ( Z |` dom S ) = ( dom S i^i dom Z )
82 inss1
 |-  ( dom S i^i dom Z ) C_ dom S
83 81 82 eqsstri
 |-  dom ( Z |` dom S ) C_ dom S
84 83 a1i
 |-  ( ( -. E. x e. A A. y e. A -. x  dom ( Z |` dom S ) C_ dom S )
85 1 nosupdm
 |-  ( -. E. x e. A A. y e. A -. x  dom S = { g | E. p e. A ( g e. dom p /\ A. q e. A ( -. q  ( p |` suc g ) = ( q |` suc g ) ) ) } )
86 85 abeq2d
 |-  ( -. E. x e. A A. y e. A -. x  ( g e. dom S <-> E. p e. A ( g e. dom p /\ A. q e. A ( -. q  ( p |` suc g ) = ( q |` suc g ) ) ) ) )
87 86 adantr
 |-  ( ( -. E. x e. A A. y e. A -. x  ( g e. dom S <-> E. p e. A ( g e. dom p /\ A. q e. A ( -. q  ( p |` suc g ) = ( q |` suc g ) ) ) ) )
88 simprl
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p e. A )
89 simplrr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A. a e. A a 
90 breq1
 |-  ( a = p -> ( a  p 
91 90 rspcv
 |-  ( p e. A -> ( A. a e. A a  p 
92 88 89 91 sylc
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p 
93 simprl1
 |-  ( ( -. E. x e. A A. y e. A -. x  A C_ No )
94 93 adantr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A C_ No )
95 94 88 sseldd
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p e. No )
96 74 adantr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> Z e. No )
97 sltso
 |-  
98 soasym
 |-  ( (  ( p  -. Z 
99 97 98 mpan
 |-  ( ( p e. No /\ Z e. No ) -> ( p  -. Z 
100 95 96 99 syl2anc
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( p  -. Z 
101 92 100 mpd
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. Z 
102 nodmon
 |-  ( p e. No -> dom p e. On )
103 95 102 syl
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> dom p e. On )
104 simprrl
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> g e. dom p )
105 onelon
 |-  ( ( dom p e. On /\ g e. dom p ) -> g e. On )
106 103 104 105 syl2anc
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> g e. On )
107 sucelon
 |-  ( g e. On <-> suc g e. On )
108 106 107 sylib
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> suc g e. On )
109 sltres
 |-  ( ( Z e. No /\ p e. No /\ suc g e. On ) -> ( ( Z |` suc g )  Z 
110 96 95 108 109 syl3anc
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( ( Z |` suc g )  Z 
111 101 110 mtod
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. ( Z |` suc g ) 
112 simpll
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. E. x e. A A. y e. A -. x 
113 simprl2
 |-  ( ( -. E. x e. A A. y e. A -. x  A e. _V )
114 93 113 jca
 |-  ( ( -. E. x e. A A. y e. A -. x  ( A C_ No /\ A e. _V ) )
115 114 adantr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( A C_ No /\ A e. _V ) )
116 simprrr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A. q e. A ( -. q  ( p |` suc g ) = ( q |` suc g ) ) )
117 breq1
 |-  ( v = q -> ( v  q 
118 117 notbid
 |-  ( v = q -> ( -. v  -. q 
119 reseq1
 |-  ( v = q -> ( v |` suc g ) = ( q |` suc g ) )
120 119 eqeq2d
 |-  ( v = q -> ( ( p |` suc g ) = ( v |` suc g ) <-> ( p |` suc g ) = ( q |` suc g ) ) )
121 118 120 imbi12d
 |-  ( v = q -> ( ( -. v  ( p |` suc g ) = ( v |` suc g ) ) <-> ( -. q  ( p |` suc g ) = ( q |` suc g ) ) ) )
122 121 cbvralvw
 |-  ( A. v e. A ( -. v  ( p |` suc g ) = ( v |` suc g ) ) <-> A. q e. A ( -. q  ( p |` suc g ) = ( q |` suc g ) ) )
123 116 122 sylibr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A. v e. A ( -. v  ( p |` suc g ) = ( v |` suc g ) ) )
124 1 nosupres
 |-  ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( v |` suc g ) ) ) ) -> ( S |` suc g ) = ( p |` suc g ) )
125 112 115 88 104 123 124 syl113anc
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( S |` suc g ) = ( p |` suc g ) )
126 125 breq2d
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( ( Z |` suc g )  ( Z |` suc g ) 
127 111 126 mtbird
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. ( Z |` suc g ) 
128 127 rexlimdvaa
 |-  ( ( -. E. x e. A A. y e. A -. x  ( E. p e. A ( g e. dom p /\ A. q e. A ( -. q  ( p |` suc g ) = ( q |` suc g ) ) ) -> -. ( Z |` suc g ) 
129 87 128 sylbid
 |-  ( ( -. E. x e. A A. y e. A -. x  ( g e. dom S -> -. ( Z |` suc g ) 
130 129 imp
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( Z |` suc g ) 
131 69 adantr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  S e. No )
132 nodmord
 |-  ( S e. No -> Ord dom S )
133 131 132 syl
 |-  ( ( ( -. E. x e. A A. y e. A -. x  Ord dom S )
134 simpr
 |-  ( ( ( -. E. x e. A A. y e. A -. x  g e. dom S )
135 ordsucss
 |-  ( Ord dom S -> ( g e. dom S -> suc g C_ dom S ) )
136 133 134 135 sylc
 |-  ( ( ( -. E. x e. A A. y e. A -. x  suc g C_ dom S )
137 136 resabs1d
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( Z |` dom S ) |` suc g ) = ( Z |` suc g ) )
138 136 resabs1d
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( S |` dom S ) |` suc g ) = ( S |` suc g ) )
139 137 138 breq12d
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( ( Z |` dom S ) |` suc g )  ( Z |` suc g ) 
140 130 139 mtbird
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( ( Z |` dom S ) |` suc g ) 
141 140 ralrimiva
 |-  ( ( -. E. x e. A A. y e. A -. x  A. g e. dom S -. ( ( Z |` dom S ) |` suc g ) 
142 noresle
 |-  ( ( ( ( S |` dom S ) e. No /\ ( Z |` dom S ) e. No ) /\ ( dom ( S |` dom S ) C_ dom S /\ dom ( Z |` dom S ) C_ dom S /\ A. g e. dom S -. ( ( Z |` dom S ) |` suc g )  -. ( Z |` dom S ) 
143 73 76 80 84 141 142 syl23anc
 |-  ( ( -. E. x e. A A. y e. A -. x  -. ( Z |` dom S ) 
144 nofun
 |-  ( S e. No -> Fun S )
145 69 144 syl
 |-  ( ( -. E. x e. A A. y e. A -. x  Fun S )
146 funrel
 |-  ( Fun S -> Rel S )
147 resdm
 |-  ( Rel S -> ( S |` dom S ) = S )
148 145 146 147 3syl
 |-  ( ( -. E. x e. A A. y e. A -. x  ( S |` dom S ) = S )
149 148 breq2d
 |-  ( ( -. E. x e. A A. y e. A -. x  ( ( Z |` dom S )  ( Z |` dom S ) 
150 143 149 mtbid
 |-  ( ( -. E. x e. A A. y e. A -. x  -. ( Z |` dom S ) 
151 66 150 pm2.61ian
 |-  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a  -. ( Z |` dom S ) 
152 simpll1
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A C_ No )
153 simpll2
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A e. _V )
154 simpr
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  a e. A )
155 1 nosupbnd1
 |-  ( ( A C_ No /\ A e. _V /\ a e. A ) -> ( a |` dom S ) 
156 152 153 154 155 syl3anc
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( a |` dom S ) 
157 simplr
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  -. ( Z |` dom S ) 
158 simpl1
 |-  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A C_ No )
159 158 sselda
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  a e. No )
160 152 153 67 syl2anc
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  S e. No )
161 160 70 syl
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  dom S e. On )
162 noreson
 |-  ( ( a e. No /\ dom S e. On ) -> ( a |` dom S ) e. No )
163 159 161 162 syl2anc
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( a |` dom S ) e. No )
164 simpll3
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  Z e. No )
165 164 161 75 syl2anc
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( Z |` dom S ) e. No )
166 sotr3
 |-  ( (  ( ( ( a |` dom S )  ( a |` dom S ) 
167 97 166 mpan
 |-  ( ( ( a |` dom S ) e. No /\ S e. No /\ ( Z |` dom S ) e. No ) -> ( ( ( a |` dom S )  ( a |` dom S ) 
168 163 160 165 167 syl3anc
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( ( ( a |` dom S )  ( a |` dom S ) 
169 156 157 168 mp2and
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( a |` dom S ) 
170 sltres
 |-  ( ( a e. No /\ Z e. No /\ dom S e. On ) -> ( ( a |` dom S )  a 
171 159 164 161 170 syl3anc
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( ( a |` dom S )  a 
172 169 171 mpd
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  a 
173 172 ralrimiva
 |-  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A. a e. A a 
174 151 173 impbida
 |-  ( ( A C_ No /\ A e. _V /\ Z e. No ) -> ( A. a e. A a  -. ( Z |` dom S )