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 syl5eq 
 |-  ( 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 incom 
 |-  ( ( F \ { r } ) i^i { r } ) = ( { r } i^i ( F \ { r } ) )
95 disjdif 
 |-  ( { r } i^i ( F \ { r } ) ) = (/)
96 94 95 eqtri 
 |-  ( ( F \ { r } ) i^i { r } ) = (/)
97 96 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 } ) = (/) )
98 ssdifin0 
 |-  ( i C_ ( G \ { q } ) -> ( i i^i { q } ) = (/) )
99 82 98 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 } ) = (/) )
100 unen 
 |-  ( ( ( ( F \ { r } ) ~~ i /\ { r } ~~ { q } ) /\ ( ( ( F \ { r } ) i^i { r } ) = (/) /\ ( i i^i { q } ) = (/) ) ) -> ( ( F \ { r } ) u. { r } ) ~~ ( i u. { q } ) )
101 90 93 97 99 100 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 } ) )
102 89 101 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 } ) )
103 unass 
 |-  ( ( i u. { q } ) u. H ) = ( i u. ( { q } u. H ) )
104 uncom 
 |-  ( { q } u. H ) = ( H u. { q } )
105 104 uneq2i 
 |-  ( i u. ( { q } u. H ) ) = ( i u. ( H u. { q } ) )
106 103 105 eqtr2i 
 |-  ( i u. ( H u. { q } ) ) = ( ( i u. { q } ) u. H )
107 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 )
108 106 107 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 )
109 breq2 
 |-  ( j = ( i u. { q } ) -> ( F ~~ j <-> F ~~ ( i u. { q } ) ) )
110 uneq1 
 |-  ( j = ( i u. { q } ) -> ( j u. H ) = ( ( i u. { q } ) u. H ) )
111 110 eleq1d 
 |-  ( j = ( i u. { q } ) -> ( ( j u. H ) e. I <-> ( ( i u. { q } ) u. H ) e. I ) )
112 109 111 anbi12d 
 |-  ( j = ( i u. { q } ) -> ( ( F ~~ j /\ ( j u. H ) e. I ) <-> ( F ~~ ( i u. { q } ) /\ ( ( i u. { q } ) u. H ) e. I ) ) )
113 112 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 ) )
114 87 102 108 113 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 ) )
115 76 114 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 ) )
116 31 115 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 ) )
117 30 116 rexlimddv 
 |-  ( ( ph /\ r e. F ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
118 117 adantlr 
 |-  ( ( ( ph /\ F =/= (/) ) /\ r e. F ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
119 22 118 exlimddv 
 |-  ( ( ph /\ F =/= (/) ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )
120 19 119 pm2.61dane 
 |-  ( ph -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )