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 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 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 dfss2 
 |-  ( 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 eqtrid 
 |-  ( ( ( ( ( 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 ndmfv 
 |-  ( -. dom U e. dom U -> ( U ` dom U ) = (/) )
156 2on0 
 |-  2o =/= (/)
157 156 necomi 
 |-  (/) =/= 2o
158 neeq1 
 |-  ( ( U ` dom U ) = (/) -> ( ( U ` dom U ) =/= 2o <-> (/) =/= 2o ) )
159 157 158 mpbiri 
 |-  ( ( U ` dom U ) = (/) -> ( U ` dom U ) =/= 2o )
160 159 neneqd 
 |-  ( ( U ` dom U ) = (/) -> -. ( U ` dom U ) = 2o )
161 155 160 syl 
 |-  ( -. dom U e. dom U -> -. ( U ` dom U ) = 2o )
162 112 70 73 161 4syl 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  -. ( U ` dom U ) = 2o )
163 162 intnand 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  -. ( ( Z ` dom U ) = (/) /\ ( U ` dom U ) = 2o ) )
164 simpr 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  Z
165 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 ) } ) ) )
166 164 165 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 ) } ) )
167 166 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 ) } ) )
168 110 fveq2d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z ` |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } ) = ( Z ` dom U ) )
169 110 fveq2d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( U ` |^| { x e. On | ( Z ` x ) =/= ( U ` x ) } ) = ( U ` dom U ) )
170 167 168 169 3brtr3d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z ` dom U ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( U ` dom U ) )
171 fvex 
 |-  ( Z ` dom U ) e. _V
172 fvex 
 |-  ( U ` dom U ) e. _V
173 171 172 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 ) ) )
174 170 173 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 ) ) )
175 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 ) ) ) )
176 163 174 175 sylc 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( ( ( Z ` dom U ) = 1o /\ ( U ` dom U ) = (/) ) \/ ( ( Z ` dom U ) = 1o /\ ( U ` dom U ) = 2o ) ) )
177 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 ) ) )
178 176 177 sylibr 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( ( Z ` dom U ) = 1o /\ ( ( U ` dom U ) = (/) \/ ( U ` dom U ) = 2o ) ) )
179 178 simpld 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z ` dom U ) = 1o )
180 ndmfv 
 |-  ( -. dom U e. dom Z -> ( Z ` dom U ) = (/) )
181 1n0 
 |-  1o =/= (/)
182 181 necomi 
 |-  (/) =/= 1o
183 neeq1 
 |-  ( ( Z ` dom U ) = (/) -> ( ( Z ` dom U ) =/= 1o <-> (/) =/= 1o ) )
184 182 183 mpbiri 
 |-  ( ( Z ` dom U ) = (/) -> ( Z ` dom U ) =/= 1o )
185 184 neneqd 
 |-  ( ( Z ` dom U ) = (/) -> -. ( Z ` dom U ) = 1o )
186 180 185 syl 
 |-  ( -. dom U e. dom Z -> -. ( Z ` dom U ) = 1o )
187 186 con4i 
 |-  ( ( Z ` dom U ) = 1o -> dom U e. dom Z )
188 179 187 syl 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  dom U e. dom Z )
189 fnressn 
 |-  ( ( Z Fn dom Z /\ dom U e. dom Z ) -> ( Z |` { dom U } ) = { <. dom U , ( Z ` dom U ) >. } )
190 154 188 189 syl2an2r 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z |` { dom U } ) = { <. dom U , ( Z ` dom U ) >. } )
191 179 opeq2d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  <. dom U , ( Z ` dom U ) >. = <. dom U , 1o >. )
192 191 sneqd 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  { <. dom U , ( Z ` dom U ) >. } = { <. dom U , 1o >. } )
193 190 192 eqtrd 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z |` { dom U } ) = { <. dom U , 1o >. } )
194 152 193 uneq12d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( ( Z |` dom U ) u. ( Z |` { dom U } ) ) = ( U u. { <. dom U , 1o >. } ) )
195 106 194 eqtrid 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( Z |` suc dom U ) = ( U u. { <. dom U , 1o >. } ) )
196 195 breq2d 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  ( ( U u. { <. dom U , 1o >. } )  ( U u. { <. dom U , 1o >. } ) . } ) ) )
197 102 196 mtbird 
 |-  ( ( ( ( ( U e. B /\ A. y e. B -. y  -. ( U u. { <. dom U , 1o >. } )
198 nosepssdm 
 |-  ( ( U e. No /\ Z e. No /\ U =/= Z ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U )
199 7 35 120 198 syl3anc 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } C_ dom U )
200 nosepon 
 |-  ( ( U e. No /\ Z e. No /\ U =/= Z ) -> |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On )
201 7 35 120 200 syl3anc 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  |^| { x e. On | ( U ` x ) =/= ( Z ` x ) } e. On )
202 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 ) ) )
203 201 9 202 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 ) ) )
204 199 203 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 ) )
205 99 197 204 mpjaodan 
 |-  ( ( ( ( U e. B /\ A. y e. B -. y  -. ( U u. { <. dom U , 1o >. } )
206 4 205 mpdan 
 |-  ( ( ( U e. B /\ A. y e. B -. y  -. ( U u. { <. dom U , 1o >. } )