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 bilani 
 |-  ( ( ph /\ F =/= (/) ) -> E. r r e. F )
22 1 adantr 
 |-  ( ( ph /\ r e. F ) -> A e. ( Moore ` X ) )
23 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 } ) ) )
24 5 adantr 
 |-  ( ( ph /\ r e. F ) -> F C_ ( X \ H ) )
25 6 adantr 
 |-  ( ( ph /\ r e. F ) -> G C_ ( X \ H ) )
26 7 adantr 
 |-  ( ( ph /\ r e. F ) -> F C_ ( N ` ( G u. H ) ) )
27 8 adantr 
 |-  ( ( ph /\ r e. F ) -> ( F u. H ) e. I )
28 simpr 
 |-  ( ( ph /\ r e. F ) -> r e. F )
29 22 2 3 23 24 25 26 27 28 mreexexlem2d 
 |-  ( ( ph /\ r e. F ) -> E. q e. G ( -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) )
30 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 ) ) )
31 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 ) )
32 31 elfvexd 
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> X e. _V )
33 simpr2 
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> -. q e. ( F \ { r } ) )
34 difsnb 
 |-  ( -. q e. ( F \ { r } ) <-> ( ( F \ { r } ) \ { q } ) = ( F \ { r } ) )
35 33 34 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 } ) )
36 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 ) )
37 36 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 ) )
38 37 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 } ) )
39 35 38 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 } ) )
40 difun1 
 |-  ( X \ ( H u. { q } ) ) = ( ( X \ H ) \ { q } )
41 39 40 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 } ) ) )
42 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 ) )
43 42 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 } ) )
44 43 40 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 } ) ) )
45 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 ) ) )
46 simpr1 
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> q e. G )
47 uncom 
 |-  ( H u. { q } ) = ( { q } u. H )
48 47 uneq2i 
 |-  ( ( G \ { q } ) u. ( H u. { q } ) ) = ( ( G \ { q } ) u. ( { q } u. H ) )
49 unass 
 |-  ( ( ( G \ { q } ) u. { q } ) u. H ) = ( ( G \ { q } ) u. ( { q } u. H ) )
50 difsnid 
 |-  ( q e. G -> ( ( G \ { q } ) u. { q } ) = G )
51 50 uneq1d 
 |-  ( q e. G -> ( ( ( G \ { q } ) u. { q } ) u. H ) = ( G u. H ) )
52 49 51 eqtr3id 
 |-  ( q e. G -> ( ( G \ { q } ) u. ( { q } u. H ) ) = ( G u. H ) )
53 48 52 eqtrid 
 |-  ( q e. G -> ( ( G \ { q } ) u. ( H u. { q } ) ) = ( G u. H ) )
54 46 53 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 ) )
55 54 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 ) ) )
56 45 55 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 } ) ) ) )
57 56 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 } ) ) ) )
58 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 )
59 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 ) )
60 9 ad2antrr 
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> L e. _om )
61 simplr 
 |-  ( ( ( ph /\ r e. F ) /\ ( q e. G /\ -. q e. ( F \ { r } ) /\ ( ( F \ { r } ) u. ( H u. { q } ) ) e. I ) ) -> r e. F )
62 3anan12 
 |-  ( ( L e. _om /\ F ~~ suc L /\ r e. F ) <-> ( F ~~ suc L /\ ( L e. _om /\ r e. F ) ) )
63 dif1ennn 
 |-  ( ( L e. _om /\ F ~~ suc L /\ r e. F ) -> ( F \ { r } ) ~~ L )
64 62 63 sylbir 
 |-  ( ( F ~~ suc L /\ ( L e. _om /\ r e. F ) ) -> ( F \ { r } ) ~~ L )
65 64 expcom 
 |-  ( ( L e. _om /\ r e. F ) -> ( F ~~ suc L -> ( F \ { r } ) ~~ L ) )
66 60 61 65 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 ) )
67 3anan12 
 |-  ( ( L e. _om /\ G ~~ suc L /\ q e. G ) <-> ( G ~~ suc L /\ ( L e. _om /\ q e. G ) ) )
68 dif1ennn 
 |-  ( ( L e. _om /\ G ~~ suc L /\ q e. G ) -> ( G \ { q } ) ~~ L )
69 67 68 sylbir 
 |-  ( ( G ~~ suc L /\ ( L e. _om /\ q e. G ) ) -> ( G \ { q } ) ~~ L )
70 69 expcom 
 |-  ( ( L e. _om /\ q e. G ) -> ( G ~~ suc L -> ( G \ { q } ) ~~ L ) )
71 60 46 70 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 ) )
72 66 71 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 ) ) )
73 59 72 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 ) )
74 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 ) ) )
75 32 41 44 57 58 73 74 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 ) )
76 32 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 )
77 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 ) )
78 77 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 )
79 76 78 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 )
80 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 } ) )
81 80 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 } ) )
82 81 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 )
83 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 )
84 83 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 )
85 82 84 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 )
86 79 85 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 )
87 difsnid 
 |-  ( r e. F -> ( ( F \ { r } ) u. { r } ) = F )
88 87 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 )
89 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 )
90 en2sn 
 |-  ( ( r e. _V /\ q e. _V ) -> { r } ~~ { q } )
91 90 el2v 
 |-  { r } ~~ { q }
92 91 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 } )
93 disjdifr 
 |-  ( ( F \ { r } ) i^i { r } ) = (/)
94 93 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 } ) = (/) )
95 ssdifin0 
 |-  ( i C_ ( G \ { q } ) -> ( i i^i { q } ) = (/) )
96 81 95 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 } ) = (/) )
97 unen 
 |-  ( ( ( ( F \ { r } ) ~~ i /\ { r } ~~ { q } ) /\ ( ( ( F \ { r } ) i^i { r } ) = (/) /\ ( i i^i { q } ) = (/) ) ) -> ( ( F \ { r } ) u. { r } ) ~~ ( i u. { q } ) )
98 89 92 94 96 97 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 } ) )
99 88 98 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 } ) )
100 unass 
 |-  ( ( i u. { q } ) u. H ) = ( i u. ( { q } u. H ) )
101 uncom 
 |-  ( { q } u. H ) = ( H u. { q } )
102 101 uneq2i 
 |-  ( i u. ( { q } u. H ) ) = ( i u. ( H u. { q } ) )
103 100 102 eqtr2i 
 |-  ( i u. ( H u. { q } ) ) = ( ( i u. { q } ) u. H )
104 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 )
105 103 104 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 )
106 breq2 
 |-  ( j = ( i u. { q } ) -> ( F ~~ j <-> F ~~ ( i u. { q } ) ) )
107 uneq1 
 |-  ( j = ( i u. { q } ) -> ( j u. H ) = ( ( i u. { q } ) u. H ) )
108 107 eleq1d 
 |-  ( j = ( i u. { q } ) -> ( ( j u. H ) e. I <-> ( ( i u. { q } ) u. H ) e. I ) )
109 106 108 anbi12d 
 |-  ( j = ( i u. { q } ) -> ( ( F ~~ j /\ ( j u. H ) e. I ) <-> ( F ~~ ( i u. { q } ) /\ ( ( i u. { q } ) u. H ) e. I ) ) )
110 109 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 ) )
111 86 99 105 110 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 ) )
112 75 111 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 ) )
113 30 112 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 ) )
114 29 113 rexlimddv 
 |-  ( ( ph /\ r e. F ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
115 114 adantlr 
 |-  ( ( ( ph /\ F =/= (/) ) /\ r e. F ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
116 21 115 exlimddv 
 |-  ( ( ph /\ F =/= (/) ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
117 19 116 pm2.61dane 
 |-  ( ph -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )