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 eqtrid 
 |-  ( ( ( ( ( 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 eqtrid 
 |-  ( ( ( ( ( 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 funrel 
 |-  ( Fun U -> Rel U )
96 resdm 
 |-  ( Rel U -> ( U |` dom U ) = U )
97 30 94 95 96 4syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U |` dom U ) = U )
98 93 97 eqtrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U u. { <. dom U , 2o >. } ) |` dom U ) = U )
99 sssucid 
 |-  dom U C_ suc dom U
100 resabs1 
 |-  ( dom U C_ suc dom U -> ( ( Z |` suc dom U ) |` dom U ) = ( Z |` dom U ) )
101 99 100 mp1i 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` suc dom U ) |` dom U ) = ( Z |` dom U ) )
102 72 98 101 3brtr4d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U u. { <. dom U , 2o >. } ) |` dom U )
103 74 elexi 
 |-  2o e. _V
104 103 prid2 
 |-  2o e. { 1o , 2o }
105 104 noextend 
 |-  ( U e. No -> ( U u. { <. dom U , 2o >. } ) e. No )
106 8 105 syl 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  ( U u. { <. dom U , 2o >. } ) e. No )
107 106 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U u. { <. dom U , 2o >. } ) e. No )
108 onsucb 
 |-  ( dom U e. On <-> suc dom U e. On )
109 27 108 sylib 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  suc dom U e. On )
110 noreson 
 |-  ( ( Z e. No /\ suc dom U e. On ) -> ( Z |` suc dom U ) e. No )
111 9 109 110 syl2anc 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` suc dom U ) e. No )
112 111 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` suc dom U ) e. No )
113 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 >. } )
114 107 112 46 113 syl3anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( ( U u. { <. dom U , 2o >. } ) |` dom U )  ( U u. { <. dom U , 2o >. } )
115 102 114 mpd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U u. { <. dom U , 2o >. } )
116 soasym 
 |-  ( ( . } ) e. No /\ ( Z |` suc dom U ) e. No ) ) -> ( ( U u. { <. dom U , 2o >. } )  -. ( Z |` suc dom U ) . } ) ) )
117 12 116 mpan 
 |-  ( ( ( U u. { <. dom U , 2o >. } ) e. No /\ ( Z |` suc dom U ) e. No ) -> ( ( U u. { <. dom U , 2o >. } )  -. ( Z |` suc dom U ) . } ) ) )
118 107 112 117 syl2anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U u. { <. dom U , 2o >. } )  -. ( Z |` suc dom U ) . } ) ) )
119 115 118 mpd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )
120 df-suc 
 |-  suc dom U = ( dom U u. { dom U } )
121 120 reseq2i 
 |-  ( Z |` suc dom U ) = ( Z |` ( dom U u. { dom U } ) )
122 resundi 
 |-  ( Z |` ( dom U u. { dom U } ) ) = ( ( Z |` dom U ) u. ( Z |` { dom U } ) )
123 121 122 eqtri 
 |-  ( Z |` suc dom U ) = ( ( Z |` dom U ) u. ( Z |` { dom U } ) )
124 dmres 
 |-  dom ( Z |` dom U ) = ( dom U i^i dom Z )
125 simpr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U )
126 necom 
 |-  ( ( U ` x ) =/= ( Z ` x ) <-> ( Z ` x ) =/= ( U ` x ) )
127 126 rabbii 
 |-  { x e. On | ( U ` x ) =/= ( Z ` x ) } = { x e. On | ( Z ` x ) =/= ( U ` x ) }
128 127 inteqi 
 |-  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = |^| { x e. On | ( Z ` x ) =/= ( U ` x ) }
129 9 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Z e. No )
130 8 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  U e. No )
131 21 adantr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  U =/= Z )
132 131 necomd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Z =/= U )
133 nosepssdm 
 |-  ( ( Z e. No /\ U e. No /\ Z =/= U ) -> |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } C_ dom Z )
134 129 130 132 133 syl3anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } C_ dom Z )
135 128 134 eqsstrid 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom Z )
136 125 135 eqsstrrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  dom U C_ dom Z )
137 dfss2 
 |-  ( dom U C_ dom Z <-> ( dom U i^i dom Z ) = dom U )
138 136 137 sylib 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( dom U i^i dom Z ) = dom U )
139 124 138 eqtrid 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  dom ( Z |` dom U ) = dom U )
140 139 eleq2d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( q e. dom ( Z |` dom U ) <-> q e. dom U ) )
141 simpr 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  q e. dom U )
142 141 fvresd 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` dom U ) ` q ) = ( Z ` q ) )
143 130 26 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  dom U e. On )
144 onelon 
 |-  ( ( dom U e. On /\ q e. dom U ) -> q e. On )
145 143 144 sylan 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  q e. On )
146 125 eleq2d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } <-> q e. dom U ) )
147 146 biimpar 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } )
148 145 147 40 sylc 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( U ` q ) =/= ( Z ` q ) )
149 nesym 
 |-  ( ( U ` q ) =/= ( Z ` q ) <-> -. ( Z ` q ) = ( U ` q ) )
150 149 con2bii 
 |-  ( ( Z ` q ) = ( U ` q ) <-> -. ( U ` q ) =/= ( Z ` q ) )
151 148 150 sylibr 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z ` q ) = ( U ` q ) )
152 142 151 eqtrd 
 |-  ( ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` dom U ) ` q ) = ( U ` q ) )
153 152 ex 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( q e. dom U -> ( ( Z |` dom U ) ` q ) = ( U ` q ) ) )
154 140 153 sylbid 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( q e. dom ( Z |` dom U ) -> ( ( Z |` dom U ) ` q ) = ( U ` q ) ) )
155 154 ralrimiv 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  A. q e. dom ( Z |` dom U ) ( ( Z |` dom U ) ` q ) = ( U ` q ) )
156 nofun 
 |-  ( Z e. No -> Fun Z )
157 funres 
 |-  ( Fun Z -> Fun ( Z |` dom U ) )
158 129 156 157 3syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Fun ( Z |` dom U ) )
159 130 94 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Fun U )
160 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 ) ) ) )
161 158 159 160 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 ) ) ) )
162 139 155 161 mpbir2and 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` dom U ) = U )
163 129 156 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Fun Z )
164 funfn 
 |-  ( Fun Z <-> Z Fn dom Z )
165 163 164 sylib 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  Z Fn dom Z )
166 1oex 
 |-  1o e. _V
167 166 prid1 
 |-  1o e. { 1o , 2o }
168 167 nosgnn0i 
 |-  (/) =/= 1o
169 ndmfv 
 |-  ( -. dom U e. dom U -> ( U ` dom U ) = (/) )
170 130 79 80 169 4syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` dom U ) = (/) )
171 170 neeq1d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U ` dom U ) =/= 1o <-> (/) =/= 1o ) )
172 168 171 mpbiri 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` dom U ) =/= 1o )
173 172 neneqd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( U ` dom U ) = 1o )
174 173 intnanrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = (/) ) )
175 173 intnanrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( ( U ` dom U ) = 1o /\ ( Z ` dom U ) = 2o ) )
176 simplr 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  U
177 130 129 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 ) } ) ) )
178 176 177 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 ) } ) )
179 fveq2 
 |-  ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U -> ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( U ` dom U ) )
180 179 adantl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( U ` dom U ) )
181 fveq2 
 |-  ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U -> ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( Z ` dom U ) )
182 181 adantl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z ` |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } ) = ( Z ` dom U ) )
183 178 180 182 3brtr3d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( U ` dom U ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( Z ` dom U ) )
184 fvex 
 |-  ( U ` dom U ) e. _V
185 fvex 
 |-  ( Z ` dom U ) e. _V
186 184 185 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 ) ) )
187 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 ) = (/) ) ) )
188 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 ) ) )
189 186 187 188 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 ) ) )
190 183 189 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 ) ) )
191 174 175 190 ecase23d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( U ` dom U ) = (/) /\ ( Z ` dom U ) = 2o ) )
192 191 simprd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z ` dom U ) = 2o )
193 ndmfv 
 |-  ( -. dom U e. dom Z -> ( Z ` dom U ) = (/) )
194 104 nosgnn0i 
 |-  (/) =/= 2o
195 neeq1 
 |-  ( ( Z ` dom U ) = (/) -> ( ( Z ` dom U ) =/= 2o <-> (/) =/= 2o ) )
196 194 195 mpbiri 
 |-  ( ( Z ` dom U ) = (/) -> ( Z ` dom U ) =/= 2o )
197 196 neneqd 
 |-  ( ( Z ` dom U ) = (/) -> -. ( Z ` dom U ) = 2o )
198 193 197 syl 
 |-  ( -. dom U e. dom Z -> -. ( Z ` dom U ) = 2o )
199 198 con4i 
 |-  ( ( Z ` dom U ) = 2o -> dom U e. dom Z )
200 192 199 syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  dom U e. dom Z )
201 fnressn 
 |-  ( ( Z Fn dom Z /\ dom U e. dom Z ) -> ( Z |` { dom U } ) = { <. dom U , ( Z ` dom U ) >. } )
202 165 200 201 syl2anc 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` { dom U } ) = { <. dom U , ( Z ` dom U ) >. } )
203 192 opeq2d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  <. dom U , ( Z ` dom U ) >. = <. dom U , 2o >. )
204 203 sneqd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  { <. dom U , ( Z ` dom U ) >. } = { <. dom U , 2o >. } )
205 202 204 eqtrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` { dom U } ) = { <. dom U , 2o >. } )
206 162 205 uneq12d 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( ( Z |` dom U ) u. ( Z |` { dom U } ) ) = ( U u. { <. dom U , 2o >. } ) )
207 123 206 eqtrid 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  ( Z |` suc dom U ) = ( U u. { <. dom U , 2o >. } ) )
208 sonr 
 |-  ( ( . } ) e. No ) -> -. ( U u. { <. dom U , 2o >. } ) . } ) )
209 12 208 mpan 
 |-  ( ( U u. { <. dom U , 2o >. } ) e. No -> -. ( U u. { <. dom U , 2o >. } ) . } ) )
210 130 105 209 3syl 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( U u. { <. dom U , 2o >. } ) . } ) )
211 207 210 eqnbrtrd 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )
212 119 211 jaodan 
 |-  ( ( ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )
213 212 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 ) . } ) ) )
214 29 213 sylbid 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  ( |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U -> -. ( Z |` suc dom U ) . } ) ) )
215 23 214 mpd 
 |-  ( ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )
216 5 215 mpdan 
 |-  ( ( ( U e. A /\ A. y e. A -. U  -. ( Z |` suc dom U ) . } ) )