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 syl5eq 
 |-  ( 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 sseldi 
 |-  ( ( 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 ) )