Metamath Proof Explorer


Theorem mreexexlem4d

Description: Induction step 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 )
mreexexlem4d.9
|- ( ph -> L e. _om )
mreexexlem4d.A
|- ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ L \/ g ~~ L ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) )
mreexexlem4d.B
|- ( ph -> ( F ~~ suc L \/ G ~~ suc L ) )
Assertion mreexexlem4d
|- ( ph -> E. j e. ~P G ( F ~~ j /\ ( j 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 mreexexlem4d.9
 |-  ( ph -> L e. _om )
10 mreexexlem4d.A
 |-  ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ L \/ g ~~ L ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) )
11 mreexexlem4d.B
 |-  ( ph -> ( F ~~ suc L \/ G ~~ suc L ) )
12 1 adantr
 |-  ( ( ph /\ F = (/) ) -> A e. ( Moore ` X ) )
13 4 adantr
 |-  ( ( ph /\ F = (/) ) -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
14 5 adantr
 |-  ( ( ph /\ F = (/) ) -> F C_ ( X \ H ) )
15 6 adantr
 |-  ( ( ph /\ F = (/) ) -> G C_ ( X \ H ) )
16 7 adantr
 |-  ( ( ph /\ F = (/) ) -> F C_ ( N ` ( G u. H ) ) )
17 8 adantr
 |-  ( ( ph /\ F = (/) ) -> ( F u. H ) e. I )
18 animorrl
 |-  ( ( ph /\ F = (/) ) -> ( F = (/) \/ G = (/) ) )
19 12 2 3 13 14 15 16 17 18 mreexexlem3d
 |-  ( ( ph /\ F = (/) ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
20 n0
 |-  ( F =/= (/) <-> E. r r e. F )
21 20 biimpi
 |-  ( F =/= (/) -> E. r r e. F )
22 21 adantl
 |-  ( ( ph /\ F =/= (/) ) -> E. r r e. F )
23 1 adantr
 |-  ( ( ph /\ r e. F ) -> A e. ( Moore ` X ) )
24 4 adantr
 |-  ( ( ph /\ r e. F ) -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
25 5 adantr
 |-  ( ( ph /\ r e. F ) -> F C_ ( X \ H ) )
26 6 adantr
 |-  ( ( ph /\ r e. F ) -> G C_ ( X \ H ) )
27 7 adantr
 |-  ( ( ph /\ r e. F ) -> F C_ ( N ` ( G u. H ) ) )
28 8 adantr
 |-  ( ( ph /\ r e. F ) -> ( F u. H ) e. I )
29 simpr
 |-  ( ( ph /\ r e. F ) -> r e. F )
30 23 2 3 24 25 26 27 28 29 mreexexlem2d
 |-  ( ( ph /\ r e. F ) -> E. q e. G ( -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) )
31 3anass
 |-  ( ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) <-> ( q e. G /\ ( -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) )
32 1 ad2antrr
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> A e. ( Moore ` X ) )
33 32 elfvexd
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> X e. _V )
34 simpr2
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> -. q e. ( F \ { r } ) )
35 difsnb
 |-  ( -. q e. ( F \ { r } ) <-> ( ( F \ { r } ) \ { q } ) = ( F \ { r } ) )
36 34 35 sylib
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( ( F \ { r } ) \ { q } ) = ( F \ { r } ) )
37 5 ad2antrr
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> F C_ ( X \ H ) )
38 37 ssdifssd
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( F \ { r } ) C_ ( X \ H ) )
39 38 ssdifd
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( ( F \ { r } ) \ { q } ) C_ ( ( X \ H ) \ { q } ) )
40 36 39 eqsstrrd
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( F \ { r } ) C_ ( ( X \ H ) \ { q } ) )
41 difun1
 |-  ( X \ ( H u. { q } ) ) = ( ( X \ H ) \ { q } )
42 40 41 sseqtrrdi
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( F \ { r } ) C_ ( X \ ( H u. { q } ) ) )
43 6 ad2antrr
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> G C_ ( X \ H ) )
44 43 ssdifd
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( G \ { q } ) C_ ( ( X \ H ) \ { q } ) )
45 44 41 sseqtrrdi
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( G \ { q } ) C_ ( X \ ( H u. { q } ) ) )
46 7 ad2antrr
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> F C_ ( N ` ( G u. H ) ) )
47 simpr1
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> q e. G )
48 uncom
 |-  ( H u. { q } ) = ( { q } u. H )
49 48 uneq2i
 |-  ( ( G \ { q } ) u. ( H u. { q } ) ) = ( ( G \ { q } ) u. ( { q } u. H ) )
50 unass
 |-  ( ( ( G \ { q } ) u. { q } ) u. H ) = ( ( G \ { q } ) u. ( { q } u. H ) )
51 difsnid
 |-  ( q e. G -> ( ( G \ { q } ) u. { q } ) = G )
52 51 uneq1d
 |-  ( q e. G -> ( ( ( G \ { q } ) u. { q } ) u. H ) = ( G u. H ) )
53 50 52 eqtr3id
 |-  ( q e. G -> ( ( G \ { q } ) u. ( { q } u. H ) ) = ( G u. H ) )
54 49 53 eqtrid
 |-  ( q e. G -> ( ( G \ { q } ) u. ( H u. { q } ) ) = ( G u. H ) )
55 47 54 syl
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( ( G \ { q } ) u. ( H u. { q } ) ) = ( G u. H ) )
56 55 fveq2d
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( N ` ( ( G \ { q } ) u. ( H u. { q } ) ) ) = ( N ` ( G u. H ) ) )
57 46 56 sseqtrrd
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> F C_ ( N ` ( ( G \ { q } ) u. ( H u. { q } ) ) ) )
58 57 ssdifssd
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( F \ { r } ) C_ ( N ` ( ( G \ { q } ) u. ( H u. { q } ) ) ) )
59 simpr3
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( ( F \ { r } ) u. ( H u. { q } ) ) e. I )
60 11 ad2antrr
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( F ~~ suc L \/ G ~~ suc L ) )
61 9 ad2antrr
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> L e. _om )
62 simplr
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> r e. F )
63 3anan12
 |-  ( ( L e. _om /\ F ~~ suc L /\ r e. F ) <-> ( F ~~ suc L /\ ( L e. _om /\ r e. F ) ) )
64 dif1en
 |-  ( ( L e. _om /\ F ~~ suc L /\ r e. F ) -> ( F \ { r } ) ~~ L )
65 63 64 sylbir
 |-  ( ( F ~~ suc L /\ ( L e. _om /\ r e. F ) ) -> ( F \ { r } ) ~~ L )
66 65 expcom
 |-  ( ( L e. _om /\ r e. F ) -> ( F ~~ suc L -> ( F \ { r } ) ~~ L ) )
67 61 62 66 syl2anc
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( F ~~ suc L -> ( F \ { r } ) ~~ L ) )
68 3anan12
 |-  ( ( L e. _om /\ G ~~ suc L /\ q e. G ) <-> ( G ~~ suc L /\ ( L e. _om /\ q e. G ) ) )
69 dif1en
 |-  ( ( L e. _om /\ G ~~ suc L /\ q e. G ) -> ( G \ { q } ) ~~ L )
70 68 69 sylbir
 |-  ( ( G ~~ suc L /\ ( L e. _om /\ q e. G ) ) -> ( G \ { q } ) ~~ L )
71 70 expcom
 |-  ( ( L e. _om /\ q e. G ) -> ( G ~~ suc L -> ( G \ { q } ) ~~ L ) )
72 61 47 71 syl2anc
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( G ~~ suc L -> ( G \ { q } ) ~~ L ) )
73 67 72 orim12d
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( ( F ~~ suc L \/ G ~~ suc L ) -> ( ( F \ { r } ) ~~ L \/ ( G \ { q } ) ~~ L ) ) )
74 60 73 mpd
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> ( ( F \ { r } ) ~~ L \/ ( G \ { q } ) ~~ L ) )
75 10 ad2antrr
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ L \/ g ~~ L ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) )
76 33 42 45 58 59 74 75 mreexexlemd
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> E. i e. ~P ( G \ { q } ) ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) )
77 33 adantr
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> X e. _V )
78 6 ad3antrrr
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> G C_ ( X \ H ) )
79 78 difss2d
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> G C_ X )
80 77 79 ssexd
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> G e. _V )
81 simprl
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> i e. ~P ( G \ { q } ) )
82 81 elpwid
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> i C_ ( G \ { q } ) )
83 82 difss2d
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> i C_ G )
84 simplr1
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> q e. G )
85 84 snssd
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> { q } C_ G )
86 83 85 unssd
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> ( i u. { q } ) C_ G )
87 80 86 sselpwd
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> ( i u. { q } ) e. ~P G )
88 difsnid
 |-  ( r e. F -> ( ( F \ { r } ) u. { r } ) = F )
89 88 ad3antlr
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> ( ( F \ { r } ) u. { r } ) = F )
90 simprrl
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> ( F \ { r } ) ~~ i )
91 en2sn
 |-  ( ( r e. _V /\ q e. _V ) -> { r } ~~ { q } )
92 91 el2v
 |-  { r } ~~ { q }
93 92 a1i
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> { r } ~~ { q } )
94 disjdifr
 |-  ( ( F \ { r } ) i^i { r } ) = (/)
95 94 a1i
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> ( ( F \ { r } ) i^i { r } ) = (/) )
96 ssdifin0
 |-  ( i C_ ( G \ { q } ) -> ( i i^i { q } ) = (/) )
97 82 96 syl
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> ( i i^i { q } ) = (/) )
98 unen
 |-  ( ( ( ( F \ { r } ) ~~ i /\ { r } ~~ { q } ) /\ ( ( ( F \ { r } ) i^i { r } ) = (/) /\ ( i i^i { q } ) = (/) ) ) -> ( ( F \ { r } ) u. { r } ) ~~ ( i u. { q } ) )
99 90 93 95 97 98 syl22anc
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> ( ( F \ { r } ) u. { r } ) ~~ ( i u. { q } ) )
100 89 99 eqbrtrrd
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> F ~~ ( i u. { q } ) )
101 unass
 |-  ( ( i u. { q } ) u. H ) = ( i u. ( { q } u. H ) )
102 uncom
 |-  ( { q } u. H ) = ( H u. { q } )
103 102 uneq2i
 |-  ( i u. ( { q } u. H ) ) = ( i u. ( H u. { q } ) )
104 101 103 eqtr2i
 |-  ( i u. ( H u. { q } ) ) = ( ( i u. { q } ) u. H )
105 simprrr
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> ( i u. ( H u. { q } ) ) e. I )
106 104 105 eqeltrrid
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> ( ( i u. { q } ) u. H ) e. I )
107 breq2
 |-  ( j = ( i u. { q } ) -> ( F ~~ j <-> F ~~ ( i u. { q } ) ) )
108 uneq1
 |-  ( j = ( i u. { q } ) -> ( j u. H ) = ( ( i u. { q } ) u. H ) )
109 108 eleq1d
 |-  ( j = ( i u. { q } ) -> ( ( j u. H ) e. I <-> ( ( i u. { q } ) u. H ) e. I ) )
110 107 109 anbi12d
 |-  ( j = ( i u. { q } ) -> ( ( F ~~ j /\ ( j u. H ) e. I ) <-> ( F ~~ ( i u. { q } ) /\ ( ( i u. { q } ) u. H ) e. I ) ) )
111 110 rspcev
 |-  ( ( ( i u. { q } ) e. ~P G /\ ( F ~~ ( i u. { q } ) /\ ( ( i u. { q } ) u. H ) e. I ) ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
112 87 100 106 111 syl12anc
 |-  ( ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) /\ ( i e. ~P ( G \ { q } ) /\ ( ( F \ { r } ) ~~ i /\ ( i u. ( H u. { q } ) ) e. I ) ) ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
113 76 112 rexlimddv
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
114 31 113 sylan2br
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ ( -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
115 30 114 rexlimddv
 |-  ( ( ph /\ r e. F ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
116 115 adantlr
 |-  ( ( ( ph /\ F =/= (/) ) /\ r e. F ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
117 22 116 exlimddv
 |-  ( ( ph /\ F =/= (/) ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
118 19 117 pm2.61dane
 |-  ( ph -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )