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