Step |
Hyp |
Ref |
Expression |
1 |
|
mreexd.1 |
|- ( ph -> X e. V ) |
2 |
|
mreexd.2 |
|- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) ) |
3 |
|
mreexd.3 |
|- ( ph -> S C_ X ) |
4 |
|
mreexd.4 |
|- ( ph -> Y e. X ) |
5 |
|
mreexd.5 |
|- ( ph -> Z e. ( N ` ( S u. { Y } ) ) ) |
6 |
|
mreexd.6 |
|- ( ph -> -. Z e. ( N ` S ) ) |
7 |
1 3
|
sselpwd |
|- ( ph -> S e. ~P X ) |
8 |
4
|
adantr |
|- ( ( ph /\ s = S ) -> Y e. X ) |
9 |
5
|
ad2antrr |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> Z e. ( N ` ( S u. { Y } ) ) ) |
10 |
|
simplr |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> s = S ) |
11 |
|
simpr |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> y = Y ) |
12 |
11
|
sneqd |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> { y } = { Y } ) |
13 |
10 12
|
uneq12d |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( s u. { y } ) = ( S u. { Y } ) ) |
14 |
13
|
fveq2d |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( N ` ( s u. { y } ) ) = ( N ` ( S u. { Y } ) ) ) |
15 |
9 14
|
eleqtrrd |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> Z e. ( N ` ( s u. { y } ) ) ) |
16 |
6
|
ad2antrr |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> -. Z e. ( N ` S ) ) |
17 |
10
|
fveq2d |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( N ` s ) = ( N ` S ) ) |
18 |
16 17
|
neleqtrrd |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> -. Z e. ( N ` s ) ) |
19 |
15 18
|
eldifd |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> Z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) |
20 |
|
simplr |
|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> y = Y ) |
21 |
|
simpllr |
|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> s = S ) |
22 |
|
simpr |
|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> z = Z ) |
23 |
22
|
sneqd |
|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> { z } = { Z } ) |
24 |
21 23
|
uneq12d |
|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> ( s u. { z } ) = ( S u. { Z } ) ) |
25 |
24
|
fveq2d |
|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> ( N ` ( s u. { z } ) ) = ( N ` ( S u. { Z } ) ) ) |
26 |
20 25
|
eleq12d |
|- ( ( ( ( ph /\ s = S ) /\ y = Y ) /\ z = Z ) -> ( y e. ( N ` ( s u. { z } ) ) <-> Y e. ( N ` ( S u. { Z } ) ) ) ) |
27 |
19 26
|
rspcdv |
|- ( ( ( ph /\ s = S ) /\ y = Y ) -> ( A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) -> Y e. ( N ` ( S u. { Z } ) ) ) ) |
28 |
8 27
|
rspcimdv |
|- ( ( ph /\ s = S ) -> ( A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) -> Y e. ( N ` ( S u. { Z } ) ) ) ) |
29 |
7 28
|
rspcimdv |
|- ( ph -> ( A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) -> Y e. ( N ` ( S u. { Z } ) ) ) ) |
30 |
2 29
|
mpd |
|- ( ph -> Y e. ( N ` ( S u. { Z } ) ) ) |