MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mreexexlemd Unicode version

Theorem mreexexlemd 13546
Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 13550. (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.
StepHypRef 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 731 . . . . . . . . . . 11  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  u  =  f )
65breq1d 4033 . . . . . . . . . 10  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  (
u  ~~  K  <->  f  ~~  K ) )
7 simpr 447 . . . . . . . . . . 11  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  v  =  g )
87breq1d 4033 . . . . . . . . . 10  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  (
v  ~~  K  <->  g  ~~  K ) )
96, 8orbi12d 690 . . . . . . . . 9  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  (
( u  ~~  K  \/  v  ~~  K )  <-> 
( f  ~~  K  \/  g  ~~  K ) ) )
10 simpll 730 . . . . . . . . . . . 12  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  t  =  h )
117, 10uneq12d 3330 . . . . . . . . . . 11  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  (
v  u.  t )  =  ( g  u.  h ) )
1211fveq2d 5529 . . . . . . . . . 10  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  ( N `  ( v  u.  t ) )  =  ( N `  (
g  u.  h ) ) )
135, 12sseq12d 3207 . . . . . . . . 9  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  (
u  C_  ( N `  ( v  u.  t
) )  <->  f  C_  ( N `  ( g  u.  h ) ) ) )
145, 10uneq12d 3330 . . . . . . . . . 10  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  (
u  u.  t )  =  ( f  u.  h ) )
1514eleq1d 2349 . . . . . . . . 9  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  (
( u  u.  t
)  e.  I  <->  ( f  u.  h )  e.  I
) )
169, 13, 153anbi123d 1252 . . . . . . . 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 735 . . . . . . . . . . 11  |-  ( ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  /\  i  =  j )  ->  u  =  f )
18 simpr 447 . . . . . . . . . . 11  |-  ( ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  /\  i  =  j )  ->  i  =  j )
1917, 18breq12d 4036 . . . . . . . . . 10  |-  ( ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  /\  i  =  j )  ->  ( u  ~~  i  <->  f 
~~  j ) )
20 simplll 734 . . . . . . . . . . . 12  |-  ( ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  /\  i  =  j )  ->  t  =  h )
2118, 20uneq12d 3330 . . . . . . . . . . 11  |-  ( ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  /\  i  =  j )  ->  ( i  u.  t
)  =  ( j  u.  h ) )
2221eleq1d 2349 . . . . . . . . . 10  |-  ( ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  /\  i  =  j )  ->  ( ( i  u.  t )  e.  I  <->  ( j  u.  h )  e.  I ) )
2319, 22anbi12d 691 . . . . . . . . 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 731 . . . . . . . . . 10  |-  ( ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  /\  i  =  j )  ->  v  =  g )
2524pweqd 3630 . . . . . . . . 9  |-  ( ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  /\  i  =  j )  ->  ~P v  =  ~P g )
2623, 25cbvrexdva2 2769 . . . . . . . 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
) ) )
2716, 26imbi12d 311 . . . . . . 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 443 . . . . . . . . . 10  |-  ( ( t  =  h  /\  u  =  f )  ->  t  =  h )
2928difeq2d 3294 . . . . . . . . 9  |-  ( ( t  =  h  /\  u  =  f )  ->  ( X  \  t
)  =  ( X 
\  h ) )
3029pweqd 3630 . . . . . . . 8  |-  ( ( t  =  h  /\  u  =  f )  ->  ~P ( X  \ 
t )  =  ~P ( X  \  h
) )
3130adantr 451 . . . . . . 7  |-  ( ( ( t  =  h  /\  u  =  f )  /\  v  =  g )  ->  ~P ( X  \  t
)  =  ~P ( X  \  h ) )
3227, 31cbvraldva2 2768 . . . . . 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
) ) ) )
3332, 30cbvraldva2 2768 . . . . 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
) ) ) )
3433cbvalv 1942 . . . 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
) ) )
354, 34sylib 188 . . 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 3339 . . . . . 6  |-  H  C_  ( F  u.  H
)
3736a1i 10 . . . . 5  |-  ( ph  ->  H  C_  ( F  u.  H ) )
383, 37ssexd 4161 . . . 4  |-  ( ph  ->  H  e.  _V )
39 mreexexlemd.2 . . . . . . . 8  |-  ( ph  ->  F  C_  ( X  \  H ) )
40 mreexexlemd.1 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  J )
41 difexg 4162 . . . . . . . . . . 11  |-  ( X  e.  J  ->  ( X  \  H )  e. 
_V )
4240, 41syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( X  \  H
)  e.  _V )
4342, 39ssexd 4161 . . . . . . . . 9  |-  ( ph  ->  F  e.  _V )
44 elpwg 3632 . . . . . . . . 9  |-  ( F  e.  _V  ->  ( F  e.  ~P ( X  \  H )  <->  F  C_  ( X  \  H ) ) )
4543, 44syl 15 . . . . . . . 8  |-  ( ph  ->  ( F  e.  ~P ( X  \  H )  <-> 
F  C_  ( X  \  H ) ) )
4639, 45mpbird 223 . . . . . . 7  |-  ( ph  ->  F  e.  ~P ( X  \  H ) )
4746adantr 451 . . . . . 6  |-  ( (
ph  /\  h  =  H )  ->  F  e.  ~P ( X  \  H ) )
48 simpr 447 . . . . . . . 8  |-  ( (
ph  /\  h  =  H )  ->  h  =  H )
4948difeq2d 3294 . . . . . . 7  |-  ( (
ph  /\  h  =  H )  ->  ( X  \  h )  =  ( X  \  H
) )
5049pweqd 3630 . . . . . 6  |-  ( (
ph  /\  h  =  H )  ->  ~P ( X  \  h
)  =  ~P ( X  \  H ) )
5147, 50eleqtrrd 2360 . . . . 5  |-  ( (
ph  /\  h  =  H )  ->  F  e.  ~P ( X  \  h ) )
52 mreexexlemd.3 . . . . . . . . 9  |-  ( ph  ->  G  C_  ( X  \  H ) )
5342, 52ssexd 4161 . . . . . . . . . 10  |-  ( ph  ->  G  e.  _V )
54 elpwg 3632 . . . . . . . . . 10  |-  ( G  e.  _V  ->  ( G  e.  ~P ( X  \  H )  <->  G  C_  ( X  \  H ) ) )
5553, 54syl 15 . . . . . . . . 9  |-  ( ph  ->  ( G  e.  ~P ( X  \  H )  <-> 
G  C_  ( X  \  H ) ) )
5652, 55mpbird 223 . . . . . . . 8  |-  ( ph  ->  G  e.  ~P ( X  \  H ) )
5756ad2antrr 706 . . . . . . 7  |-  ( ( ( ph  /\  h  =  H )  /\  f  =  F )  ->  G  e.  ~P ( X  \  H ) )
5850adantr 451 . . . . . . 7  |-  ( ( ( ph  /\  h  =  H )  /\  f  =  F )  ->  ~P ( X  \  h
)  =  ~P ( X  \  H ) )
5957, 58eleqtrrd 2360 . . . . . 6  |-  ( ( ( ph  /\  h  =  H )  /\  f  =  F )  ->  G  e.  ~P ( X  \  h ) )
60 simplr 731 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  f  =  F )
6160breq1d 4033 . . . . . . . . 9  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
f  ~~  K  <->  F  ~~  K ) )
62 simpr 447 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  g  =  G )
6362breq1d 4033 . . . . . . . . 9  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
g  ~~  K  <->  G  ~~  K ) )
6461, 63orbi12d 690 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
( f  ~~  K  \/  g  ~~  K )  <-> 
( F  ~~  K  \/  G  ~~  K ) ) )
65 simpllr 735 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  h  =  H )
6662, 65uneq12d 3330 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
g  u.  h )  =  ( G  u.  H ) )
6766fveq2d 5529 . . . . . . . . 9  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  ( N `  ( g  u.  h ) )  =  ( N `  ( G  u.  H )
) )
6860, 67sseq12d 3207 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
f  C_  ( N `  ( g  u.  h
) )  <->  F  C_  ( N `  ( G  u.  H ) ) ) )
6960, 65uneq12d 3330 . . . . . . . . 9  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
f  u.  h )  =  ( F  u.  H ) )
7069eleq1d 2349 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
( f  u.  h
)  e.  I  <->  ( F  u.  H )  e.  I
) )
7164, 68, 703anbi123d 1252 . . . . . . 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
) ) )
7262pweqd 3630 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  ~P g  =  ~P G
)
7360breq1d 4033 . . . . . . . . 9  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
f  ~~  j  <->  F  ~~  j ) )
7465uneq2d 3329 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
j  u.  h )  =  ( j  u.  H ) )
7574eleq1d 2349 . . . . . . . . 9  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
( j  u.  h
)  e.  I  <->  ( j  u.  H )  e.  I
) )
7673, 75anbi12d 691 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  =  H )  /\  f  =  F
)  /\  g  =  G )  ->  (
( f  ~~  j  /\  ( j  u.  h
)  e.  I )  <-> 
( F  ~~  j  /\  ( j  u.  H
)  e.  I ) ) )
7772, 76rexeqbidv 2749 . . . . . . 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
) ) )
7871, 77imbi12d 311 . . . . . 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 ) ) ) )
7959, 78rspcdv 2887 . . . . 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 ) ) ) )
8051, 79rspcimdv 2885 . . . 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 ) ) ) )
8138, 80spcimdv 2865 . . 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 ) ) ) )
8235, 81mpd 14 . 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 ) ) )
831, 2, 3, 82mp3and 1280 1  |-  ( ph  ->  E. j  e.  ~P  G ( F  ~~  j  /\  ( j  u.  H )  e.  I
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934   A.wal 1527    = wceq 1623    e. wcel 1684   A.wral 2543   E.wrex 2544   _Vcvv 2788    \ cdif 3149    u. cun 3150    C_ wss 3152   ~Pcpw 3625   class class class wbr 4023   ` cfv 5255    ~~ cen 6860
This theorem is referenced by:  mreexexlem4d  13549  mreexexd  13550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator