Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nosupbnd2 Structured version   Visualization version   Unicode version
Theorem nosupbnd2 31862
Description: Bounding law from above for the surreal supremum. Proposition 4.3 of [Lipparini] p. 6. (Contributed by Scott Fenton, 6-Dec-2021.)
Hypothesis
Ref Expression
nosupbnd2.1 |- S = if ( E. x e. A A. y e. A -. x <s y , ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
Assertion
Ref Expression
nosupbnd2 |- ( ( A C_ No /\ A e. _V /\ Z e. No ) -> ( A. a e. A a <s Z <-> -. ( Z |` dom S ) <s S ) )
Distinct variable groups:   A, a, g, u, v, x, y   S, a, g   v, u, x, y   Z, a, g, x
Allowed substitution hints:   S( x, y, v, u)   Z( y, v, u)
Proof of Theorem nosupbnd2
Dummy variables p q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1843 . . . . . 6 |- F/ x ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z )
2 nfcv 2764 . . . . . . . . 9 |- F/_ x Z
3 nosupbnd2.1 . . . . . . . . . . 11 |- S = if ( E. x e. A A. y e. A -. x <s y , ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
4 nfre1 3005 . . . . . . . . . . . 12 |- F/ x E. x e. A A. y e. A -. x <s y
5 nfriota1 6618 . . . . . . . . . . . . 13 |- F/_ x ( iota_ x e. A A. y e. A -. x <s y )
65nfdm 5367 . . . . . . . . . . . . . . 15 |- F/_ x dom ( iota_ x e. A A. y e. A -. x <s y )
7 nfcv 2764 . . . . . . . . . . . . . . 15 |- F/_ x 2o
86, 7nfop 4418 . . . . . . . . . . . . . 14 |- F/_ x <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >.
98nfsn 4242 . . . . . . . . . . . . 13 |- F/_ x { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. }
105, 9nfun 3769 . . . . . . . . . . . 12 |- F/_ x ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } )
11 nfcv 2764 . . . . . . . . . . . . 13 |- F/_ x { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc y ) = ( v |` suc y ) ) ) }
12 nfiota1 5853 . . . . . . . . . . . . 13 |- F/_ x ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) )
1311, 12nfmpt 4746 . . . . . . . . . . . 12 |- F/_ x ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) )
144, 10, 13nfif 4115 . . . . . . . . . . 11 |- F/_ x if ( E. x e. A A. y e. A -. x <s y , ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
153, 14nfcxfr 2762 . . . . . . . . . 10 |- F/_ x S
1615nfdm 5367 . . . . . . . . 9 |- F/_ x dom S
172, 16nfres 5398 . . . . . . . 8 |- F/_ x ( Z |` dom S )
18 nfcv 2764 . . . . . . . 8 |- F/_ x <s
1917, 18, 15nfbr 4699 . . . . . . 7 |- F/ x ( Z |` dom S ) <s S
2019nfn 1784 . . . . . 6 |- F/ x -. ( Z |` dom S ) <s S
211, 20nfim 1825 . . . . 5 |- F/ x ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> -. ( Z |` dom S ) <s S )
22 simpl 473 . . . . . . . . 9 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( x e. A /\ A. y e. A -. x <s y ) )
23 rspe 3003 . . . . . . . . . . . 12 |- ( ( x e. A /\ A. y e. A -. x <s y ) -> E. x e. A A. y e. A -. x <s y )
2423adantr 481 . . . . . . . . . . 11 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> E. x e. A A. y e. A -. x <s y )
25 nomaxmo 31847 . . . . . . . . . . . . 13 |- ( A C_ No -> E* x e. A A. y e. A -. x <s y )
26253ad2ant1 1082 . . . . . . . . . . . 12 |- ( ( A C_ No /\ A e. _V /\ Z e. No ) -> E* x e. A A. y e. A -. x <s y )
2726ad2antrl 764 . . . . . . . . . . 11 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> E* x e. A A. y e. A -. x <s y )
28 reu5 3159 . . . . . . . . . . 11 |- ( E! x e. A A. y e. A -. x <s y <-> ( E. x e. A A. y e. A -. x <s y /\ E* x e. A A. y e. A -. x <s y ) )
2924, 27, 28sylanbrc 698 . . . . . . . . . 10 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> E! x e. A A. y e. A -. x <s y )
30 riota1 6629 . . . . . . . . . 10 |- ( E! x e. A A. y e. A -. x <s y -> ( ( x e. A /\ A. y e. A -. x <s y ) <-> ( iota_ x e. A A. y e. A -. x <s y ) = x ) )
3129, 30syl 17 . . . . . . . . 9 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( ( x e. A /\ A. y e. A -. x <s y ) <-> ( iota_ x e. A A. y e. A -. x <s y ) = x ) )
3222, 31mpbid 222 . . . . . . . 8 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( iota_ x e. A A. y e. A -. x <s y ) = x )
33 nosupbnd2lem1 31861 . . . . . . . . . 10 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> -. ( Z |` suc dom x ) <s ( x u. { <. dom x , 2o >. } ) )
34333expb 1266 . . . . . . . . 9 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> -. ( Z |` suc dom x ) <s ( x u. { <. dom x , 2o >. } ) )
35 dmeq 5324 . . . . . . . . . . . . 13 |- ( ( iota_ x e. A A. y e. A -. x <s y ) = x -> dom ( iota_ x e. A A. y e. A -. x <s y ) = dom x )
36 suceq 5790 . . . . . . . . . . . . 13 |- ( dom ( iota_ x e. A A. y e. A -. x <s y ) = dom x -> suc dom ( iota_ x e. A A. y e. A -. x <s y ) = suc dom x )
3735, 36syl 17 . . . . . . . . . . . 12 |- ( ( iota_ x e. A A. y e. A -. x <s y ) = x -> suc dom ( iota_ x e. A A. y e. A -. x <s y ) = suc dom x )
3837reseq2d 5396 . . . . . . . . . . 11 |- ( ( iota_ x e. A A. y e. A -. x <s y ) = x -> ( Z |` suc dom ( iota_ x e. A A. y e. A -. x <s y ) ) = ( Z |` suc dom x ) )
39 id 22 . . . . . . . . . . . 12 |- ( ( iota_ x e. A A. y e. A -. x <s y ) = x -> ( iota_ x e. A A. y e. A -. x <s y ) = x )
4035opeq1d 4408 . . . . . . . . . . . . 13 |- ( ( iota_ x e. A A. y e. A -. x <s y ) = x -> <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. = <. dom x , 2o >. )
4140sneqd 4189 . . . . . . . . . . . 12 |- ( ( iota_ x e. A A. y e. A -. x <s y ) = x -> { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } = { <. dom x , 2o >. } )
4239, 41uneq12d 3768 . . . . . . . . . . 11 |- ( ( iota_ x e. A A. y e. A -. x <s y ) = x -> ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) = ( x u. { <. dom x , 2o >. } ) )
4338, 42breq12d 4666 . . . . . . . . . 10 |- ( ( iota_ x e. A A. y e. A -. x <s y ) = x -> ( ( Z |` suc dom ( iota_ x e. A A. y e. A -. x <s y ) ) <s ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) <-> ( Z |` suc dom x ) <s ( x u. { <. dom x , 2o >. } ) ) )
4443notbid 308 . . . . . . . . 9 |- ( ( iota_ x e. A A. y e. A -. x <s y ) = x -> ( -. ( Z |` suc dom ( iota_ x e. A A. y e. A -. x <s y ) ) <s ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) <-> -. ( Z |` suc dom x ) <s ( x u. { <. dom x , 2o >. } ) ) )
4534, 44syl5ibrcom 237 . . . . . . . 8 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( ( iota_ x e. A A. y e. A -. x <s y ) = x -> -. ( Z |` suc dom ( iota_ x e. A A. y e. A -. x <s y ) ) <s ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) ) )
4632, 45mpd 15 . . . . . . 7 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> -. ( Z |` suc dom ( iota_ x e. A A. y e. A -. x <s y ) ) <s ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) )
47 iftrue 4092 . . . . . . . . . . . . . 14 |- ( E. x e. A A. y e. A -. x <s y -> if ( E. x e. A A. y e. A -. x <s y , ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ) = ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) )
483, 47syl5eq 2668 . . . . . . . . . . . . 13 |- ( E. x e. A A. y e. A -. x <s y -> S = ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) )
4923, 48syl 17 . . . . . . . . . . . 12 |- ( ( x e. A /\ A. y e. A -. x <s y ) -> S = ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) )
5049dmeqd 5326 . . . . . . . . . . 11 |- ( ( x e. A /\ A. y e. A -. x <s y ) -> dom S = dom ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) )
51 2on 7568 . . . . . . . . . . . . . . 15 |- 2o e. On
5251elexi 3213 . . . . . . . . . . . . . 14 |- 2o e. _V
5352dmsnop 5609 . . . . . . . . . . . . 13 |- dom { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } = { dom ( iota_ x e. A A. y e. A -. x <s y ) }
5453uneq2i 3764 . . . . . . . . . . . 12 |- ( dom ( iota_ x e. A A. y e. A -. x <s y ) u. dom { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) = ( dom ( iota_ x e. A A. y e. A -. x <s y ) u. { dom ( iota_ x e. A A. y e. A -. x <s y ) } )
55 dmun 5331 . . . . . . . . . . . 12 |- dom ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) = ( dom ( iota_ x e. A A. y e. A -. x <s y ) u. dom { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } )
56 df-suc 5729 . . . . . . . . . . . 12 |- suc dom ( iota_ x e. A A. y e. A -. x <s y ) = ( dom ( iota_ x e. A A. y e. A -. x <s y ) u. { dom ( iota_ x e. A A. y e. A -. x <s y ) } )
5754, 55, 563eqtr4i 2654 . . . . . . . . . . 11 |- dom ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) = suc dom ( iota_ x e. A A. y e. A -. x <s y )
5850, 57syl6eq 2672 . . . . . . . . . 10 |- ( ( x e. A /\ A. y e. A -. x <s y ) -> dom S = suc dom ( iota_ x e. A A. y e. A -. x <s y ) )
5958reseq2d 5396 . . . . . . . . 9 |- ( ( x e. A /\ A. y e. A -. x <s y ) -> ( Z |` dom S ) = ( Z |` suc dom ( iota_ x e. A A. y e. A -. x <s y ) ) )
6059adantr 481 . . . . . . . 8 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( Z |` dom S ) = ( Z |` suc dom ( iota_ x e. A A. y e. A -. x <s y ) ) )
6149adantr 481 . . . . . . . 8 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> S = ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) )
6260, 61breq12d 4666 . . . . . . 7 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( ( Z |` dom S ) <s S <-> ( Z |` suc dom ( iota_ x e. A A. y e. A -. x <s y ) ) <s ( ( iota_ x e. A A. y e. A -. x <s y ) u. { <. dom ( iota_ x e. A A. y e. A -. x <s y ) , 2o >. } ) ) )
6346, 62mtbird 315 . . . . . 6 |- ( ( ( x e. A /\ A. y e. A -. x <s y ) /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> -. ( Z |` dom S ) <s S )
6463exp31 630 . . . . 5 |- ( x e. A -> ( A. y e. A -. x <s y -> ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> -. ( Z |` dom S ) <s S ) ) )
6521, 64rexlimi 3024 . . . 4 |- ( E. x e. A A. y e. A -. x <s y -> ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> -. ( Z |` dom S ) <s S ) )
6665imp 445 . . 3 |- ( ( E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> -. ( Z |` dom S ) <s S )
673nosupno 31849 . . . . . . . 8 |- ( ( A C_ No /\ A e. _V ) -> S e. No )
68673adant3 1081 . . . . . . 7 |- ( ( A C_ No /\ A e. _V /\ Z e. No ) -> S e. No )
6968ad2antrl 764 . . . . . 6 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> S e. No )
70 nodmon 31803 . . . . . . 7 |- ( S e. No -> dom S e. On )
7169, 70syl 17 . . . . . 6 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> dom S e. On )
72 noreson 31813 . . . . . 6 |- ( ( S e. No /\ dom S e. On ) -> ( S |` dom S ) e. No )
7369, 71, 72syl2anc 693 . . . . 5 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( S |` dom S ) e. No )
74 simprl3 1108 . . . . . 6 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> Z e. No )
75 noreson 31813 . . . . . 6 |- ( ( Z e. No /\ dom S e. On ) -> ( Z |` dom S ) e. No )
7674, 71, 75syl2anc 693 . . . . 5 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( Z |` dom S ) e. No )
77 dmres 5419 . . . . . . 7 |- dom ( S |` dom S ) = ( dom S i^i dom S )
78 inss2 3834 . . . . . . 7 |- ( dom S i^i dom S ) C_ dom S
7977, 78eqsstri 3635 . . . . . 6 |- dom ( S |` dom S ) C_ dom S
8079a1i 11 . . . . 5 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> dom ( S |` dom S ) C_ dom S )
81 dmres 5419 . . . . . . 7 |- dom ( Z |` dom S ) = ( dom S i^i dom Z )
82 inss1 3833 . . . . . . 7 |- ( dom S i^i dom Z ) C_ dom S
8381, 82eqsstri 3635 . . . . . 6 |- dom ( Z |` dom S ) C_ dom S
8483a1i 11 . . . . 5 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> dom ( Z |` dom S ) C_ dom S )
853nosupdm 31850 . . . . . . . . . . 11 |- ( -. E. x e. A A. y e. A -. x <s y -> dom S = { g | E. p e. A ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) } )
8685abeq2d 2734 . . . . . . . . . 10 |- ( -. E. x e. A A. y e. A -. x <s y -> ( g e. dom S <-> E. p e. A ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) )
8786adantr 481 . . . . . . . . 9 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( g e. dom S <-> E. p e. A ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) )
88 simprl 794 . . . . . . . . . . . . . 14 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p e. A )
89 simplrr 801 . . . . . . . . . . . . . 14 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A. a e. A a <s Z )
90 breq1 4656 . . . . . . . . . . . . . . 15 |- ( a = p -> ( a <s Z <-> p <s Z ) )
9190rspcv 3305 . . . . . . . . . . . . . 14 |- ( p e. A -> ( A. a e. A a <s Z -> p <s Z ) )
9288, 89, 91sylc 65 . . . . . . . . . . . . 13 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p <s Z )
93 simprl1 1106 . . . . . . . . . . . . . . . 16 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> A C_ No )
9493adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A C_ No )
9594, 88sseldd 3604 . . . . . . . . . . . . . 14 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> p e. No )
9674adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> Z e. No )
97 sltso 31827 . . . . . . . . . . . . . . 15 |- <s Or No
98 soasym 31657 . . . . . . . . . . . . . . 15 |- ( ( <s Or No /\ ( p e. No /\ Z e. No ) ) -> ( p <s Z -> -. Z <s p ) )
9997, 98mpan 706 . . . . . . . . . . . . . 14 |- ( ( p e. No /\ Z e. No ) -> ( p <s Z -> -. Z <s p ) )
10095, 96, 99syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( p <s Z -> -. Z <s p ) )
10192, 100mpd 15 . . . . . . . . . . . 12 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. Z <s p )
102 nodmon 31803 . . . . . . . . . . . . . . . 16 |- ( p e. No -> dom p e. On )
10395, 102syl 17 . . . . . . . . . . . . . . 15 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> dom p e. On )
104 simprrl 804 . . . . . . . . . . . . . . 15 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> g e. dom p )
105 onelon 5748 . . . . . . . . . . . . . . 15 |- ( ( dom p e. On /\ g e. dom p ) -> g e. On )
106103, 104, 105syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> g e. On )
107 sucelon 7017 . . . . . . . . . . . . . 14 |- ( g e. On <-> suc g e. On )
108106, 107sylib 208 . . . . . . . . . . . . 13 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> suc g e. On )
109 sltres 31815 . . . . . . . . . . . . 13 |- ( ( Z e. No /\ p e. No /\ suc g e. On ) -> ( ( Z |` suc g ) <s ( p |` suc g ) -> Z <s p ) )
11096, 95, 108, 109syl3anc 1326 . . . . . . . . . . . 12 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( ( Z |` suc g ) <s ( p |` suc g ) -> Z <s p ) )
111101, 110mtod 189 . . . . . . . . . . 11 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. ( Z |` suc g ) <s ( p |` suc g ) )
112 simpll 790 . . . . . . . . . . . . 13 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. E. x e. A A. y e. A -. x <s y )
113 simprl2 1107 . . . . . . . . . . . . . . 15 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> A e. _V )
11493, 113jca 554 . . . . . . . . . . . . . 14 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( A C_ No /\ A e. _V ) )
115114adantr 481 . . . . . . . . . . . . 13 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( A C_ No /\ A e. _V ) )
116 simprrr 805 . . . . . . . . . . . . . 14 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) )
117 breq1 4656 . . . . . . . . . . . . . . . . 17 |- ( v = q -> ( v <s p <-> q <s p ) )
118117notbid 308 . . . . . . . . . . . . . . . 16 |- ( v = q -> ( -. v <s p <-> -. q <s p ) )
119 reseq1 5390 . . . . . . . . . . . . . . . . 17 |- ( v = q -> ( v |` suc g ) = ( q |` suc g ) )
120119eqeq2d 2632 . . . . . . . . . . . . . . . 16 |- ( v = q -> ( ( p |` suc g ) = ( v |` suc g ) <-> ( p |` suc g ) = ( q |` suc g ) ) )
121118, 120imbi12d 334 . . . . . . . . . . . . . . 15 |- ( v = q -> ( ( -. v <s p -> ( p |` suc g ) = ( v |` suc g ) ) <-> ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) )
122121cbvralv 3171 . . . . . . . . . . . . . 14 |- ( A. v e. A ( -. v <s p -> ( p |` suc g ) = ( v |` suc g ) ) <-> A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) )
123116, 122sylibr 224 . . . . . . . . . . . . 13 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> A. v e. A ( -. v <s p -> ( p |` suc g ) = ( v |` suc g ) ) )
1243nosupres 31853 . . . . . . . . . . . . 13 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( A C_ No /\ A e. _V ) /\ ( p e. A /\ g e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc g ) = ( v |` suc g ) ) ) ) -> ( S |` suc g ) = ( p |` suc g ) )
125112, 115, 88, 104, 123, 124syl113anc 1338 . . . . . . . . . . . 12 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( S |` suc g ) = ( p |` suc g ) )
126125breq2d 4665 . . . . . . . . . . 11 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> ( ( Z |` suc g ) <s ( S |` suc g ) <-> ( Z |` suc g ) <s ( p |` suc g ) ) )
127111, 126mtbird 315 . . . . . . . . . 10 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ ( p e. A /\ ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) ) ) -> -. ( Z |` suc g ) <s ( S |` suc g ) )
128127rexlimdvaa 3032 . . . . . . . . 9 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( E. p e. A ( g e. dom p /\ A. q e. A ( -. q <s p -> ( p |` suc g ) = ( q |` suc g ) ) ) -> -. ( Z |` suc g ) <s ( S |` suc g ) ) )
12987, 128sylbid 230 . . . . . . . 8 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( g e. dom S -> -. ( Z |` suc g ) <s ( S |` suc g ) ) )
130129imp 445 . . . . . . 7 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ g e. dom S ) -> -. ( Z |` suc g ) <s ( S |` suc g ) )
13169adantr 481 . . . . . . . . . . 11 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ g e. dom S ) -> S e. No )
132 nodmord 31806 . . . . . . . . . . 11 |- ( S e. No -> Ord dom S )
133131, 132syl 17 . . . . . . . . . 10 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ g e. dom S ) -> Ord dom S )
134 simpr 477 . . . . . . . . . 10 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ g e. dom S ) -> g e. dom S )
135 ordsucss 7018 . . . . . . . . . 10 |- ( Ord dom S -> ( g e. dom S -> suc g C_ dom S ) )
136133, 134, 135sylc 65 . . . . . . . . 9 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ g e. dom S ) -> suc g C_ dom S )
137136resabs1d 5428 . . . . . . . 8 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ g e. dom S ) -> ( ( Z |` dom S ) |` suc g ) = ( Z |` suc g ) )
138136resabs1d 5428 . . . . . . . 8 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ g e. dom S ) -> ( ( S |` dom S ) |` suc g ) = ( S |` suc g ) )
139137, 138breq12d 4666 . . . . . . 7 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ g e. dom S ) -> ( ( ( Z |` dom S ) |` suc g ) <s ( ( S |` dom S ) |` suc g ) <-> ( Z |` suc g ) <s ( S |` suc g ) ) )
140130, 139mtbird 315 . . . . . 6 |- ( ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) /\ g e. dom S ) -> -. ( ( Z |` dom S ) |` suc g ) <s ( ( S |` dom S ) |` suc g ) )
141140ralrimiva 2966 . . . . 5 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> A. g e. dom S -. ( ( Z |` dom S ) |` suc g ) <s ( ( S |` dom S ) |` suc g ) )
142 noresle 31846 . . . . 5 |- ( ( ( ( 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 ) <s ( ( S |` dom S ) |` suc g ) ) ) -> -. ( Z |` dom S ) <s ( S |` dom S ) )
14373, 76, 80, 84, 141, 142syl23anc 1333 . . . 4 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> -. ( Z |` dom S ) <s ( S |` dom S ) )
144 nofun 31802 . . . . . . 7 |- ( S e. No -> Fun S )
14569, 144syl 17 . . . . . 6 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> Fun S )
146 funrel 5905 . . . . . 6 |- ( Fun S -> Rel S )
147 resdm 5441 . . . . . 6 |- ( Rel S -> ( S |` dom S ) = S )
148145, 146, 1473syl 18 . . . . 5 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( S |` dom S ) = S )
149148breq2d 4665 . . . 4 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> ( ( Z |` dom S ) <s ( S |` dom S ) <-> ( Z |` dom S ) <s S ) )
150143, 149mtbid 314 . . 3 |- ( ( -. E. x e. A A. y e. A -. x <s y /\ ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) ) -> -. ( Z |` dom S ) <s S )
15166, 150pm2.61ian 831 . 2 |- ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> -. ( Z |` dom S ) <s S )
152 simpll1 1100 . . . . . 6 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> A C_ No )
153 simpll2 1101 . . . . . 6 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> A e. _V )
154 simpr 477 . . . . . 6 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> a e. A )
1553nosupbnd1 31860 . . . . . 6 |- ( ( A C_ No /\ A e. _V /\ a e. A ) -> ( a |` dom S ) <s S )
156152, 153, 154, 155syl3anc 1326 . . . . 5 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> ( a |` dom S ) <s S )
157 simplr 792 . . . . 5 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> -. ( Z |` dom S ) <s S )
158 simpl1 1064 . . . . . . . 8 |- ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) -> A C_ No )
159158sselda 3603 . . . . . . 7 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> a e. No )
160152, 153, 67syl2anc 693 . . . . . . . 8 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> S e. No )
161160, 70syl 17 . . . . . . 7 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> dom S e. On )
162 noreson 31813 . . . . . . 7 |- ( ( a e. No /\ dom S e. On ) -> ( a |` dom S ) e. No )
163159, 161, 162syl2anc 693 . . . . . 6 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> ( a |` dom S ) e. No )
164 simpll3 1102 . . . . . . 7 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> Z e. No )
165164, 161, 75syl2anc 693 . . . . . 6 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> ( Z |` dom S ) e. No )
166 sotr3 31656 . . . . . . 7 |- ( ( <s Or No /\ ( ( a |` dom S ) e. No /\ S e. No /\ ( Z |` dom S ) e. No ) ) -> ( ( ( a |` dom S ) <s S /\ -. ( Z |` dom S ) <s S ) -> ( a |` dom S ) <s ( Z |` dom S ) ) )
16797, 166mpan 706 . . . . . 6 |- ( ( ( a |` dom S ) e. No /\ S e. No /\ ( Z |` dom S ) e. No ) -> ( ( ( a |` dom S ) <s S /\ -. ( Z |` dom S ) <s S ) -> ( a |` dom S ) <s ( Z |` dom S ) ) )
168163, 160, 165, 167syl3anc 1326 . . . . 5 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> ( ( ( a |` dom S ) <s S /\ -. ( Z |` dom S ) <s S ) -> ( a |` dom S ) <s ( Z |` dom S ) ) )
169156, 157, 168mp2and 715 . . . 4 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> ( a |` dom S ) <s ( Z |` dom S ) )
170 sltres 31815 . . . . 5 |- ( ( a e. No /\ Z e. No /\ dom S e. On ) -> ( ( a |` dom S ) <s ( Z |` dom S ) -> a <s Z ) )
171159, 164, 161, 170syl3anc 1326 . . . 4 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> ( ( a |` dom S ) <s ( Z |` dom S ) -> a <s Z ) )
172169, 171mpd 15 . . 3 |- ( ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) /\ a e. A ) -> a <s Z )
173172ralrimiva 2966 . 2 |- ( ( ( A C_ No /\ A e. _V /\ Z e. No ) /\ -. ( Z |` dom S ) <s S ) -> A. a e. A a <s Z )
174151, 173impbida 877 1 |- ( ( A C_ No /\ A e. _V /\ Z e. No ) -> ( A. a e. A a <s Z <-> -. ( Z |` dom S ) <s S ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   A.wral 2912   E.wrex 2913   E!wreu 2914   E*wrmo 2915   _Vcvv 3200   u. cun 3572   i^i cin 3573   C_ wss 3574   ifcif 4086   {csn 4177   <.cop 4183   class class class wbr 4653   |-> cmpt 4729   Or wor 5034   dom cdm 5114   |` cres 5116   Rel wrel 5119   Ord word 5722   Oncon0 5723   suc csuc 5725   iotacio 5849   Fun wfun 5882   ` cfv 5888   iota_crio 6610   2oc2o 7554   Nocsur 31793   <scslt 31794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-ord 5726  df-on 5727  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-1o 7560  df-2o 7561  df-no 31796  df-slt 31797  df-bday 31798
This theorem is referenced by:  noetalem3  31865
  Copyright terms: Public domain W3C validator