Metamath Proof Explorer

Theorem mreexexlem3d

Description: Base case of the induction in mreexexd . (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 )
mreexexlem3d.9 
|- ( ph -> ( F = (/) \/ G = (/) ) )
Assertion mreexexlem3d 
|- ( ph -> E. i e. ~P G ( F ~~ i /\ ( i u. H ) 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 mreexexlem3d.9 
 |-  ( ph -> ( F = (/) \/ G = (/) ) )
10 simpr 
 |-  ( ( ph /\ F = (/) ) -> F = (/) )
11 1 adantr 
 |-  ( ( ph /\ G = (/) ) -> A e. ( Moore ` X ) )
12 7 adantr 
 |-  ( ( ph /\ G = (/) ) -> F C_ ( N ` ( G u. H ) ) )
13 simpr 
 |-  ( ( ph /\ G = (/) ) -> G = (/) )
14 13 uneq1d 
 |-  ( ( ph /\ G = (/) ) -> ( G u. H ) = ( (/) u. H ) )
15 uncom 
 |-  ( H u. (/) ) = ( (/) u. H )
16 un0 
 |-  ( H u. (/) ) = H
17 15 16 eqtr3i 
 |-  ( (/) u. H ) = H
18 14 17 eqtrdi 
 |-  ( ( ph /\ G = (/) ) -> ( G u. H ) = H )
19 18 fveq2d 
 |-  ( ( ph /\ G = (/) ) -> ( N ` ( G u. H ) ) = ( N ` H ) )
20 12 19 sseqtrd 
 |-  ( ( ph /\ G = (/) ) -> F C_ ( N ` H ) )
21 8 adantr 
 |-  ( ( ph /\ G = (/) ) -> ( F u. H ) e. I )
22 3 11 21 mrissd 
 |-  ( ( ph /\ G = (/) ) -> ( F u. H ) C_ X )
23 22 unssbd 
 |-  ( ( ph /\ G = (/) ) -> H C_ X )
24 11 2 23 mrcssidd 
 |-  ( ( ph /\ G = (/) ) -> H C_ ( N ` H ) )
25 20 24 unssd 
 |-  ( ( ph /\ G = (/) ) -> ( F u. H ) C_ ( N ` H ) )
26 ssun2 
 |-  H C_ ( F u. H )
27 26 a1i 
 |-  ( ( ph /\ G = (/) ) -> H C_ ( F u. H ) )
28 11 2 3 25 27 21 mrissmrcd 
 |-  ( ( ph /\ G = (/) ) -> ( F u. H ) = H )
29 ssequn1 
 |-  ( F C_ H <-> ( F u. H ) = H )
30 28 29 sylibr 
 |-  ( ( ph /\ G = (/) ) -> F C_ H )
31 5 adantr 
 |-  ( ( ph /\ G = (/) ) -> F C_ ( X \ H ) )
32 30 31 ssind 
 |-  ( ( ph /\ G = (/) ) -> F C_ ( H i^i ( X \ H ) ) )
33 disjdif 
 |-  ( H i^i ( X \ H ) ) = (/)
34 32 33 sseqtrdi 
 |-  ( ( ph /\ G = (/) ) -> F C_ (/) )
35 ss0b 
 |-  ( F C_ (/) <-> F = (/) )
36 34 35 sylib 
 |-  ( ( ph /\ G = (/) ) -> F = (/) )
37 10 36 9 mpjaodan 
 |-  ( ph -> F = (/) )
38 0elpw 
 |-  (/) e. ~P G
39 37 38 eqeltrdi 
 |-  ( ph -> F e. ~P G )
40 1 elfvexd 
 |-  ( ph -> X e. _V )
41 5 difss2d 
 |-  ( ph -> F C_ X )
42 40 41 ssexd 
 |-  ( ph -> F e. _V )
43 enrefg 
 |-  ( F e. _V -> F ~~ F )
44 42 43 syl 
 |-  ( ph -> F ~~ F )
45 breq2 
 |-  ( i = F -> ( F ~~ i <-> F ~~ F ) )
46 uneq1 
 |-  ( i = F -> ( i u. H ) = ( F u. H ) )
47 46 eleq1d 
 |-  ( i = F -> ( ( i u. H ) e. I <-> ( F u. H ) e. I ) )
48 45 47 anbi12d 
 |-  ( i = F -> ( ( F ~~ i /\ ( i u. H ) e. I ) <-> ( F ~~ F /\ ( F u. H ) e. I ) ) )
49 48 rspcev 
 |-  ( ( F e. ~P G /\ ( F ~~ F /\ ( F u. H ) e. I ) ) -> E. i e. ~P G ( F ~~ i /\ ( i u. H ) e. I ) )
50 39 44 8 49 syl12anc 
 |-  ( ph -> E. i e. ~P G ( F ~~ i /\ ( i u. H ) e. I ) )