Theorem mreexexlemd 16304

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

Hypotheses

Ref	Expression
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

Ref	Expression
mreexexlemd	|- ( ph -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )

Distinct variable groups:   j, F   j, G   j, H   ph, j   u, t, v, i, I, j   t, K, u, v   t, N, u, v   t, X, u, v

Allowed substitution hints:   ph( v, u, t, i)   F( v, u, t, i)   G( v, u, t, i)   H( v, u, t, i)   J( v, u, t, i, j)   K( i, j)   N( i, j)   X( i, j)

Proof of Theorem mreexexlemd

Dummy variables f g h are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mreexexlemd.6	. 2 |- ( ph -> ( F ~~ K \/ G ~~ K ) )
2		mreexexlemd.4	. 2 |- ( ph -> F C_ ( N ` ( G u. H ) ) )
3		mreexexlemd.5	. 2 |- ( ph -> ( F u. H ) e. I )
4		mreexexlemd.7	. . . 4 |- ( 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 ) ) )
5		simplr 792	. . . . . . . . . . 11 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> u = f )
6	5	breq1d 4663	. . . . . . . . . 10 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> ( u ~~ K <-> f ~~ K ) )
7		simpr 477	. . . . . . . . . . 11 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> v = g )
8	7	breq1d 4663	. . . . . . . . . 10 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> ( v ~~ K <-> g ~~ K ) )
9	6, 8	orbi12d 746	. . . . . . . . 9 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> ( ( u ~~ K \/ v ~~ K ) <-> ( f ~~ K \/ g ~~ K ) ) )
10		simpll 790	. . . . . . . . . . . 12 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> t = h )
11	7, 10	uneq12d 3768	. . . . . . . . . . 11 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> ( v u. t ) = ( g u. h ) )
12	11	fveq2d 6195	. . . . . . . . . 10 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> ( N ` ( v u. t ) ) = ( N ` ( g u. h ) ) )
13	5, 12	sseq12d 3634	. . . . . . . . 9 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> ( u C_ ( N ` ( v u. t ) ) <-> f C_ ( N ` ( g u. h ) ) ) )
14	5, 10	uneq12d 3768	. . . . . . . . . 10 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> ( u u. t ) = ( f u. h ) )
15	14	eleq1d 2686	. . . . . . . . 9 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> ( ( u u. t ) e. I <-> ( f u. h ) e. I ) )
16	9, 13, 15	3anbi123d 1399	. . . . . . . 8 |- ( ( ( 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 ) ) )
17		simpllr 799	. . . . . . . . . . 11 |- ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> u = f )
18		simpr 477	. . . . . . . . . . 11 |- ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> i = j )
19	17, 18	breq12d 4666	. . . . . . . . . 10 |- ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> ( u ~~ i <-> f ~~ j ) )
20		simplll 798	. . . . . . . . . . . 12 |- ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> t = h )
21	18, 20	uneq12d 3768	. . . . . . . . . . 11 |- ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> ( i u. t ) = ( j u. h ) )
22	21	eleq1d 2686	. . . . . . . . . 10 |- ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> ( ( i u. t ) e. I <-> ( j u. h ) e. I ) )
23	19, 22	anbi12d 747	. . . . . . . . 9 |- ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> ( ( u ~~ i /\ ( i u. t ) e. I ) <-> ( f ~~ j /\ ( j u. h ) e. I ) ) )
24		simplr 792	. . . . . . . . . 10 |- ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> v = g )
25	24	pweqd 4163	. . . . . . . . 9 |- ( ( ( ( t = h /\ u = f ) /\ v = g ) /\ i = j ) -> ~P v = ~P g )
26	23, 25	cbvrexdva2 3176	. . . . . . . 8 |- ( ( ( 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 ) ) )
27	16, 26	imbi12d 334	. . . . . . 7 |- ( ( ( 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 ) ) ) )
28		simpl 473	. . . . . . . . . 10 |- ( ( t = h /\ u = f ) -> t = h )
29	28	difeq2d 3728	. . . . . . . . 9 |- ( ( t = h /\ u = f ) -> ( X \ t ) = ( X \ h ) )
30	29	pweqd 4163	. . . . . . . 8 |- ( ( t = h /\ u = f ) -> ~P ( X \ t ) = ~P ( X \ h ) )
31	30	adantr 481	. . . . . . 7 |- ( ( ( t = h /\ u = f ) /\ v = g ) -> ~P ( X \ t ) = ~P ( X \ h ) )
32	27, 31	cbvraldva2 3175	. . . . . 6 |- ( ( 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 ) ) ) )
33	32, 30	cbvraldva2 3175	. . . . 5 |- ( 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 ) ) ) )
34	33	cbvalv 2273	. . . 4 |- ( 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 ) ) )
35	4, 34	sylib 208	. . 3 |- ( 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 ) ) )
36		ssun2 3777	. . . . . 6 |- H C_ ( F u. H )
37	36	a1i 11	. . . . 5 |- ( ph -> H C_ ( F u. H ) )
38	3, 37	ssexd 4805	. . . 4 |- ( ph -> H e. _V )
39		mreexexlemd.1	. . . . . . . . 9 |- ( ph -> X e. J )
40		difexg 4808	. . . . . . . . 9 |- ( X e. J -> ( X \ H ) e. _V )
41	39, 40	syl 17	. . . . . . . 8 |- ( ph -> ( X \ H ) e. _V )
42		mreexexlemd.2	. . . . . . . 8 |- ( ph -> F C_ ( X \ H ) )
43	41, 42	sselpwd 4807	. . . . . . 7 |- ( ph -> F e. ~P ( X \ H ) )
44	43	adantr 481	. . . . . 6 |- ( ( ph /\ h = H ) -> F e. ~P ( X \ H ) )
45		simpr 477	. . . . . . . 8 |- ( ( ph /\ h = H ) -> h = H )
46	45	difeq2d 3728	. . . . . . 7 |- ( ( ph /\ h = H ) -> ( X \ h ) = ( X \ H ) )
47	46	pweqd 4163	. . . . . 6 |- ( ( ph /\ h = H ) -> ~P ( X \ h ) = ~P ( X \ H ) )
48	44, 47	eleqtrrd 2704	. . . . 5 |- ( ( ph /\ h = H ) -> F e. ~P ( X \ h ) )
49		mreexexlemd.3	. . . . . . . . 9 |- ( ph -> G C_ ( X \ H ) )
50	41, 49	sselpwd 4807	. . . . . . . 8 |- ( ph -> G e. ~P ( X \ H ) )
51	50	ad2antrr 762	. . . . . . 7 |- ( ( ( ph /\ h = H ) /\ f = F ) -> G e. ~P ( X \ H ) )
52	47	adantr 481	. . . . . . 7 |- ( ( ( ph /\ h = H ) /\ f = F ) -> ~P ( X \ h ) = ~P ( X \ H ) )
53	51, 52	eleqtrrd 2704	. . . . . 6 |- ( ( ( ph /\ h = H ) /\ f = F ) -> G e. ~P ( X \ h ) )
54		simplr 792	. . . . . . . . . 10 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> f = F )
55	54	breq1d 4663	. . . . . . . . 9 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( f ~~ K <-> F ~~ K ) )
56		simpr 477	. . . . . . . . . 10 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> g = G )
57	56	breq1d 4663	. . . . . . . . 9 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( g ~~ K <-> G ~~ K ) )
58	55, 57	orbi12d 746	. . . . . . . 8 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( ( f ~~ K \/ g ~~ K ) <-> ( F ~~ K \/ G ~~ K ) ) )
59		simpllr 799	. . . . . . . . . . 11 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> h = H )
60	56, 59	uneq12d 3768	. . . . . . . . . 10 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( g u. h ) = ( G u. H ) )
61	60	fveq2d 6195	. . . . . . . . 9 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( N ` ( g u. h ) ) = ( N ` ( G u. H ) ) )
62	54, 61	sseq12d 3634	. . . . . . . 8 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( f C_ ( N ` ( g u. h ) ) <-> F C_ ( N ` ( G u. H ) ) ) )
63	54, 59	uneq12d 3768	. . . . . . . . 9 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( f u. h ) = ( F u. H ) )
64	63	eleq1d 2686	. . . . . . . 8 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( ( f u. h ) e. I <-> ( F u. H ) e. I ) )
65	58, 62, 64	3anbi123d 1399	. . . . . . 7 |- ( ( ( ( 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 4163	. . . . . . . 8 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ~P g = ~P G )
67	54	breq1d 4663	. . . . . . . . 9 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( f ~~ j <-> F ~~ j ) )
68	59	uneq2d 3767	. . . . . . . . . 10 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( j u. h ) = ( j u. H ) )
69	68	eleq1d 2686	. . . . . . . . 9 |- ( ( ( ( ph /\ h = H ) /\ f = F ) /\ g = G ) -> ( ( j u. h ) e. I <-> ( j u. H ) e. I ) )
70	67, 69	anbi12d 747	. . . . . . . 8 |- ( ( ( ( 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 3153	. . . . . . 7 |- ( ( ( ( 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 334	. . . . . 6 |- ( ( ( ( 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 3312	. . . . 5 |- ( ( ( 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	48, 73	rspcimdv 3310	. . . 4 |- ( ( 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	38, 74	spcimdv 3290	. . 3 |- ( 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	35, 75	mpd 15	. 2 |- ( 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	1, 2, 3, 76	mp3and 1427	1 |- ( ph -> E. j e. ~P G ( F ~~ j /\ ( j u. H ) e. I ) )

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   \ cdif 3571   u. cun 3572   C_ wss 3574   ~Pcpw 4158   class class class wbr 4653   ` cfv 5888   ~~ cen 7952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896

This theorem is referenced by:  mreexexlem4d  16307  mreexexd  16308  mreexexdOLD  16309