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 ltsval2 
 |-  ( ( 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 ltsval 
 |-  ( ( ( 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 eqtrid 
 |-  ( ( ( ( ( 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 onsucb 
 |-  ( 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 ltsres 
 |-  ( ( ( 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 ltsso 
 |-
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 bilani 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } = dom U )
110 35 adantr 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  Z e. No )
111 7 adantr 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  U e. No )
112 simp23 
 |-  ( ( ( U e. B /\ A. y e. B -. y  Z e. No )
113 sonr 
 |-  ( (  -. Z
114 95 112 113 sylancr 
 |-  ( ( ( U e. B /\ A. y e. B -. y  -. Z
115 breq2 
 |-  ( U = Z -> ( Z  Z
116 115 notbid 
 |-  ( U = Z -> ( -. Z  -. Z
117 114 116 syl5ibrcom 
 |-  ( ( ( U e. B /\ A. y e. B -. y  ( U = Z -> -. Z
118 117 necon2ad 
 |-  ( ( ( U e. B /\ A. y e. B -. y  ( Z  U =/= Z ) )
119 118 imp 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  U =/= Z )
120 119 necomd 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  Z =/= U )
121 120 adantr 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  Z =/= U )
122 nosepssdm 
 |-  ( ( Z e. No /\ U e. No /\ Z =/= U ) -> |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } C_ dom Z )
123 110 111 121 122 syl3anc 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } C_ dom Z )
124 109 123 eqsstrrd 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  dom U C_ dom Z )
125 dfss2 
 |-  ( dom U C_ dom Z <-> ( dom U i^i dom Z ) = dom U )
126 124 125 sylib 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( dom U i^i dom Z ) = dom U )
127 107 126 eqtrid 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  dom ( Z |` dom U ) = dom U )
128 127 eleq2d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( q e. dom ( Z |` dom U ) <-> q e. dom U ) )
129 simpr 
 |-  ( ( ( ( ( ( U e. B /\ A. y e. B -. y  q e. dom U )
130 129 fvresd 
 |-  ( ( ( ( ( ( U e. B /\ A. y e. B -. y  ( ( Z |` dom U ) ` q ) = ( Z ` q ) )
131 111 8 syl 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  dom U e. On )
132 onelon 
 |-  ( ( dom U e. On /\ q e. dom U ) -> q e. On )
133 131 132 sylan 
 |-  ( ( ( ( ( ( U e. B /\ A. y e. B -. y  q e. On )
134 simpr 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } = dom U )
135 134 eleq2d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } <-> q e. dom U ) )
136 135 biimpar 
 |-  ( ( ( ( ( ( U e. B /\ A. y e. B -. y  q e. |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } )
137 133 136 25 sylc 
 |-  ( ( ( ( ( ( U e. B /\ A. y e. B -. y  -. ( U ` q ) =/= ( Z ` q ) )
138 nesym 
 |-  ( ( U ` q ) =/= ( Z ` q ) <-> -. ( Z ` q ) = ( U ` q ) )
139 138 con2bii 
 |-  ( ( Z ` q ) = ( U ` q ) <-> -. ( U ` q ) =/= ( Z ` q ) )
140 137 139 sylibr 
 |-  ( ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z ` q ) = ( U ` q ) )
141 130 140 eqtrd 
 |-  ( ( ( ( ( ( U e. B /\ A. y e. B -. y  ( ( Z |` dom U ) ` q ) = ( U ` q ) )
142 141 ex 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( q e. dom U -> ( ( Z |` dom U ) ` q ) = ( U ` q ) ) )
143 128 142 sylbid 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( q e. dom ( Z |` dom U ) -> ( ( Z |` dom U ) ` q ) = ( U ` q ) ) )
144 143 ralrimiv 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  A. q e. dom ( Z |` dom U ) ( ( Z |` dom U ) ` q ) = ( U ` q ) )
145 nofun 
 |-  ( Z e. No -> Fun Z )
146 110 145 syl 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  Fun Z )
147 146 funresd 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  Fun ( Z |` dom U ) )
148 64 adantr 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  Fun U )
149 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 ) ) ) )
150 147 148 149 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 ) ) ) )
151 127 144 150 mpbir2and 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z |` dom U ) = U )
152 35 145 syl 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  Fun Z )
153 152 funfnd 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  Z Fn dom Z )
154 ndmfv 
 |-  ( -. dom U e. dom U -> ( U ` dom U ) = (/) )
155 2on0 
 |-  2o =/= (/)
156 155 necomi 
 |-  (/) =/= 2o
157 neeq1 
 |-  ( ( U ` dom U ) = (/) -> ( ( U ` dom U ) =/= 2o <-> (/) =/= 2o ) )
158 156 157 mpbiri 
 |-  ( ( U ` dom U ) = (/) -> ( U ` dom U ) =/= 2o )
159 158 neneqd 
 |-  ( ( U ` dom U ) = (/) -> -. ( U ` dom U ) = 2o )
160 154 159 syl 
 |-  ( -. dom U e. dom U -> -. ( U ` dom U ) = 2o )
161 111 70 73 160 4syl 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  -. ( U ` dom U ) = 2o )
162 161 intnand 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  -. ( ( Z ` dom U ) = (/) /\ ( U ` dom U ) = 2o ) )
163 simpr 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  Z
164 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 ) } ) ) )
165 163 164 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 ) } ) )
166 165 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 ) } ) )
167 109 fveq2d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z ` |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } ) = ( Z ` dom U ) )
168 109 fveq2d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( U ` |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } ) = ( U ` dom U ) )
169 166 167 168 3brtr3d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z ` dom U ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( U ` dom U ) )
170 fvex 
 |-  ( Z ` dom U ) e. _V
171 fvex 
 |-  ( U ` dom U ) e. _V
172 170 171 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 ) ) )
173 169 172 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 ) ) )
174 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 ) ) ) )
175 162 173 174 sylc 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( ( ( Z ` dom U ) = 1o /\ ( U ` dom U ) = (/) ) \/ ( ( Z ` dom U ) = 1o /\ ( U ` dom U ) = 2o ) ) )
176 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 ) ) )
177 175 176 sylibr 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( ( Z ` dom U ) = 1o /\ ( ( U ` dom U ) = (/) \/ ( U ` dom U ) = 2o ) ) )
178 177 simpld 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z ` dom U ) = 1o )
179 ndmfv 
 |-  ( -. dom U e. dom Z -> ( Z ` dom U ) = (/) )
180 1n0 
 |-  1o =/= (/)
181 180 necomi 
 |-  (/) =/= 1o
182 neeq1 
 |-  ( ( Z ` dom U ) = (/) -> ( ( Z ` dom U ) =/= 1o <-> (/) =/= 1o ) )
183 181 182 mpbiri 
 |-  ( ( Z ` dom U ) = (/) -> ( Z ` dom U ) =/= 1o )
184 183 neneqd 
 |-  ( ( Z ` dom U ) = (/) -> -. ( Z ` dom U ) = 1o )
185 179 184 syl 
 |-  ( -. dom U e. dom Z -> -. ( Z ` dom U ) = 1o )
186 185 con4i 
 |-  ( ( Z ` dom U ) = 1o -> dom U e. dom Z )
187 178 186 syl 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  dom U e. dom Z )
188 fnressn 
 |-  ( ( Z Fn dom Z /\ dom U e. dom Z ) -> ( Z |` { dom U } ) = { <. dom U , ( Z ` dom U ) >. } )
189 153 187 188 syl2an2r 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z |` { dom U } ) = { <. dom U , ( Z ` dom U ) >. } )
190 178 opeq2d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  <. dom U , ( Z ` dom U ) >. = <. dom U , 1o >. )
191 190 sneqd 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  { <. dom U , ( Z ` dom U ) >. } = { <. dom U , 1o >. } )
192 189 191 eqtrd 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z |` { dom U } ) = { <. dom U , 1o >. } )
193 151 192 uneq12d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( ( Z |` dom U ) u. ( Z |` { dom U } ) ) = ( U u. { <. dom U , 1o >. } ) )
194 106 193 eqtrid 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z |` suc dom U ) = ( U u. { <. dom U , 1o >. } ) )
195 194 breq2d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( ( U u. { <. dom U , 1o >. } )  ( U u. { <. dom U , 1o >. } ) . } ) ) )
196 102 195 mtbird 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  -. ( U u. { <. dom U , 1o >. } )
197 nosepssdm 
 |-  ( ( U e. No /\ Z e. No /\ U =/= Z ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U )
198 7 35 119 197 syl3anc 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U )
199 nosepon 
 |-  ( ( U e. No /\ Z e. No /\ U =/= Z ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On )
200 7 35 119 199 syl3anc 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On )
201 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 ) ) )
202 200 9 201 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 ) ) )
203 198 202 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 ) )
204 99 196 203 mpjaodan 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  -. ( U u. { <. dom U , 1o >. } )
205 4 204 mpdan 
 |-  ( ( ( U e. B /\ A. y e. B -. y  -. ( U u. { <. dom U , 1o >. } )