Metamath Proof Explorer


Theorem noinfbnd2lem1

Description: Bounding law from below when a set of surreals has a minimum. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Assertion noinfbnd2lem1
|- ( ( ( U e. B /\ A. y e. B -. y  -. ( U u. { <. dom U , 1o >. } ) 

Proof

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