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 35 suceqd 
 |-  ( ( iota_ x e. A A. y e. A -. x  suc dom ( iota_ x e. A A. y e. A -. x
37 36 reseq2d 
 |-  ( ( iota_ x e. A A. y e. A -. x  ( Z |` suc dom ( iota_ x e. A A. y e. A -. x
38 id 
 |-  ( ( iota_ x e. A A. y e. A -. x  ( iota_ x e. A A. y e. A -. x
39 35 opeq1d 
 |-  ( ( iota_ x e. A A. y e. A -. x  <. dom ( iota_ x e. A A. y e. A -. x . = <. dom x , 2o >. )
40 39 sneqd 
 |-  ( ( iota_ x e. A A. y e. A -. x  { <. dom ( iota_ x e. A A. y e. A -. x . } = { <. dom x , 2o >. } )
41 38 40 uneq12d 
 |-  ( ( iota_ x e. A A. y e. A -. x  ( ( iota_ x e. A A. y e. A -. x . } ) = ( x u. { <. dom x , 2o >. } ) )
42 37 41 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 ) . } ) ) )
43 42 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 ) . } ) ) )
44 34 43 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 . } ) ) )
45 32 44 mpd 
 |-  ( ( ( x e. A /\ A. y e. A -. x  -. ( Z |` suc dom ( iota_ x e. A A. y e. A -. x . } ) )
46 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 . } ) )
47 1 46 eqtrid 
 |-  ( E. x e. A A. y e. A -. x  S = ( ( iota_ x e. A A. y e. A -. x . } ) )
48 23 47 syl 
 |-  ( ( x e. A /\ A. y e. A -. x  S = ( ( iota_ x e. A A. y e. A -. x . } ) )
49 48 dmeqd 
 |-  ( ( x e. A /\ A. y e. A -. x  dom S = dom ( ( iota_ x e. A A. y e. A -. x . } ) )
50 2on 
 |-  2o e. On
51 50 elexi 
 |-  2o e. _V
52 51 dmsnop 
 |-  dom { <. dom ( iota_ x e. A A. y e. A -. x . } = { dom ( iota_ x e. A A. y e. A -. x
53 52 uneq2i 
 |-  ( dom ( iota_ x e. A A. y e. A -. x . } ) = ( dom ( iota_ x e. A A. y e. A -. x
54 dmun 
 |-  dom ( ( iota_ x e. A A. y e. A -. x . } ) = ( dom ( iota_ x e. A A. y e. A -. x . } )
55 df-suc 
 |-  suc dom ( iota_ x e. A A. y e. A -. x
56 53 54 55 3eqtr4i 
 |-  dom ( ( iota_ x e. A A. y e. A -. x . } ) = suc dom ( iota_ x e. A A. y e. A -. x
57 49 56 eqtrdi 
 |-  ( ( x e. A /\ A. y e. A -. x  dom S = suc dom ( iota_ x e. A A. y e. A -. x
58 57 reseq2d 
 |-  ( ( x e. A /\ A. y e. A -. x  ( Z |` dom S ) = ( Z |` suc dom ( iota_ x e. A A. y e. A -. x
59 58 adantr 
 |-  ( ( ( x e. A /\ A. y e. A -. x  ( Z |` dom S ) = ( Z |` suc dom ( iota_ x e. A A. y e. A -. x
60 48 adantr 
 |-  ( ( ( x e. A /\ A. y e. A -. x  S = ( ( iota_ x e. A A. y e. A -. x . } ) )
61 59 60 breq12d 
 |-  ( ( ( x e. A /\ A. y e. A -. x  ( ( Z |` dom S )  ( Z |` suc dom ( iota_ x e. A A. y e. A -. x . } ) ) )
62 45 61 mtbird 
 |-  ( ( ( x e. A /\ A. y e. A -. x  -. ( Z |` dom S )
63 62 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 )
64 21 63 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 )
65 64 imp 
 |-  ( ( E. x e. A A. y e. A -. x  -. ( Z |` dom S )
66 1 nosupno 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
67 66 3adant3 
 |-  ( ( A C_ No /\ A e. _V /\ Z e. No ) -> S e. No )
68 67 ad2antrl 
 |-  ( ( -. E. x e. A A. y e. A -. x  S e. No )
69 nodmon 
 |-  ( S e. No -> dom S e. On )
70 68 69 syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  dom S e. On )
71 noreson 
 |-  ( ( S e. No /\ dom S e. On ) -> ( S |` dom S ) e. No )
72 68 70 71 syl2anc 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( S |` dom S ) e. No )
73 simprl3 
 |-  ( ( -. E. x e. A A. y e. A -. x  Z e. No )
74 noreson 
 |-  ( ( Z e. No /\ dom S e. On ) -> ( Z |` dom S ) e. No )
75 73 70 74 syl2anc 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( Z |` dom S ) e. No )
76 dmres 
 |-  dom ( S |` dom S ) = ( dom S i^i dom S )
77 inss2 
 |-  ( dom S i^i dom S ) C_ dom S
78 76 77 eqsstri 
 |-  dom ( S |` dom S ) C_ dom S
79 78 a1i 
 |-  ( ( -. E. x e. A A. y e. A -. x  dom ( S |` dom S ) C_ dom S )
80 dmres 
 |-  dom ( Z |` dom S ) = ( dom S i^i dom Z )
81 inss1 
 |-  ( dom S i^i dom Z ) C_ dom S
82 80 81 eqsstri 
 |-  dom ( Z |` dom S ) C_ dom S
83 82 a1i 
 |-  ( ( -. E. x e. A A. y e. A -. x  dom ( Z |` dom S ) C_ dom S )
84 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 ) ) ) } )
85 84 eqabrd 
 |-  ( -. 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 ) ) ) ) )
86 85 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 ) ) ) ) )
87 simprl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p e. A )
88 simplrr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A. a e. A a
89 breq1 
 |-  ( a = p -> ( a  p
90 89 rspcv 
 |-  ( p e. A -> ( A. a e. A a  p
91 87 88 90 sylc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p
92 simprl1 
 |-  ( ( -. E. x e. A A. y e. A -. x  A C_ No )
93 92 adantr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A C_ No )
94 93 87 sseldd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p e. No )
95 73 adantr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> Z e. No )
96 sltso 
 |-
97 soasym 
 |-  ( (  ( p  -. Z
98 96 97 mpan 
 |-  ( ( p e. No /\ Z e. No ) -> ( p  -. Z
99 94 95 98 syl2anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( p  -. Z
100 91 99 mpd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. Z
101 nodmon 
 |-  ( p e. No -> dom p e. On )
102 94 101 syl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> dom p e. On )
103 simprrl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> g e. dom p )
104 onelon 
 |-  ( ( dom p e. On /\ g e. dom p ) -> g e. On )
105 102 103 104 syl2anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> g e. On )
106 onsucb 
 |-  ( g e. On <-> suc g e. On )
107 105 106 sylib 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> suc g e. On )
108 sltres 
 |-  ( ( Z e. No /\ p e. No /\ suc g e. On ) -> ( ( Z |` suc g )  Z
109 95 94 107 108 syl3anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( ( Z |` suc g )  Z
110 100 109 mtod 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. ( Z |` suc g )
111 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
112 simprl2 
 |-  ( ( -. E. x e. A A. y e. A -. x  A e. _V )
113 92 112 jca 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( A C_ No /\ A e. _V ) )
114 113 adantr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( A C_ No /\ A e. _V ) )
115 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 ) ) )
116 breq1 
 |-  ( v = q -> ( v  q
117 116 notbid 
 |-  ( v = q -> ( -. v  -. q
118 reseq1 
 |-  ( v = q -> ( v |` suc g ) = ( q |` suc g ) )
119 118 eqeq2d 
 |-  ( v = q -> ( ( p |` suc g ) = ( v |` suc g ) <-> ( p |` suc g ) = ( q |` suc g ) ) )
120 117 119 imbi12d 
 |-  ( v = q -> ( ( -. v  ( p |` suc g ) = ( v |` suc g ) ) <-> ( -. q  ( p |` suc g ) = ( q |` suc g ) ) ) )
121 120 cbvralvw 
 |-  ( A. v e. A ( -. v  ( p |` suc g ) = ( v |` suc g ) ) <-> A. q e. A ( -. q  ( p |` suc g ) = ( q |` suc g ) ) )
122 115 121 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 ) ) )
123 1 nosupres 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( v |` suc g ) ) ) ) -> ( S |` suc g ) = ( p |` suc g ) )
124 111 114 87 103 122 123 syl113anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( S |` suc g ) = ( p |` suc g ) )
125 124 breq2d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( ( Z |` suc g )  ( Z |` suc g )
126 110 125 mtbird 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. ( Z |` suc g )
127 126 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 )
128 86 127 sylbid 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( g e. dom S -> -. ( Z |` suc g )
129 128 imp 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( Z |` suc g )
130 68 adantr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  S e. No )
131 nodmord 
 |-  ( S e. No -> Ord dom S )
132 130 131 syl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  Ord dom S )
133 simpr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  g e. dom S )
134 ordsucss 
 |-  ( Ord dom S -> ( g e. dom S -> suc g C_ dom S ) )
135 132 133 134 sylc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  suc g C_ dom S )
136 135 resabs1d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( Z |` dom S ) |` suc g ) = ( Z |` suc g ) )
137 135 resabs1d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( S |` dom S ) |` suc g ) = ( S |` suc g ) )
138 136 137 breq12d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( ( Z |` dom S ) |` suc g )  ( Z |` suc g )
139 129 138 mtbird 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( ( Z |` dom S ) |` suc g )
140 139 ralrimiva 
 |-  ( ( -. E. x e. A A. y e. A -. x  A. g e. dom S -. ( ( Z |` dom S ) |` suc g )
141 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 )
142 72 75 79 83 140 141 syl23anc 
 |-  ( ( -. E. x e. A A. y e. A -. x  -. ( Z |` dom S )
143 nofun 
 |-  ( S e. No -> Fun S )
144 funrel 
 |-  ( Fun S -> Rel S )
145 resdm 
 |-  ( Rel S -> ( S |` dom S ) = S )
146 68 143 144 145 4syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( S |` dom S ) = S )
147 146 breq2d 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( ( Z |` dom S )  ( Z |` dom S )
148 142 147 mtbid 
 |-  ( ( -. E. x e. A A. y e. A -. x  -. ( Z |` dom S )
149 65 148 pm2.61ian 
 |-  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a  -. ( Z |` dom S )
150 simpll1 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A C_ No )
151 simpll2 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A e. _V )
152 simpr 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  a e. A )
153 1 nosupbnd1 
 |-  ( ( A C_ No /\ A e. _V /\ a e. A ) -> ( a |` dom S )
154 150 151 152 153 syl3anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( a |` dom S )
155 simplr 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  -. ( Z |` dom S )
156 simpl1 
 |-  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A C_ No )
157 156 sselda 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  a e. No )
158 150 151 66 syl2anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  S e. No )
159 158 69 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  dom S e. On )
160 noreson 
 |-  ( ( a e. No /\ dom S e. On ) -> ( a |` dom S ) e. No )
161 157 159 160 syl2anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( a |` dom S ) e. No )
162 simpll3 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  Z e. No )
163 162 159 74 syl2anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( Z |` dom S ) e. No )
164 sotr3 
 |-  ( (  ( ( ( a |` dom S )  ( a |` dom S )
165 96 164 mpan 
 |-  ( ( ( a |` dom S ) e. No /\ S e. No /\ ( Z |` dom S ) e. No ) -> ( ( ( a |` dom S )  ( a |` dom S )
166 161 158 163 165 syl3anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( ( ( a |` dom S )  ( a |` dom S )
167 154 155 166 mp2and 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( a |` dom S )
168 sltres 
 |-  ( ( a e. No /\ Z e. No /\ dom S e. On ) -> ( ( a |` dom S )  a
169 157 162 159 168 syl3anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( ( a |` dom S )  a
170 167 169 mpd 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  a
171 170 ralrimiva 
 |-  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A. a e. A a
172 149 171 impbida 
 |-  ( ( A C_ No /\ A e. _V /\ Z e. No ) -> ( A. a e. A a  -. ( Z |` dom S )