Metamath Proof Explorer

Theorem nosupbnd2lem1

Description: Bounding law from above when a set of surreals has a maximum. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nosupbnd2lem1 
|- ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )

Proof

Step Hyp Ref Expression
1 simp1l 
 |-  ( ( ( U e. A /\ A. y e. A -. U  U e. A )
2 simp3 
 |-  ( ( ( U e. A /\ A. y e. A -. U  A. a e. A a
3 breq1 
 |-  ( a = U -> ( a  U
4 3 rspcv 
 |-  ( U e. A -> ( A. a e. A a  U
5 1 2 4 sylc 
 |-  ( ( ( U e. A /\ A. y e. A -. U  U
6 simpl21 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  A C_ No )
7 simpl1l 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  U e. A )
8 6 7 sseldd 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  U e. No )
9 simpl23 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  Z e. No )
10 simp21 
 |-  ( ( ( U e. A /\ A. y e. A -. U  A C_ No )
11 10 1 sseldd 
 |-  ( ( ( U e. A /\ A. y e. A -. U  U e. No )
12 sltso 
 |-
13 sonr 
 |-  ( (  -. U
14 12 13 mpan 
 |-  ( U e. No -> -. U
15 11 14 syl 
 |-  ( ( ( U e. A /\ A. y e. A -. U  -. U
16 breq2 
 |-  ( U = Z -> ( U  U
17 16 notbid 
 |-  ( U = Z -> ( -. U  -. U
18 15 17 syl5ibcom 
 |-  ( ( ( U e. A /\ A. y e. A -. U  ( U = Z -> -. U
19 18 con2d 
 |-  ( ( ( U e. A /\ A. y e. A -. U  ( U  -. U = Z ) )
20 19 imp 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  -. U = Z )
21 20 neqned 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  U =/= Z )
22 nosepssdm 
 |-  ( ( U e. No /\ Z e. No /\ U =/= Z ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U )
23 8 9 21 22 syl3anc 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U )
24 nosepon 
 |-  ( ( U e. No /\ Z e. No /\ U =/= Z ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On )
25 8 9 21 24 syl3anc 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On )
26 nodmon 
 |-  ( U e. No -> dom U e. On )
27 8 26 syl 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  dom U e. On )
28 onsseleq 
 |-  ( ( |^| { 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 ) ) )
29 25 27 28 syl2anc 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  ( |^| { 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 ) ) )
30 8 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  U e. No )
31 9 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Z e. No )
32 21 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  U =/= Z )
33 30 31 32 24 syl3anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On )
34 onelon 
 |-  ( ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On /\ q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) -> q e. On )
35 33 34 sylan 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  q e. On )
36 simpr 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } )
37 fveq2 
 |-  ( x = q -> ( U ` x ) = ( U ` q ) )
38 fveq2 
 |-  ( x = q -> ( Z ` x ) = ( Z ` q ) )
39 37 38 neeq12d 
 |-  ( x = q -> ( ( U ` x ) =/= ( Z ` x ) <-> ( U ` q ) =/= ( Z ` q ) ) )
40 39 onnminsb 
 |-  ( q e. On -> ( q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } -> -. ( U ` q ) =/= ( Z ` q ) ) )
41 35 36 40 sylc 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( U ` q ) =/= ( Z ` q ) )
42 df-ne 
 |-  ( ( U ` q ) =/= ( Z ` q ) <-> -. ( U ` q ) = ( Z ` q ) )
43 42 con2bii 
 |-  ( ( U ` q ) = ( Z ` q ) <-> -. ( U ` q ) =/= ( Z ` q ) )
44 41 43 sylibr 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` q ) = ( Z ` q ) )
45 simplr 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U )
46 27 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  dom U e. On )
47 46 adantr 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  dom U e. On )
48 ontr1 
 |-  ( 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 ) )
49 47 48 syl 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } /\ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U ) -> q e. dom U ) )
50 36 45 49 mp2and 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  q e. dom U )
51 50 fvresd 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` dom U ) ` q ) = ( Z ` q ) )
52 44 51 eqtr4d 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` q ) = ( ( Z |` dom U ) ` q ) )
53 52 ralrimiva 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  A. q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ( U ` q ) = ( ( Z |` dom U ) ` q ) )
54 simplr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  U
55 sltval2 
 |-  ( ( U e. No /\ Z e. No ) -> ( U  ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) ) )
56 30 31 55 syl2anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U  ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) ) )
57 54 56 mpbid 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
58 simpr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U )
59 58 fvresd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` dom U ) ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
60 57 59 breqtrrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. 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 
 |-  ( 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 
 |-  ( p = |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } -> ( U ` p ) = ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
63 fveq2 
 |-  ( p = |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } -> ( ( Z |` dom U ) ` p ) = ( ( Z |` dom U ) ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
64 62 63 breq12d 
 |-  ( 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 ) } ) ) )
65 61 64 anbi12d 
 |-  ( 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 ) } ) ) ) )
66 65 rspcev 
 |-  ( ( |^| { 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 ) ) )
67 33 53 60 66 syl12anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. 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 
 |-  ( ( Z e. No /\ dom U e. On ) -> ( Z |` dom U ) e. No )
69 31 46 68 syl2anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` dom U ) e. No )
70 sltval 
 |-  ( ( U e. No /\ ( Z |` dom U ) e. No ) -> ( 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 ) ) ) )
71 30 69 70 syl2anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( 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 ) ) ) )
72 67 71 mpbird 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  U
73 df-res 
 |-  ( { <. dom U , 2o >. } |` dom U ) = ( { <. dom U , 2o >. } i^i ( dom U X. _V ) )
74 2on 
 |-  2o e. On
75 xpsng 
 |-  ( ( dom U e. On /\ 2o e. On ) -> ( { dom U } X. { 2o } ) = { <. dom U , 2o >. } )
76 46 74 75 sylancl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( { dom U } X. { 2o } ) = { <. dom U , 2o >. } )
77 76 ineq1d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( { dom U } X. { 2o } ) i^i ( dom U X. _V ) ) = ( { <. dom U , 2o >. } i^i ( dom U X. _V ) ) )
78 incom 
 |-  ( { dom U } i^i dom U ) = ( dom U i^i { dom U } )
79 nodmord 
 |-  ( U e. No -> Ord dom U )
80 ordirr 
 |-  ( Ord dom U -> -. dom U e. dom U )
81 30 79 80 3syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. dom U e. dom U )
82 disjsn 
 |-  ( ( dom U i^i { dom U } ) = (/) <-> -. dom U e. dom U )
83 81 82 sylibr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( dom U i^i { dom U } ) = (/) )
84 78 83 syl5eq 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( { dom U } i^i dom U ) = (/) )
85 xpdisj1 
 |-  ( ( { dom U } i^i dom U ) = (/) -> ( ( { dom U } X. { 2o } ) i^i ( dom U X. _V ) ) = (/) )
86 84 85 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( { dom U } X. { 2o } ) i^i ( dom U X. _V ) ) = (/) )
87 77 86 eqtr3d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( { <. dom U , 2o >. } i^i ( dom U X. _V ) ) = (/) )
88 73 87 syl5eq 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( { <. dom U , 2o >. } |` dom U ) = (/) )
89 88 uneq2d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U |` dom U ) u. ( { <. dom U , 2o >. } |` dom U ) ) = ( ( U |` dom U ) u. (/) ) )
90 resundir 
 |-  ( ( U u. { <. dom U , 2o >. } ) |` dom U ) = ( ( U |` dom U ) u. ( { <. dom U , 2o >. } |` dom U ) )
91 un0 
 |-  ( ( U |` dom U ) u. (/) ) = ( U |` dom U )
92 91 eqcomi 
 |-  ( U |` dom U ) = ( ( U |` dom U ) u. (/) )
93 89 90 92 3eqtr4g 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U u. { <. dom U , 2o >. } ) |` dom U ) = ( U |` dom U ) )
94 nofun 
 |-  ( U e. No -> Fun U )
95 30 94 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Fun U )
96 funrel 
 |-  ( Fun U -> Rel U )
97 resdm 
 |-  ( Rel U -> ( U |` dom U ) = U )
98 95 96 97 3syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U |` dom U ) = U )
99 93 98 eqtrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U u. { <. dom U , 2o >. } ) |` dom U ) = U )
100 sssucid 
 |-  dom U C_ suc dom U
101 resabs1 
 |-  ( dom U C_ suc dom U -> ( ( Z |` suc dom U ) |` dom U ) = ( Z |` dom U ) )
102 100 101 mp1i 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` suc dom U ) |` dom U ) = ( Z |` dom U ) )
103 72 99 102 3brtr4d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U u. { <. dom U , 2o >. } ) |` dom U )
104 74 elexi 
 |-  2o e. _V
105 104 prid2 
 |-  2o e. { 1o , 2o }
106 105 noextend 
 |-  ( U e. No -> ( U u. { <. dom U , 2o >. } ) e. No )
107 8 106 syl 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  ( U u. { <. dom U , 2o >. } ) e. No )
108 107 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U u. { <. dom U , 2o >. } ) e. No )
109 sucelon 
 |-  ( dom U e. On <-> suc dom U e. On )
110 27 109 sylib 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  suc dom U e. On )
111 noreson 
 |-  ( ( Z e. No /\ suc dom U e. On ) -> ( Z |` suc dom U ) e. No )
112 9 110 111 syl2anc 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` suc dom U ) e. No )
113 112 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` suc dom U ) e. No )
114 sltres 
 |-  ( ( ( U u. { <. dom U , 2o >. } ) e. No /\ ( Z |` suc dom U ) e. No /\ dom U e. On ) -> ( ( ( U u. { <. dom U , 2o >. } ) |` dom U )  ( U u. { <. dom U , 2o >. } )
115 108 113 46 114 syl3anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( ( U u. { <. dom U , 2o >. } ) |` dom U )  ( U u. { <. dom U , 2o >. } )
116 103 115 mpd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U u. { <. dom U , 2o >. } )
117 soasym 
 |-  ( ( . } ) e. No /\ ( Z |` suc dom U ) e. No ) ) -> ( ( U u. { <. dom U , 2o >. } )  -. ( Z |` suc dom U ) . } ) ) )
118 12 117 mpan 
 |-  ( ( ( U u. { <. dom U , 2o >. } ) e. No /\ ( Z |` suc dom U ) e. No ) -> ( ( U u. { <. dom U , 2o >. } )  -. ( Z |` suc dom U ) . } ) ) )
119 108 113 118 syl2anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U u. { <. dom U , 2o >. } )  -. ( Z |` suc dom U ) . } ) ) )
120 116 119 mpd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )
121 df-suc 
 |-  suc dom U = ( dom U u. { dom U } )
122 121 reseq2i 
 |-  ( Z |` suc dom U ) = ( Z |` ( dom U u. { dom U } ) )
123 resundi 
 |-  ( Z |` ( dom U u. { dom U } ) ) = ( ( Z |` dom U ) u. ( Z |` { dom U } ) )
124 122 123 eqtri 
 |-  ( Z |` suc dom U ) = ( ( Z |` dom U ) u. ( Z |` { dom U } ) )
125 dmres 
 |-  dom ( Z |` dom U ) = ( dom U i^i dom Z )
126 simpr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U )
127 necom 
 |-  ( ( U ` x ) =/= ( Z ` x ) <-> ( Z ` x ) =/= ( U ` x ) )
128 127 rabbii 
 |-  { x e. On | ( U ` x ) =/= ( Z ` x ) } = { x e. On | ( Z ` x ) =/= ( U ` x ) }
129 128 inteqi 
 |-  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = |^| { x e. On | ( Z ` x ) =/= ( U ` x ) }
130 9 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Z e. No )
131 8 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  U e. No )
132 21 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  U =/= Z )
133 132 necomd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Z =/= U )
134 nosepssdm 
 |-  ( ( Z e. No /\ U e. No /\ Z =/= U ) -> |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } C_ dom Z )
135 130 131 133 134 syl3anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } C_ dom Z )
136 129 135 eqsstrid 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom Z )
137 126 136 eqsstrrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  dom U C_ dom Z )
138 df-ss 
 |-  ( dom U C_ dom Z <-> ( dom U i^i dom Z ) = dom U )
139 137 138 sylib 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( dom U i^i dom Z ) = dom U )
140 125 139 syl5eq 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  dom ( Z |` dom U ) = dom U )
141 140 eleq2d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( q e. dom ( Z |` dom U ) <-> q e. dom U ) )
142 simpr 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  q e. dom U )
143 142 fvresd 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` dom U ) ` q ) = ( Z ` q ) )
144 131 26 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  dom U e. On )
145 onelon 
 |-  ( ( dom U e. On /\ q e. dom U ) -> q e. On )
146 144 145 sylan 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  q e. On )
147 126 eleq2d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } <-> q e. dom U ) )
148 147 biimpar 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } )
149 146 148 40 sylc 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( U ` q ) =/= ( Z ` q ) )
150 nesym 
 |-  ( ( U ` q ) =/= ( Z ` q ) <-> -. ( Z ` q ) = ( U ` q ) )
151 150 con2bii 
 |-  ( ( Z ` q ) = ( U ` q ) <-> -. ( U ` q ) =/= ( Z ` q ) )
152 149 151 sylibr 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z ` q ) = ( U ` q ) )
153 143 152 eqtrd 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` dom U ) ` q ) = ( U ` q ) )
154 153 ex 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( q e. dom U -> ( ( Z |` dom U ) ` q ) = ( U ` q ) ) )
155 141 154 sylbid 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( q e. dom ( Z |` dom U ) -> ( ( Z |` dom U ) ` q ) = ( U ` q ) ) )
156 155 ralrimiv 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  A. q e. dom ( Z |` dom U ) ( ( Z |` dom U ) ` q ) = ( U ` q ) )
157 nofun 
 |-  ( Z e. No -> Fun Z )
158 funres 
 |-  ( Fun Z -> Fun ( Z |` dom U ) )
159 130 157 158 3syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Fun ( Z |` dom U ) )
160 131 94 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Fun U )
161 eqfunfv 
 |-  ( ( 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 ) ) ) )
162 159 160 161 syl2anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` dom U ) = U <-> ( dom ( Z |` dom U ) = dom U /\ A. q e. dom ( Z |` dom U ) ( ( Z |` dom U ) ` q ) = ( U ` q ) ) ) )
163 140 156 162 mpbir2and 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` dom U ) = U )
164 130 157 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Fun Z )
165 funfn 
 |-  ( Fun Z <-> Z Fn dom Z )
166 164 165 sylib 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Z Fn dom Z )
167 1oex 
 |-  1o e. _V
168 167 prid1 
 |-  1o e. { 1o , 2o }
169 168 nosgnn0i 
 |-  (/) =/= 1o
170 131 79 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Ord dom U )
171 ndmfv 
 |-  ( -. dom U e. dom U -> ( U ` dom U ) = (/) )
172 170 80 171 3syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` dom U ) = (/) )
173 172 neeq1d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U ` dom U ) =/= 1o <-> (/) =/= 1o ) )
174 169 173 mpbiri 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` dom U ) =/= 1o )
175 174 neneqd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( U ` dom U ) = 1o )
176 175 intnanrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) )
177 175 intnanrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) )
178 simplr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  U
179 131 130 55 syl2anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U  ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) ) )
180 178 179 mpbid 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) )
181 fveq2 
 |-  ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U -> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( U ` dom U ) )
182 181 adantl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( U ` dom U ) )
183 fveq2 
 |-  ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U -> ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( Z ` dom U ) )
184 183 adantl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( Z ` dom U ) )
185 180 182 184 3brtr3d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` dom U ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` dom U ) )
186 fvex 
 |-  ( U ` dom U ) e. _V
187 fvex 
 |-  ( Z ` dom U ) e. _V
188 186 187 brtp 
 |-  ( ( 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 ) ) )
189 3orrot 
 |-  ( ( ( ( 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 ) = (/) ) ) )
190 3orrot 
 |-  ( ( ( ( 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 ) ) )
191 188 189 190 3bitri 
 |-  ( ( 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 ) ) )
192 185 191 sylib 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) \/ ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) ) )
193 176 177 192 ecase23d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) )
194 193 simprd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z ` dom U ) = 2o )
195 ndmfv 
 |-  ( -. dom U e. dom Z -> ( Z ` dom U ) = (/) )
196 105 nosgnn0i 
 |-  (/) =/= 2o
197 neeq1 
 |-  ( ( Z ` dom U ) = (/) -> ( ( Z ` dom U ) =/= 2o <-> (/) =/= 2o ) )
198 196 197 mpbiri 
 |-  ( ( Z ` dom U ) = (/) -> ( Z ` dom U ) =/= 2o )
199 198 neneqd 
 |-  ( ( Z ` dom U ) = (/) -> -. ( Z ` dom U ) = 2o )
200 195 199 syl 
 |-  ( -. dom U e. dom Z -> -. ( Z ` dom U ) = 2o )
201 200 con4i 
 |-  ( ( Z ` dom U ) = 2o -> dom U e. dom Z )
202 194 201 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  dom U e. dom Z )
203 fnressn 
 |-  ( ( Z Fn dom Z /\ dom U e. dom Z ) -> ( Z |` { dom U } ) = { <. dom U , ( Z ` dom U ) >. } )
204 166 202 203 syl2anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` { dom U } ) = { <. dom U , ( Z ` dom U ) >. } )
205 194 opeq2d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  <. dom U , ( Z ` dom U ) >. = <. dom U , 2o >. )
206 205 sneqd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  { <. dom U , ( Z ` dom U ) >. } = { <. dom U , 2o >. } )
207 204 206 eqtrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` { dom U } ) = { <. dom U , 2o >. } )
208 163 207 uneq12d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` dom U ) u. ( Z |` { dom U } ) ) = ( U u. { <. dom U , 2o >. } ) )
209 124 208 syl5eq 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` suc dom U ) = ( U u. { <. dom U , 2o >. } ) )
210 sonr 
 |-  ( ( . } ) e. No ) -> -. ( U u. { <. dom U , 2o >. } ) . } ) )
211 12 210 mpan 
 |-  ( ( U u. { <. dom U , 2o >. } ) e. No -> -. ( U u. { <. dom U , 2o >. } ) . } ) )
212 131 106 211 3syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( U u. { <. dom U , 2o >. } ) . } ) )
213 209 212 eqnbrtrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )
214 120 213 jaodan 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )
215 214 ex 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  ( ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. dom U \/ |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U ) -> -. ( Z |` suc dom U ) . } ) ) )
216 29 215 sylbid 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U -> -. ( Z |` suc dom U ) . } ) ) )
217 23 216 mpd 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )
218 5 217 mpdan 
 |-  ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )