Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nosupbnd2lem1 Structured version   Visualization version   Unicode version
Theorem nosupbnd2lem1 31861
Description: Bounding law from above when a set of surreals has a maximum. (Contributed by Scott Fenton, 6-Dec-2021.)
Assertion
Ref Expression
nosupbnd2lem1 |- ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) )
Distinct variable groups:   A, a   U, a   Z, a
Allowed substitution hints:   A( y)   U( y)   Z( y)
Proof of Theorem nosupbnd2lem1
Dummy variables q p x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1l 1085 . . 3 |- ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> U e. A )
2 simp3 1063 . . 3 |- ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> A. a e. A a <s Z )
3 breq1 4656 . . . 4 |- ( a = U -> ( a <s Z <-> U <s Z ) )
43rspcv 3305 . . 3 |- ( U e. A -> ( A. a e. A a <s Z -> U <s Z ) )
51, 2, 4sylc 65 . 2 |- ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> U <s Z )
6 simpl21 1139 . . . . 5 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> A C_ No )
7 simpl1l 1112 . . . . 5 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> U e. A )
86, 7sseldd 3604 . . . 4 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> U e. No )
9 simpl23 1141 . . . 4 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> Z e. No )
10 simp21 1094 . . . . . . . . . 10 |- ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> A C_ No )
1110, 1sseldd 3604 . . . . . . . . 9 |- ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> U e. No )
12 sltso 31827 . . . . . . . . . 10 |- <s Or No
13 sonr 5056 . . . . . . . . . 10 |- ( ( <s Or No /\ U e. No ) -> -. U <s U )
1412, 13mpan 706 . . . . . . . . 9 |- ( U e. No -> -. U <s U )
1511, 14syl 17 . . . . . . . 8 |- ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> -. U <s U )
16 breq2 4657 . . . . . . . . 9 |- ( U = Z -> ( U <s U <-> U <s Z ) )
1716notbid 308 . . . . . . . 8 |- ( U = Z -> ( -. U <s U <-> -. U <s Z ) )
1815, 17syl5ibcom 235 . . . . . . 7 |- ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> ( U = Z -> -. U <s Z ) )
1918con2d 129 . . . . . 6 |- ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> ( U <s Z -> -. U = Z ) )
2019imp 445 . . . . 5 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> -. U = Z )
2120neqned 2801 . . . 4 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> U =/= Z )
22 nosepssdm 31836 . . . 4 |- ( ( U e. No /\ Z e. No /\ U =/= Z ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U )
238, 9, 21, 22syl3anc 1326 . . 3 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U )
24 nosepon 31818 . . . . . 6 |- ( ( U e. No /\ Z e. No /\ U =/= Z ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On )
258, 9, 21, 24syl3anc 1326 . . . . 5 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On )
26 nodmon 31803 . . . . . 6 |- ( U e. No -> dom U e. On )
278, 26syl 17 . . . . 5 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> dom U e. On )
28 onsseleq 5765 . . . . 5 |- ( ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On /\ dom U e. On ) -> ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U <-> ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U \/ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) ) )
2925, 27, 28syl2anc 693 . . . 4 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U <-> ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U \/ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) ) )
308adantr 481 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> U e. No )
319adantr 481 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> Z e. No )
3221adantr 481 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> U =/= Z )
3330, 31, 32, 24syl3anc 1326 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On )
34 onelon 5748 . . . . . . . . . . . . . . . 16 |- ( ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> q e. On )
3533, 34sylan 488 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> q e. On )
36 simpr 477 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } )
37 fveq2 6191 . . . . . . . . . . . . . . . . 17 |- ( x = q -> ( U ` x ) = ( U ` q ) )
38 fveq2 6191 . . . . . . . . . . . . . . . . 17 |- ( x = q -> ( Z ` x ) = ( Z ` q ) )
3937, 38neeq12d 2855 . . . . . . . . . . . . . . . 16 |- ( x = q -> ( ( U ` x ) =/= ( Z ` x ) <-> ( U ` q ) =/= ( Z ` q ) ) )
4039onnminsb 7004 . . . . . . . . . . . . . . 15 |- ( q e. On -> ( q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } -> -. ( U ` q ) =/= ( Z ` q ) ) )
4135, 36, 40sylc 65 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> -. ( U ` q ) =/= ( Z ` q ) )
42 df-ne 2795 . . . . . . . . . . . . . . 15 |- ( ( U ` q ) =/= ( Z ` q ) <-> -. ( U ` q ) = ( Z ` q ) )
4342con2bii 347 . . . . . . . . . . . . . 14 |- ( ( U ` q ) = ( Z ` q ) <-> -. ( U ` q ) =/= ( Z ` q ) )
4441, 43sylibr 224 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> ( U ` q ) = ( Z ` q ) )
45 simplr 792 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U )
4627adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> dom U e. On )
4746adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> dom U e. On )
48 ontr1 5771 . . . . . . . . . . . . . . . 16 |- ( dom U e. On -> ( ( q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> q e. dom U ) )
4947, 48syl 17 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> ( ( q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> q e. dom U ) )
5036, 45, 49mp2and 715 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> q e. dom U )
5150fvresd 6208 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> ( ( Z |` dom U ) ` q ) = ( Z ` q ) )
5244, 51eqtr4d 2659 . . . . . . . . . . . 12 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> ( U ` q ) = ( ( Z |` dom U ) ` q ) )
5352ralrimiva 2966 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> A. q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ( U ` q ) = ( ( Z |` dom U ) ` q ) )
54 simplr 792 . . . . . . . . . . . . 13 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> U <s Z )
55 sltval2 31809 . . . . . . . . . . . . . 14 |- ( ( U e. No /\ Z e. No ) -> ( U <s Z <-> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) ) )
5630, 31, 55syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( U <s Z <-> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) ) )
5754, 56mpbid 222 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
58 simpr 477 . . . . . . . . . . . . 13 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U )
5958fvresd 6208 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( ( Z |` dom U ) ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
6057, 59breqtrrd 4681 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( Z |` dom U ) ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
61 raleq 3138 . . . . . . . . . . . . 13 |- ( p = |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } -> ( A. q e. p ( U ` q ) = ( ( Z |` dom U ) ` q ) <-> A. q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ( U ` q ) = ( ( Z |` dom U ) ` q ) ) )
62 fveq2 6191 . . . . . . . . . . . . . 14 |- ( p = |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } -> ( U ` p ) = ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
63 fveq2 6191 . . . . . . . . . . . . . 14 |- ( p = |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } -> ( ( Z |` dom U ) ` p ) = ( ( Z |` dom U ) ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
6462, 63breq12d 4666 . . . . . . . . . . . . 13 |- ( p = |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } -> ( ( U ` p ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( Z |` dom U ) ` p ) <-> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( Z |` dom U ) ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) ) )
6561, 64anbi12d 747 . . . . . . . . . . . 12 |- ( p = |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } -> ( ( A. q e. p ( U ` q ) = ( ( Z |` dom U ) ` q ) /\ ( U ` p ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( Z |` dom U ) ` p ) ) <-> ( A. q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ( U ` q ) = ( ( Z |` dom U ) ` q ) /\ ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( Z |` dom U ) ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) ) ) )
6665rspcev 3309 . . . . . . . . . . 11 |- ( ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On /\ ( A. q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ( U ` q ) = ( ( Z |` dom U ) ` q ) /\ ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( Z |` dom U ) ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) ) ) -> E. p e. On ( A. q e. p ( U ` q ) = ( ( Z |` dom U ) ` q ) /\ ( U ` p ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( Z |` dom U ) ` p ) ) )
6733, 53, 60, 66syl12anc 1324 . . . . . . . . . 10 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> E. p e. On ( A. q e. p ( U ` q ) = ( ( Z |` dom U ) ` q ) /\ ( U ` p ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( Z |` dom U ) ` p ) ) )
68 noreson 31813 . . . . . . . . . . . 12 |- ( ( Z e. No /\ dom U e. On ) -> ( Z |` dom U ) e. No )
6931, 46, 68syl2anc 693 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( Z |` dom U ) e. No )
70 sltval 31800 . . . . . . . . . . 11 |- ( ( U e. No /\ ( Z |` dom U ) e. No ) -> ( U <s ( Z |` dom U ) <-> E. p e. On ( A. q e. p ( U ` q ) = ( ( Z |` dom U ) ` q ) /\ ( U ` p ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( Z |` dom U ) ` p ) ) ) )
7130, 69, 70syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( U <s ( Z |` dom U ) <-> E. p e. On ( A. q e. p ( U ` q ) = ( ( Z |` dom U ) ` q ) /\ ( U ` p ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( Z |` dom U ) ` p ) ) ) )
7267, 71mpbird 247 . . . . . . . . 9 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> U <s ( Z |` dom U ) )
73 df-res 5126 . . . . . . . . . . . . 13 |- ( { <. dom U , 2o >. } |` dom U ) = ( { <. dom U , 2o >. } i^i ( dom U X. _V ) )
74 2on 7568 . . . . . . . . . . . . . . . 16 |- 2o e. On
75 xpsng 6406 . . . . . . . . . . . . . . . 16 |- ( ( dom U e. On /\ 2o e. On ) -> ( { dom U } X. { 2o } ) = { <. dom U , 2o >. } )
7646, 74, 75sylancl 694 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( { dom U } X. { 2o } ) = { <. dom U , 2o >. } )
7776ineq1d 3813 . . . . . . . . . . . . . 14 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( ( { dom U } X. { 2o } ) i^i ( dom U X. _V ) ) = ( { <. dom U , 2o >. } i^i ( dom U X. _V ) ) )
78 incom 3805 . . . . . . . . . . . . . . . 16 |- ( { dom U } i^i dom U ) = ( dom U i^i { dom U } )
79 nodmord 31806 . . . . . . . . . . . . . . . . . 18 |- ( U e. No -> Ord dom U )
80 ordirr 5741 . . . . . . . . . . . . . . . . . 18 |- ( Ord dom U -> -. dom U e. dom U )
8130, 79, 803syl 18 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> -. dom U e. dom U )
82 disjsn 4246 . . . . . . . . . . . . . . . . 17 |- ( ( dom U i^i { dom U } ) = (/) <-> -. dom U e. dom U )
8381, 82sylibr 224 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( dom U i^i { dom U } ) = (/) )
8478, 83syl5eq 2668 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( { dom U } i^i dom U ) = (/) )
85 xpdisj1 5555 . . . . . . . . . . . . . . 15 |- ( ( { dom U } i^i dom U ) = (/) -> ( ( { dom U } X. { 2o } ) i^i ( dom U X. _V ) ) = (/) )
8684, 85syl 17 . . . . . . . . . . . . . 14 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( ( { dom U } X. { 2o } ) i^i ( dom U X. _V ) ) = (/) )
8777, 86eqtr3d 2658 . . . . . . . . . . . . 13 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( { <. dom U , 2o >. } i^i ( dom U X. _V ) ) = (/) )
8873, 87syl5eq 2668 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( { <. dom U , 2o >. } |` dom U ) = (/) )
8988uneq2d 3767 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( ( U |` dom U ) u. ( { <. dom U , 2o >. } |` dom U ) ) = ( ( U |` dom U ) u. (/) ) )
90 resundir 5411 . . . . . . . . . . 11 |- ( ( U u. { <. dom U , 2o >. } ) |` dom U ) = ( ( U |` dom U ) u. ( { <. dom U , 2o >. } |` dom U ) )
91 un0 3967 . . . . . . . . . . . 12 |- ( ( U |` dom U ) u. (/) ) = ( U |` dom U )
9291eqcomi 2631 . . . . . . . . . . 11 |- ( U |` dom U ) = ( ( U |` dom U ) u. (/) )
9389, 90, 923eqtr4g 2681 . . . . . . . . . 10 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( ( U u. { <. dom U , 2o >. } ) |` dom U ) = ( U |` dom U ) )
94 nofun 31802 . . . . . . . . . . . 12 |- ( U e. No -> Fun U )
9530, 94syl 17 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> Fun U )
96 funrel 5905 . . . . . . . . . . 11 |- ( Fun U -> Rel U )
97 resdm 5441 . . . . . . . . . . 11 |- ( Rel U -> ( U |` dom U ) = U )
9895, 96, 973syl 18 . . . . . . . . . 10 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( U |` dom U ) = U )
9993, 98eqtrd 2656 . . . . . . . . 9 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( ( U u. { <. dom U , 2o >. } ) |` dom U ) = U )
100 sssucid 5802 . . . . . . . . . 10 |- dom U C_ suc dom U
101 resabs1 5427 . . . . . . . . . 10 |- ( dom U C_ suc dom U -> ( ( Z |` suc dom U ) |` dom U ) = ( Z |` dom U ) )
102100, 101mp1i 13 . . . . . . . . 9 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( ( Z |` suc dom U ) |` dom U ) = ( Z |` dom U ) )
10372, 99, 1023brtr4d 4685 . . . . . . . 8 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( ( U u. { <. dom U , 2o >. } ) |` dom U ) <s ( ( Z |` suc dom U ) |` dom U ) )
10474elexi 3213 . . . . . . . . . . . . 13 |- 2o e. _V
105104prid2 4298 . . . . . . . . . . . 12 |- 2o e. { 1o , 2o }
106105noextend 31819 . . . . . . . . . . 11 |- ( U e. No -> ( U u. { <. dom U , 2o >. } ) e. No )
1078, 106syl 17 . . . . . . . . . 10 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> ( U u. { <. dom U , 2o >. } ) e. No )
108107adantr 481 . . . . . . . . 9 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( U u. { <. dom U , 2o >. } ) e. No )
109 sucelon 7017 . . . . . . . . . . . 12 |- ( dom U e. On <-> suc dom U e. On )
11027, 109sylib 208 . . . . . . . . . . 11 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> suc dom U e. On )
111 noreson 31813 . . . . . . . . . . 11 |- ( ( Z e. No /\ suc dom U e. On ) -> ( Z |` suc dom U ) e. No )
1129, 110, 111syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> ( Z |` suc dom U ) e. No )
113112adantr 481 . . . . . . . . 9 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( Z |` suc dom U ) e. No )
114 sltres 31815 . . . . . . . . 9 |- ( ( ( U u. { <. dom U , 2o >. } ) e. No /\ ( Z |` suc dom U ) e. No /\ dom U e. On ) -> ( ( ( U u. { <. dom U , 2o >. } ) |` dom U ) <s ( ( Z |` suc dom U ) |` dom U ) -> ( U u. { <. dom U , 2o >. } ) <s ( Z |` suc dom U ) ) )
115108, 113, 46, 114syl3anc 1326 . . . . . . . 8 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( ( ( U u. { <. dom U , 2o >. } ) |` dom U ) <s ( ( Z |` suc dom U ) |` dom U ) -> ( U u. { <. dom U , 2o >. } ) <s ( Z |` suc dom U ) ) )
116103, 115mpd 15 . . . . . . 7 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( U u. { <. dom U , 2o >. } ) <s ( Z |` suc dom U ) )
117 soasym 31657 . . . . . . . . 9 |- ( ( <s Or No /\ ( ( U u. { <. dom U , 2o >. } ) e. No /\ ( Z |` suc dom U ) e. No ) ) -> ( ( U u. { <. dom U , 2o >. } ) <s ( Z |` suc dom U ) -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) ) )
11812, 117mpan 706 . . . . . . . 8 |- ( ( ( U u. { <. dom U , 2o >. } ) e. No /\ ( Z |` suc dom U ) e. No ) -> ( ( U u. { <. dom U , 2o >. } ) <s ( Z |` suc dom U ) -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) ) )
119108, 113, 118syl2anc 693 . . . . . . 7 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> ( ( U u. { <. dom U , 2o >. } ) <s ( Z |` suc dom U ) -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) ) )
120116, 119mpd 15 . . . . . 6 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) )
121 df-suc 5729 . . . . . . . . . 10 |- suc dom U = ( dom U u. { dom U } )
122121reseq2i 5393 . . . . . . . . 9 |- ( Z |` suc dom U ) = ( Z |` ( dom U u. { dom U } ) )
123 resundi 5410 . . . . . . . . 9 |- ( Z |` ( dom U u. { dom U } ) ) = ( ( Z |` dom U ) u. ( Z |` { dom U } ) )
124122, 123eqtri 2644 . . . . . . . 8 |- ( Z |` suc dom U ) = ( ( Z |` dom U ) u. ( Z |` { dom U } ) )
125 dmres 5419 . . . . . . . . . . 11 |- dom ( Z |` dom U ) = ( dom U i^i dom Z )
126 simpr 477 . . . . . . . . . . . . 13 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U )
127 necom 2847 . . . . . . . . . . . . . . . . 17 |- ( ( U ` x ) =/= ( Z ` x ) <-> ( Z ` x ) =/= ( U ` x ) )
128127a1i 11 . . . . . . . . . . . . . . . 16 |- ( x e. On -> ( ( U ` x ) =/= ( Z ` x ) <-> ( Z ` x ) =/= ( U ` x ) ) )
129128rabbiia 3185 . . . . . . . . . . . . . . 15 |- { x e. On | ( U ` x ) =/= ( Z ` x ) } = { x e. On | ( Z ` x ) =/= ( U ` x ) }
130129inteqi 4479 . . . . . . . . . . . . . 14 |- |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = |^| { x e. On | ( Z ` x ) =/= ( U ` x ) }
1319adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> Z e. No )
1328adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> U e. No )
13321adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> U =/= Z )
134133necomd 2849 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> Z =/= U )
135 nosepssdm 31836 . . . . . . . . . . . . . . 15 |- ( ( Z e. No /\ U e. No /\ Z =/= U ) -> |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } C_ dom Z )
136131, 132, 134, 135syl3anc 1326 . . . . . . . . . . . . . 14 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } C_ dom Z )
137130, 136syl5eqss 3649 . . . . . . . . . . . . 13 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom Z )
138126, 137eqsstr3d 3640 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> dom U C_ dom Z )
139 df-ss 3588 . . . . . . . . . . . 12 |- ( dom U C_ dom Z <-> ( dom U i^i dom Z ) = dom U )
140138, 139sylib 208 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( dom U i^i dom Z ) = dom U )
141125, 140syl5eq 2668 . . . . . . . . . 10 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> dom ( Z |` dom U ) = dom U )
142141eleq2d 2687 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( q e. dom ( Z |` dom U ) <-> q e. dom U ) )
143 simpr 477 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) /\ q e. dom U ) -> q e. dom U )
144143fvresd 6208 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) /\ q e. dom U ) -> ( ( Z |` dom U ) ` q ) = ( Z ` q ) )
145132, 26syl 17 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> dom U e. On )
146 onelon 5748 . . . . . . . . . . . . . . . . 17 |- ( ( dom U e. On /\ q e. dom U ) -> q e. On )
147145, 146sylan 488 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) /\ q e. dom U ) -> q e. On )
148126eleq2d 2687 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } <-> q e. dom U ) )
149148biimpar 502 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) /\ q e. dom U ) -> q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } )
150147, 149, 40sylc 65 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) /\ q e. dom U ) -> -. ( U ` q ) =/= ( Z ` q ) )
151 nesym 2850 . . . . . . . . . . . . . . . 16 |- ( ( U ` q ) =/= ( Z ` q ) <-> -. ( Z ` q ) = ( U ` q ) )
152151con2bii 347 . . . . . . . . . . . . . . 15 |- ( ( Z ` q ) = ( U ` q ) <-> -. ( U ` q ) =/= ( Z ` q ) )
153150, 152sylibr 224 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) /\ q e. dom U ) -> ( Z ` q ) = ( U ` q ) )
154144, 153eqtrd 2656 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) /\ q e. dom U ) -> ( ( Z |` dom U ) ` q ) = ( U ` q ) )
155154ex 450 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( q e. dom U -> ( ( Z |` dom U ) ` q ) = ( U ` q ) ) )
156142, 155sylbid 230 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( q e. dom ( Z |` dom U ) -> ( ( Z |` dom U ) ` q ) = ( U ` q ) ) )
157156ralrimiv 2965 . . . . . . . . . 10 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> A. q e. dom ( Z |` dom U ) ( ( Z |` dom U ) ` q ) = ( U ` q ) )
158 nofun 31802 . . . . . . . . . . . 12 |- ( Z e. No -> Fun Z )
159 funres 5929 . . . . . . . . . . . 12 |- ( Fun Z -> Fun ( Z |` dom U ) )
160131, 158, 1593syl 18 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> Fun ( Z |` dom U ) )
161132, 94syl 17 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> Fun U )
162 eqfunfv 6316 . . . . . . . . . . 11 |- ( ( Fun ( Z |` dom U ) /\ Fun U ) -> ( ( Z |` dom U ) = U <-> ( dom ( Z |` dom U ) = dom U /\ A. q e. dom ( Z |` dom U ) ( ( Z |` dom U ) ` q ) = ( U ` q ) ) ) )
163160, 161, 162syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( ( Z |` dom U ) = U <-> ( dom ( Z |` dom U ) = dom U /\ A. q e. dom ( Z |` dom U ) ( ( Z |` dom U ) ` q ) = ( U ` q ) ) ) )
164141, 157, 163mpbir2and 957 . . . . . . . . 9 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( Z |` dom U ) = U )
165131, 158syl 17 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> Fun Z )
166 funfn 5918 . . . . . . . . . . . 12 |- ( Fun Z <-> Z Fn dom Z )
167165, 166sylib 208 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> Z Fn dom Z )
168 1on 7567 . . . . . . . . . . . . . . . . . . . 20 |- 1o e. On
169168elexi 3213 . . . . . . . . . . . . . . . . . . 19 |- 1o e. _V
170169prid1 4297 . . . . . . . . . . . . . . . . . 18 |- 1o e. { 1o , 2o }
171170nosgnn0i 31812 . . . . . . . . . . . . . . . . 17 |- (/) =/= 1o
172132, 79syl 17 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> Ord dom U )
173 ndmfv 6218 . . . . . . . . . . . . . . . . . . 19 |- ( -. dom U e. dom U -> ( U ` dom U ) = (/) )
174172, 80, 1733syl 18 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( U ` dom U ) = (/) )
175174neeq1d 2853 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( ( U ` dom U ) =/= 1o <-> (/) =/= 1o ) )
176171, 175mpbiri 248 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( U ` dom U ) =/= 1o )
177176neneqd 2799 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> -. ( U ` dom U ) = 1o )
178177intnanrd 963 . . . . . . . . . . . . . 14 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> -. ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) )
179177intnanrd 963 . . . . . . . . . . . . . 14 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> -. ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) )
180 simplr 792 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> U <s Z )
181132, 131, 55syl2anc 693 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( U <s Z <-> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) ) )
182180, 181mpbid 222 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
183 fveq2 6191 . . . . . . . . . . . . . . . . 17 |- ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U -> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( U ` dom U ) )
184183adantl 482 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( U ` dom U ) )
185 fveq2 6191 . . . . . . . . . . . . . . . . 17 |- ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U -> ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( Z ` dom U ) )
186185adantl 482 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( Z ` dom U ) )
187182, 184, 1863brtr3d 4684 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( U ` dom U ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` dom U ) )
188 fvex 6201 . . . . . . . . . . . . . . . . 17 |- ( U ` dom U ) e. _V
189 fvex 6201 . . . . . . . . . . . . . . . . 17 |- ( Z ` dom U ) e. _V
190188, 189brtp 31639 . . . . . . . . . . . . . . . 16 |- ( ( U ` dom U ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` dom U ) <-> ( ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) \/ ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) ) )
191 3orrot 1044 . . . . . . . . . . . . . . . 16 |- ( ( ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) \/ ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) ) <-> ( ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) \/ ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) ) )
192 3orrot 1044 . . . . . . . . . . . . . . . 16 |- ( ( ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) \/ ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) ) <-> ( ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) ) )
193190, 191, 1923bitri 286 . . . . . . . . . . . . . . 15 |- ( ( U ` dom U ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` dom U ) <-> ( ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) ) )
194187, 193sylib 208 . . . . . . . . . . . . . 14 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) ) )
195178, 179, 194ecase23d 1436 . . . . . . . . . . . . 13 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) )
196195simprd 479 . . . . . . . . . . . 12 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( Z ` dom U ) = 2o )
197 ndmfv 6218 . . . . . . . . . . . . . 14 |- ( -. dom U e. dom Z -> ( Z ` dom U ) = (/) )
198105nosgnn0i 31812 . . . . . . . . . . . . . . . 16 |- (/) =/= 2o
199 neeq1 2856 . . . . . . . . . . . . . . . 16 |- ( ( Z ` dom U ) = (/) -> ( ( Z ` dom U ) =/= 2o <-> (/) =/= 2o ) )
200198, 199mpbiri 248 . . . . . . . . . . . . . . 15 |- ( ( Z ` dom U ) = (/) -> ( Z ` dom U ) =/= 2o )
201200neneqd 2799 . . . . . . . . . . . . . 14 |- ( ( Z ` dom U ) = (/) -> -. ( Z ` dom U ) = 2o )
202197, 201syl 17 . . . . . . . . . . . . 13 |- ( -. dom U e. dom Z -> -. ( Z ` dom U ) = 2o )
203202con4i 113 . . . . . . . . . . . 12 |- ( ( Z ` dom U ) = 2o -> dom U e. dom Z )
204196, 203syl 17 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> dom U e. dom Z )
205 fnressn 6425 . . . . . . . . . . 11 |- ( ( Z Fn dom Z /\ dom U e. dom Z ) -> ( Z |` { dom U } ) = { <. dom U , ( Z ` dom U ) >. } )
206167, 204, 205syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( Z |` { dom U } ) = { <. dom U , ( Z ` dom U ) >. } )
207196opeq2d 4409 . . . . . . . . . . 11 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> <. dom U , ( Z ` dom U ) >. = <. dom U , 2o >. )
208207sneqd 4189 . . . . . . . . . 10 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> { <. dom U , ( Z ` dom U ) >. } = { <. dom U , 2o >. } )
209206, 208eqtrd 2656 . . . . . . . . 9 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( Z |` { dom U } ) = { <. dom U , 2o >. } )
210164, 209uneq12d 3768 . . . . . . . 8 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( ( Z |` dom U ) u. ( Z |` { dom U } ) ) = ( U u. { <. dom U , 2o >. } ) )
211124, 210syl5eq 2668 . . . . . . 7 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> ( Z |` suc dom U ) = ( U u. { <. dom U , 2o >. } ) )
212 sonr 5056 . . . . . . . . 9 |- ( ( <s Or No /\ ( U u. { <. dom U , 2o >. } ) e. No ) -> -. ( U u. { <. dom U , 2o >. } ) <s ( U u. { <. dom U , 2o >. } ) )
21312, 212mpan 706 . . . . . . . 8 |- ( ( U u. { <. dom U , 2o >. } ) e. No -> -. ( U u. { <. dom U , 2o >. } ) <s ( U u. { <. dom U , 2o >. } ) )
214132, 106, 2133syl 18 . . . . . . 7 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> -. ( U u. { <. dom U , 2o >. } ) <s ( U u. { <. dom U , 2o >. } ) )
215211, 214eqnbrtrd 4671 . . . . . 6 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) )
216120, 215jaodan 826 . . . . 5 |- ( ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) /\ ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U \/ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) ) -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) )
217216ex 450 . . . 4 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> ( ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U \/ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) ) )
21829, 217sylbid 230 . . 3 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) ) )
21923, 218mpd 15 . 2 |- ( ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) /\ U <s Z ) -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) )
2205, 219mpdan 702 1 |- ( ( ( U e. A /\ A. y e. A -. U <s y ) /\ ( A C_ No /\ A e. _V /\ Z e. No ) /\ A. a e. A a <s Z ) -> -. ( Z |` suc dom U ) <s ( U u. { <. dom U , 2o >. } ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   {ctp 4181   <.cop 4183   |^|cint 4475   class class class wbr 4653   Or wor 5034   X. cxp 5112   dom cdm 5114   |` cres 5116   Rel wrel 5119   Ord word 5722   Oncon0 5723   suc csuc 5725   Fun wfun 5882   Fn wfn 5883   ` cfv 5888   1oc1o 7553   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-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-1o 7560  df-2o 7561  df-no 31796  df-slt 31797
This theorem is referenced by:  nosupbnd2  31862
  Copyright terms: Public domain W3C validator