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 eqtrid 
 |-  ( 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 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 ) ) ) ) )
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 onsucb 
 |-  ( 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 funrel 
 |-  ( Fun S -> Rel S )
146 resdm 
 |-  ( Rel S -> ( S |` dom S ) = S )
147 69 144 145 146 4syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( S |` dom S ) = S )
148 147 breq2d 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( ( Z |` dom S )  ( Z |` dom S )
149 143 148 mtbid 
 |-  ( ( -. E. x e. A A. y e. A -. x  -. ( Z |` dom S )
150 66 149 pm2.61ian 
 |-  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a  -. ( Z |` dom S )
151 simpll1 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A C_ No )
152 simpll2 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A e. _V )
153 simpr 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  a e. A )
154 1 nosupbnd1 
 |-  ( ( A C_ No /\ A e. _V /\ a e. A ) -> ( a |` dom S )
155 151 152 153 154 syl3anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( a |` dom S )
156 simplr 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  -. ( Z |` dom S )
157 simpl1 
 |-  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A C_ No )
158 157 sselda 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  a e. No )
159 151 152 67 syl2anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  S e. No )
160 159 70 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  dom S e. On )
161 noreson 
 |-  ( ( a e. No /\ dom S e. On ) -> ( a |` dom S ) e. No )
162 158 160 161 syl2anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( a |` dom S ) e. No )
163 simpll3 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  Z e. No )
164 163 160 75 syl2anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( Z |` dom S ) e. No )
165 sotr3 
 |-  ( (  ( ( ( a |` dom S )  ( a |` dom S )
166 97 165 mpan 
 |-  ( ( ( a |` dom S ) e. No /\ S e. No /\ ( Z |` dom S ) e. No ) -> ( ( ( a |` dom S )  ( a |` dom S )
167 162 159 164 166 syl3anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( ( ( a |` dom S )  ( a |` dom S )
168 155 156 167 mp2and 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( a |` dom S )
169 sltres 
 |-  ( ( a e. No /\ Z e. No /\ dom S e. On ) -> ( ( a |` dom S )  a
170 158 163 160 169 syl3anc 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  ( ( a |` dom S )  a
171 168 170 mpd 
 |-  ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  a
172 171 ralrimiva 
 |-  ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S )  A. a e. A a
173 150 172 impbida 
 |-  ( ( A C_ No /\ A e. _V /\ Z e. No ) -> ( A. a e. A a  -. ( Z |` dom S )