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 ) . } ) )