Metamath Proof Explorer


Theorem mreexexlem2d

Description: Used in mreexexlem4d to prove the induction step in mreexexd . See the proof of Proposition 4.2.1 in FaureFrolicher p. 86 to 87. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mreexexlem2d.1
|- ( ph -> A e. ( Moore ` X ) )
mreexexlem2d.2
|- N = ( mrCls ` A )
mreexexlem2d.3
|- I = ( mrInd ` A )
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 } ) ) )
mreexexlem2d.5
|- ( ph -> F C_ ( X \ H ) )
mreexexlem2d.6
|- ( ph -> G C_ ( X \ H ) )
mreexexlem2d.7
|- ( ph -> F C_ ( N ` ( G u. H ) ) )
mreexexlem2d.8
|- ( ph -> ( F u. H ) e. I )
mreexexlem2d.9
|- ( ph -> Y e. F )
Assertion mreexexlem2d
|- ( ph -> E. g e. G ( -. g e. ( F \ { Y } ) /\ ( ( F \ { Y } ) u. ( H u. { g } ) ) e. I ) )

Proof

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