Step |
Hyp |
Ref |
Expression |
1 |
|
mreexexlem2d.1 |
|- ( ph -> A e. ( Moore ` X ) ) |
2 |
|
mreexexlem2d.2 |
|- N = ( mrCls ` A ) |
3 |
|
mreexexlem2d.3 |
|- I = ( mrInd ` A ) |
4 |
|
mreexexlem2d.4 |
|- ( 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 } ) ) ) |
5 |
|
mreexexlem2d.5 |
|- ( ph -> F C_ ( X \ H ) ) |
6 |
|
mreexexlem2d.6 |
|- ( ph -> G C_ ( X \ H ) ) |
7 |
|
mreexexlem2d.7 |
|- ( ph -> F C_ ( N ` ( G u. H ) ) ) |
8 |
|
mreexexlem2d.8 |
|- ( ph -> ( F u. H ) e. I ) |
9 |
|
mreexexlem2d.9 |
|- ( ph -> Y e. F ) |
10 |
7
|
adantr |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> F C_ ( N ` ( G u. H ) ) ) |
11 |
1
|
adantr |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> A e. ( Moore ` X ) ) |
12 |
|
simpr |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) |
13 |
|
ssun2 |
|- H C_ ( ( F \ { Y } ) u. H ) |
14 |
|
difundir |
|- ( ( F u. H ) \ { Y } ) = ( ( F \ { Y } ) u. ( H \ { Y } ) ) |
15 |
|
incom |
|- ( F i^i H ) = ( H i^i F ) |
16 |
|
ssdifin0 |
|- ( F C_ ( X \ H ) -> ( F i^i H ) = (/) ) |
17 |
5 16
|
syl |
|- ( ph -> ( F i^i H ) = (/) ) |
18 |
15 17
|
eqtr3id |
|- ( ph -> ( H i^i F ) = (/) ) |
19 |
|
minel |
|- ( ( Y e. F /\ ( H i^i F ) = (/) ) -> -. Y e. H ) |
20 |
9 18 19
|
syl2anc |
|- ( ph -> -. Y e. H ) |
21 |
|
difsnb |
|- ( -. Y e. H <-> ( H \ { Y } ) = H ) |
22 |
20 21
|
sylib |
|- ( ph -> ( H \ { Y } ) = H ) |
23 |
22
|
uneq2d |
|- ( ph -> ( ( F \ { Y } ) u. ( H \ { Y } ) ) = ( ( F \ { Y } ) u. H ) ) |
24 |
14 23
|
eqtrid |
|- ( ph -> ( ( F u. H ) \ { Y } ) = ( ( F \ { Y } ) u. H ) ) |
25 |
13 24
|
sseqtrrid |
|- ( ph -> H C_ ( ( F u. H ) \ { Y } ) ) |
26 |
3 1 8
|
mrissd |
|- ( ph -> ( F u. H ) C_ X ) |
27 |
26
|
ssdifssd |
|- ( ph -> ( ( F u. H ) \ { Y } ) C_ X ) |
28 |
1 2 27
|
mrcssidd |
|- ( ph -> ( ( F u. H ) \ { Y } ) C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) |
29 |
25 28
|
sstrd |
|- ( ph -> H C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) |
30 |
29
|
adantr |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> H C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) |
31 |
12 30
|
unssd |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> ( G u. H ) C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) |
32 |
11 2
|
mrcssvd |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> ( N ` ( ( F u. H ) \ { Y } ) ) C_ X ) |
33 |
11 2 31 32
|
mrcssd |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> ( N ` ( G u. H ) ) C_ ( N ` ( N ` ( ( F u. H ) \ { Y } ) ) ) ) |
34 |
27
|
adantr |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> ( ( F u. H ) \ { Y } ) C_ X ) |
35 |
11 2 34
|
mrcidmd |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> ( N ` ( N ` ( ( F u. H ) \ { Y } ) ) ) = ( N ` ( ( F u. H ) \ { Y } ) ) ) |
36 |
33 35
|
sseqtrd |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> ( N ` ( G u. H ) ) C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) |
37 |
10 36
|
sstrd |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> F C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) |
38 |
9
|
adantr |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> Y e. F ) |
39 |
37 38
|
sseldd |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> Y e. ( N ` ( ( F u. H ) \ { Y } ) ) ) |
40 |
8
|
adantr |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> ( F u. H ) e. I ) |
41 |
|
ssun1 |
|- F C_ ( F u. H ) |
42 |
41 38
|
sselid |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> Y e. ( F u. H ) ) |
43 |
2 3 11 40 42
|
ismri2dad |
|- ( ( ph /\ G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) -> -. Y e. ( N ` ( ( F u. H ) \ { Y } ) ) ) |
44 |
39 43
|
pm2.65da |
|- ( ph -> -. G C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) |
45 |
|
nss |
|- ( -. G C_ ( N ` ( ( F u. H ) \ { Y } ) ) <-> E. g ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) |
46 |
44 45
|
sylib |
|- ( ph -> E. g ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) |
47 |
|
simprl |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> g e. G ) |
48 |
|
ssun1 |
|- ( F \ { Y } ) C_ ( ( F \ { Y } ) u. H ) |
49 |
48 24
|
sseqtrrid |
|- ( ph -> ( F \ { Y } ) C_ ( ( F u. H ) \ { Y } ) ) |
50 |
49 28
|
sstrd |
|- ( ph -> ( F \ { Y } ) C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) |
51 |
50
|
adantr |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> ( F \ { Y } ) C_ ( N ` ( ( F u. H ) \ { Y } ) ) ) |
52 |
|
simprr |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) |
53 |
51 52
|
ssneldd |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> -. g e. ( F \ { Y } ) ) |
54 |
|
unass |
|- ( ( ( F \ { Y } ) u. H ) u. { g } ) = ( ( F \ { Y } ) u. ( H u. { g } ) ) |
55 |
1
|
adantr |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> A e. ( Moore ` X ) ) |
56 |
4
|
adantr |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) ) |
57 |
8
|
adantr |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> ( F u. H ) e. I ) |
58 |
|
difss |
|- ( F \ { Y } ) C_ F |
59 |
|
unss1 |
|- ( ( F \ { Y } ) C_ F -> ( ( F \ { Y } ) u. H ) C_ ( F u. H ) ) |
60 |
58 59
|
mp1i |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> ( ( F \ { Y } ) u. H ) C_ ( F u. H ) ) |
61 |
55 2 3 57 60
|
mrissmrid |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> ( ( F \ { Y } ) u. H ) e. I ) |
62 |
6
|
adantr |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> G C_ ( X \ H ) ) |
63 |
62
|
difss2d |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> G C_ X ) |
64 |
63 47
|
sseldd |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> g e. X ) |
65 |
24
|
adantr |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> ( ( F u. H ) \ { Y } ) = ( ( F \ { Y } ) u. H ) ) |
66 |
65
|
fveq2d |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> ( N ` ( ( F u. H ) \ { Y } ) ) = ( N ` ( ( F \ { Y } ) u. H ) ) ) |
67 |
52 66
|
neleqtrd |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> -. g e. ( N ` ( ( F \ { Y } ) u. H ) ) ) |
68 |
55 2 3 56 61 64 67
|
mreexmrid |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> ( ( ( F \ { Y } ) u. H ) u. { g } ) e. I ) |
69 |
54 68
|
eqeltrrid |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> ( ( F \ { Y } ) u. ( H u. { g } ) ) e. I ) |
70 |
47 53 69
|
jca32 |
|- ( ( ph /\ ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) ) -> ( g e. G /\ ( -. g e. ( F \ { Y } ) /\ ( ( F \ { Y } ) u. ( H u. { g } ) ) e. I ) ) ) |
71 |
70
|
ex |
|- ( ph -> ( ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) -> ( g e. G /\ ( -. g e. ( F \ { Y } ) /\ ( ( F \ { Y } ) u. ( H u. { g } ) ) e. I ) ) ) ) |
72 |
71
|
eximdv |
|- ( ph -> ( E. g ( g e. G /\ -. g e. ( N ` ( ( F u. H ) \ { Y } ) ) ) -> E. g ( g e. G /\ ( -. g e. ( F \ { Y } ) /\ ( ( F \ { Y } ) u. ( H u. { g } ) ) e. I ) ) ) ) |
73 |
46 72
|
mpd |
|- ( ph -> E. g ( g e. G /\ ( -. g e. ( F \ { Y } ) /\ ( ( F \ { Y } ) u. ( H u. { g } ) ) e. I ) ) ) |
74 |
|
df-rex |
|- ( E. g e. G ( -. g e. ( F \ { Y } ) /\ ( ( F \ { Y } ) u. ( H u. { g } ) ) e. I ) <-> E. g ( g e. G /\ ( -. g e. ( F \ { Y } ) /\ ( ( F \ { Y } ) u. ( H u. { g } ) ) e. I ) ) ) |
75 |
73 74
|
sylibr |
|- ( ph -> E. g e. G ( -. g e. ( F \ { Y } ) /\ ( ( F \ { Y } ) u. ( H u. { g } ) ) e. I ) ) |