Metamath Proof Explorer

Theorem mreexexlemd

Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mreexexlemd.1 
|- ( ph -> X e. J )
mreexexlemd.2 
|- ( ph -> F C_ ( X \ H ) )
mreexexlemd.3 
|- ( ph -> G C_ ( X \ H ) )
mreexexlemd.4 
|- ( ph -> F C_ ( N ` ( G u. H ) ) )
mreexexlemd.5 
|- ( ph -> ( F u. H ) e. I )
mreexexlemd.6 
|- ( ph -> ( F ~~ K \/ G ~~ K ) )
mreexexlemd.7 
|- ( ph -> A. t A. u e. ~P ( X \ t ) A. v e. ~P ( X \ t ) ( ( ( u ~~ K \/ v ~~ K ) /\ u C_ ( N ` ( v u. t ) ) /\ ( u u. t ) e. I ) -> E. i e. ~P v ( u ~~ i /\ ( i u. t ) e. I ) ) )
Assertion mreexexlemd 
|- ( ph -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )

Proof

Step Hyp Ref Expression
1 mreexexlemd.1 
 |-  ( ph -> X e. J )
2 mreexexlemd.2 
 |-  ( ph -> F C_ ( X \ H ) )
3 mreexexlemd.3 
 |-  ( ph -> G C_ ( X \ H ) )
4 mreexexlemd.4 
 |-  ( ph -> F C_ ( N ` ( G u. H ) ) )
5 mreexexlemd.5 
 |-  ( ph -> ( F u. H ) e. I )
6 mreexexlemd.6 
 |-  ( ph -> ( F ~~ K \/ G ~~ K ) )
7 mreexexlemd.7 
 |-  ( ph -> A. t A. u e. ~P ( X \ t ) A. v e. ~P ( X \ t ) ( ( ( u ~~ K \/ v ~~ K ) /\ u C_ ( N ` ( v u. t ) ) /\ ( u u. t ) e. I ) -> E. i e. ~P v ( u ~~ i /\ ( i u. t ) e. I ) ) )
8 simplr 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> u = f )
9 8 breq1d 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( u ~~ K <-> f ~~ K ) )
10 simpr 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> v = g )
11 10 breq1d 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( v ~~ K <-> g ~~ K ) )
12 9 11 orbi12d 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( ( u ~~ K \/ v ~~ K ) <-> ( f ~~ K \/ g ~~ K ) ) )
13 simpll 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> t = h )
14 10 13 uneq12d 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( v u. t ) = ( g u. h ) )
15 14 fveq2d 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( N ` ( v u. t ) ) = ( N ` ( g u. h ) ) )
16 8 15 sseq12d 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( u C_ ( N ` ( v u. t ) ) <-> f C_ ( N ` ( g u. h ) ) ) )
17 8 13 uneq12d 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( u u. t ) = ( f u. h ) )
18 17 eleq1d 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( ( u u. t ) e. I <-> ( f u. h ) e. I ) )
19 12 16 18 3anbi123d 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( ( ( u ~~ K \/ v ~~ K ) /\ u C_ ( N ` ( v u. t ) ) /\ ( u u. t ) e. I ) <-> ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) )
20 simpllr 
 |-  ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> u = f )
21 simpr 
 |-  ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> i = j )
22 20 21 breq12d 
 |-  ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> ( u ~~ i <-> f ~~ j ) )
23 simplll 
 |-  ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> t = h )
24 21 23 uneq12d 
 |-  ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> ( i u. t ) = ( j u. h ) )
25 24 eleq1d 
 |-  ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> ( ( i u. t ) e. I <-> ( j u. h ) e. I ) )
26 22 25 anbi12d 
 |-  ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> ( ( u ~~ i /\ ( i u. t ) e. I ) <-> ( f ~~ j /\ ( j u. h ) e. I ) ) )
27 simplr 
 |-  ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> v = g )
28 27 pweqd 
 |-  ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> ~P v = ~P g )
29 26 28 cbvrexdva2 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( E. i e. ~P v ( u ~~ i /\ ( i u. t ) e. I ) <-> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) )
30 19 29 imbi12d 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ( ( ( ( u ~~ K \/ v ~~ K ) /\ u C_ ( N ` ( v u. t ) ) /\ ( u u. t ) e. I ) -> E. i e. ~P v ( u ~~ i /\ ( i u. t ) e. I ) ) <-> ( ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) ) )
31 simpl 
 |-  ( ( t = h /\ u = f ) -> t = h )
32 31 difeq2d 
 |-  ( ( t = h /\ u = f ) -> ( X \ t ) = ( X \ h ) )
33 32 pweqd 
 |-  ( ( t = h /\ u = f ) -> ~P ( X \ t ) = ~P ( X \ h ) )
34 33 adantr 
 |-  ( ( ( t = h /\ u = f ) /\ v = g ) -> ~P ( X \ t ) = ~P ( X \ h ) )
35 30 34 cbvraldva2 
 |-  ( ( t = h /\ u = f ) -> ( A. v e. ~P ( X \ t ) ( ( ( u ~~ K \/ v ~~ K ) /\ u C_ ( N ` ( v u. t ) ) /\ ( u u. t ) e. I ) -> E. i e. ~P v ( u ~~ i /\ ( i u. t ) e. I ) ) <-> A. g e. ~P ( X \ h ) ( ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) ) )
36 35 33 cbvraldva2 
 |-  ( t = h -> ( A. u e. ~P ( X \ t ) A. v e. ~P ( X \ t ) ( ( ( u ~~ K \/ v ~~ K ) /\ u C_ ( N ` ( v u. t ) ) /\ ( u u. t ) e. I ) -> E. i e. ~P v ( u ~~ i /\ ( i u. t ) e. I ) ) <-> A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) ) )
37 36 cbvalvw 
 |-  ( A. t A. u e. ~P ( X \ t ) A. v e. ~P ( X \ t ) ( ( ( u ~~ K \/ v ~~ K ) /\ u C_ ( N ` ( v u. t ) ) /\ ( u u. t ) e. I ) -> E. i e. ~P v ( u ~~ i /\ ( i u. t ) e. I ) ) <-> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) )
38 7 37 sylib 
 |-  ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) )
39 ssun2 
 |-  H C_ ( F u. H )
40 39 a1i 
 |-  ( ph -> H C_ ( F u. H ) )
41 5 40 ssexd 
 |-  ( ph -> H e. _V )
42 difexg 
 |-  ( X e. J -> ( X \ H ) e. _V )
43 1 42 syl 
 |-  ( ph -> ( X \ H ) e. _V )
44 43 2 sselpwd 
 |-  ( ph -> F e. ~P ( X \ H ) )
45 44 adantr 
 |-  ( ( ph /\ h = H ) -> F e. ~P ( X \ H ) )
46 simpr 
 |-  ( ( ph /\ h = H ) -> h = H )
47 46 difeq2d 
 |-  ( ( ph /\ h = H ) -> ( X \ h ) = ( X \ H ) )
48 47 pweqd 
 |-  ( ( ph /\ h = H ) -> ~P ( X \ h ) = ~P ( X \ H ) )
49 45 48 eleqtrrd 
 |-  ( ( ph /\ h = H ) -> F e. ~P ( X \ h ) )
50 43 3 sselpwd 
 |-  ( ph -> G e. ~P ( X \ H ) )
51 50 ad2antrr 
 |-  ( ( ( ph /\ h = H ) /\ f = F ) -> G e. ~P ( X \ H ) )
52 48 adantr 
 |-  ( ( ( ph /\ h = H ) /\ f = F ) -> ~P ( X \ h ) = ~P ( X \ H ) )
53 51 52 eleqtrrd 
 |-  ( ( ( ph /\ h = H ) /\ f = F ) -> G e. ~P ( X \ h ) )
54 simplr 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> f = F )
55 54 breq1d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( f ~~ K <-> F ~~ K ) )
56 simpr 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> g = G )
57 56 breq1d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( g ~~ K <-> G ~~ K ) )
58 55 57 orbi12d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( ( f ~~ K \/ g ~~ K ) <-> ( F ~~ K \/ G ~~ K ) ) )
59 simpllr 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> h = H )
60 56 59 uneq12d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( g u. h ) = ( G u. H ) )
61 60 fveq2d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( N ` ( g u. h ) ) = ( N ` ( G u. H ) ) )
62 54 61 sseq12d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( f C_ ( N ` ( g u. h ) ) <-> F C_ ( N ` ( G u. H ) ) ) )
63 54 59 uneq12d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( f u. h ) = ( F u. H ) )
64 63 eleq1d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( ( f u. h ) e. I <-> ( F u. H ) e. I ) )
65 58 62 64 3anbi123d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) <-> ( ( F ~~ K \/ G ~~ K ) /\ F C_ ( N ` ( G u. H ) ) /\ ( F u. H ) e. I ) ) )
66 56 pweqd 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ~P g = ~P G )
67 54 breq1d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( f ~~ j <-> F ~~ j ) )
68 59 uneq2d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( j u. h ) = ( j u. H ) )
69 68 eleq1d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( ( j u. h ) e. I <-> ( j u. H ) e. I ) )
70 67 69 anbi12d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( ( f ~~ j /\ ( j u. h ) e. I ) <-> ( F ~~ j /\ ( j u. H ) e. I ) ) )
71 66 70 rexeqbidv 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) <-> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) ) )
72 65 71 imbi12d 
 |-  ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( ( ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) <-> ( ( ( F ~~ K \/ G ~~ K ) /\ F C_ ( N ` ( G u. H ) ) /\ ( F u. H ) e. I ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) ) ) )
73 53 72 rspcdv 
 |-  ( ( ( ph /\ h = H ) /\ f = F ) -> ( A. g e. ~P ( X \ h ) ( ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) -> ( ( ( F ~~ K \/ G ~~ K ) /\ F C_ ( N ` ( G u. H ) ) /\ ( F u. H ) e. I ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) ) ) )
74 49 73 rspcimdv 
 |-  ( ( ph /\ h = H ) -> ( A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) -> ( ( ( F ~~ K \/ G ~~ K ) /\ F C_ ( N ` ( G u. H ) ) /\ ( F u. H ) e. I ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) ) ) )
75 41 74 spcimdv 
 |-  ( ph -> ( A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ K \/ g ~~ K ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. j e. ~P g ( f ~~ j /\ ( j u. h ) e. I ) ) -> ( ( ( F ~~ K \/ G ~~ K ) /\ F C_ ( N ` ( G u. H ) ) /\ ( F u. H ) e. I ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) ) ) )
76 38 75 mpd 
 |-  ( ph -> ( ( ( F ~~ K \/ G ~~ K ) /\ F C_ ( N ` ( G u. H ) ) /\ ( F u. H ) e. I ) -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) ) )
77 6 4 5 76 mp3and 
 |-  ( ph -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )