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

Theorem tpres 6146
Description: An unordered triple of ordered pairs restricted to all but one first components of the pairs is an unordered pair of ordered pairs. (Contributed by AV, 14-Mar-2020.)
Hypotheses
Ref Expression
tpres.t  |-  ( ph  ->  T  =  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. } )
tpres.b  |-  ( ph  ->  B  e.  V )
tpres.c  |-  ( ph  ->  C  e.  V )
tpres.e  |-  ( ph  ->  E  e.  V )
tpres.f  |-  ( ph  ->  F  e.  V )
tpres.1  |-  ( ph  ->  B  =/=  A )
tpres.2  |-  ( ph  ->  C  =/=  A )
Assertion
Ref Expression
tpres  |-  ( ph  ->  ( T  |`  ( _V  \  { A }
) )  =  { <. B ,  E >. , 
<. C ,  F >. } )

Proof of Theorem tpres
Dummy variables  a 
b  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-res 4868 . 2  |-  ( T  |`  ( _V  \  { A } ) )  =  ( T  i^i  (
( _V  \  { A } )  X.  _V ) )
2 elin 3629 . . . 4  |-  ( x  e.  ( T  i^i  ( ( _V  \  { A } )  X. 
_V ) )  <->  ( x  e.  T  /\  x  e.  ( ( _V  \  { A } )  X. 
_V ) ) )
3 elxp 4873 . . . . . 6  |-  ( x  e.  ( ( _V 
\  { A }
)  X.  _V )  <->  E. a E. b ( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) )
43anbi2i 705 . . . . 5  |-  ( ( x  e.  T  /\  x  e.  ( ( _V  \  { A }
)  X.  _V )
)  <->  ( x  e.  T  /\  E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) ) ) )
5 tpres.t . . . . . . . . 9  |-  ( ph  ->  T  =  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. } )
65eleq2d 2525 . . . . . . . 8  |-  ( ph  ->  ( x  e.  T  <->  x  e.  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. } ) )
7 vex 3060 . . . . . . . . . . . . 13  |-  x  e. 
_V
87eltp 4029 . . . . . . . . . . . 12  |-  ( x  e.  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. }  <->  ( x  =  <. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) )
9 eldifsn 4110 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  e.  ( _V  \  { A } )  <->  ( a  e.  _V  /\  a  =/= 
A ) )
10 eqeq1 2466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  <. a ,  b
>.  ->  ( x  = 
<. A ,  D >.  <->  <. a ,  b >.  =  <. A ,  D >. )
)
1110adantl 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  (
x  =  <. A ,  D >. 
<-> 
<. a ,  b >.  =  <. A ,  D >. ) )
12 vex 3060 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  a  e. 
_V
13 vex 3060 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  b  e. 
_V
1412, 13opth 4693 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
a ,  b >.  =  <. A ,  D >.  <-> 
( a  =  A  /\  b  =  D ) )
15 eqneqall 2646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  A  ->  (
a  =/=  A  -> 
( b  =  D  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) ) )
1615com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =/=  A  ->  (
a  =  A  -> 
( b  =  D  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) ) )
1716impd 437 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =/=  A  ->  (
( a  =  A  /\  b  =  D )  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
1814, 17syl5bi 225 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =/=  A  ->  ( <. a ,  b >.  =  <. A ,  D >.  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) )
1918adantr 471 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  ( <. a ,  b >.  =  <. A ,  D >.  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) )
2011, 19sylbid 223 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  (
x  =  <. A ,  D >.  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2120impd 437 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
2221ex 440 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =/=  A  ->  (
x  =  <. a ,  b >.  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2322adantl 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  _V  /\  a  =/=  A )  -> 
( x  =  <. a ,  b >.  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
249, 23sylbi 200 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  ( _V  \  { A } )  -> 
( x  =  <. a ,  b >.  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2524adantr 471 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  ( _V 
\  { A }
)  /\  b  e.  _V )  ->  ( x  =  <. a ,  b
>.  ->  ( ( x  =  <. A ,  D >.  /\  ph )  -> 
( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2625impcom 436 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) )  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
2726com12 32 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  <. A ,  D >.  /\  ph )  -> 
( ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) )  -> 
( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
2827exlimdvv 1791 . . . . . . . . . . . . . . 15  |-  ( ( x  =  <. A ,  D >.  /\  ph )  -> 
( E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) )  -> 
( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
2928ex 440 . . . . . . . . . . . . . 14  |-  ( x  =  <. A ,  D >.  ->  ( ph  ->  ( E. a E. b
( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) )  ->  (
x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) )
3029impd 437 . . . . . . . . . . . . 13  |-  ( x  =  <. A ,  D >.  ->  ( ( ph  /\ 
E. a E. b
( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) )  -> 
( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
31 orc 391 . . . . . . . . . . . . . 14  |-  ( x  =  <. B ,  E >.  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) )
3231a1d 26 . . . . . . . . . . . . 13  |-  ( x  =  <. B ,  E >.  ->  ( ( ph  /\ 
E. a E. b
( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) )  -> 
( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
33 olc 390 . . . . . . . . . . . . . 14  |-  ( x  =  <. C ,  F >.  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) )
3433a1d 26 . . . . . . . . . . . . 13  |-  ( x  =  <. C ,  F >.  ->  ( ( ph  /\ 
E. a E. b
( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) )  -> 
( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
3530, 32, 343jaoi 1340 . . . . . . . . . . . 12  |-  ( ( x  =  <. A ,  D >.  \/  x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. )  ->  (
( ph  /\  E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) ) )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
368, 35sylbi 200 . . . . . . . . . . 11  |-  ( x  e.  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. }  ->  (
( ph  /\  E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) ) )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
377elpr 3998 . . . . . . . . . . 11  |-  ( x  e.  { <. B ,  E >. ,  <. C ,  F >. }  <->  ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )
)
3836, 37syl6ibr 235 . . . . . . . . . 10  |-  ( x  e.  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. }  ->  (
( ph  /\  E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) ) )  ->  x  e.  { <. B ,  E >. , 
<. C ,  F >. } ) )
3938expd 442 . . . . . . . . 9  |-  ( x  e.  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. }  ->  ( ph  ->  ( E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) )  ->  x  e.  { <. B ,  E >. ,  <. C ,  F >. } ) ) )
4039com12 32 . . . . . . . 8  |-  ( ph  ->  ( x  e.  { <. A ,  D >. , 
<. B ,  E >. , 
<. C ,  F >. }  ->  ( E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) )  ->  x  e.  { <. B ,  E >. ,  <. C ,  F >. } ) ) )
416, 40sylbid 223 . . . . . . 7  |-  ( ph  ->  ( x  e.  T  ->  ( E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) )  ->  x  e.  { <. B ,  E >. ,  <. C ,  F >. } ) ) )
4241impd 437 . . . . . 6  |-  ( ph  ->  ( ( x  e.  T  /\  E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) ) )  ->  x  e.  { <. B ,  E >. , 
<. C ,  F >. } ) )
43 3mix2 1184 . . . . . . . . . . . . 13  |-  ( x  =  <. B ,  E >.  ->  ( x  = 
<. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) )
44 3mix3 1185 . . . . . . . . . . . . 13  |-  ( x  =  <. C ,  F >.  ->  ( x  = 
<. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) )
4543, 44jaoi 385 . . . . . . . . . . . 12  |-  ( ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. )  ->  ( x  = 
<. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) )
4645adantr 471 . . . . . . . . . . 11  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  ( x  =  <. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )
)
476, 8syl6bb 269 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  T  <->  ( x  =  <. A ,  D >.  \/  x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
4847adantl 472 . . . . . . . . . . 11  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  ( x  e.  T  <->  ( x  =  <. A ,  D >.  \/  x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
4946, 48mpbird 240 . . . . . . . . . 10  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  x  e.  T )
50 tpres.b . . . . . . . . . . . . . . . 16  |-  ( ph  ->  B  e.  V )
51 elex 3066 . . . . . . . . . . . . . . . 16  |-  ( B  e.  V  ->  B  e.  _V )
5250, 51syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  _V )
53 tpres.1 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  =/=  A )
54 tpres.e . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E  e.  V )
55 elex 3066 . . . . . . . . . . . . . . . 16  |-  ( E  e.  V  ->  E  e.  _V )
5654, 55syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  e.  _V )
5752, 53, 56jca31 541 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( B  e. 
_V  /\  B  =/=  A )  /\  E  e. 
_V ) )
5857anim2i 577 . . . . . . . . . . . . 13  |-  ( ( x  =  <. B ,  E >.  /\  ph )  -> 
( x  =  <. B ,  E >.  /\  (
( B  e.  _V  /\  B  =/=  A )  /\  E  e.  _V ) ) )
59 opeq12 4182 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  =  B  /\  b  =  E )  -> 
<. a ,  b >.  =  <. B ,  E >. )
6059eqeq2d 2472 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  B  /\  b  =  E )  ->  ( x  =  <. a ,  b >.  <->  x  =  <. B ,  E >. ) )
61 eleq1 2528 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  B  ->  (
a  e.  _V  <->  B  e.  _V ) )
62 neeq1 2698 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  B  ->  (
a  =/=  A  <->  B  =/=  A ) )
6361, 62anbi12d 722 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  B  ->  (
( a  e.  _V  /\  a  =/=  A )  <-> 
( B  e.  _V  /\  B  =/=  A ) ) )
64 eleq1 2528 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  E  ->  (
b  e.  _V  <->  E  e.  _V ) )
6563, 64bi2anan9 889 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  B  /\  b  =  E )  ->  ( ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V )  <->  ( ( B  e.  _V  /\  B  =/=  A )  /\  E  e.  _V ) ) )
6660, 65anbi12d 722 . . . . . . . . . . . . . . . 16  |-  ( ( a  =  B  /\  b  =  E )  ->  ( ( x  = 
<. a ,  b >.  /\  ( ( a  e. 
_V  /\  a  =/=  A )  /\  b  e. 
_V ) )  <->  ( x  =  <. B ,  E >.  /\  ( ( B  e.  _V  /\  B  =/=  A )  /\  E  e.  _V ) ) ) )
6766spc2egv 3148 . . . . . . . . . . . . . . 15  |-  ( ( B  e.  V  /\  E  e.  V )  ->  ( ( x  = 
<. B ,  E >.  /\  ( ( B  e. 
_V  /\  B  =/=  A )  /\  E  e. 
_V ) )  ->  E. a E. b ( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) ) )
6850, 54, 67syl2anc 671 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( x  = 
<. B ,  E >.  /\  ( ( B  e. 
_V  /\  B  =/=  A )  /\  E  e. 
_V ) )  ->  E. a E. b ( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) ) )
6968adantl 472 . . . . . . . . . . . . 13  |-  ( ( x  =  <. B ,  E >.  /\  ph )  -> 
( ( x  = 
<. B ,  E >.  /\  ( ( B  e. 
_V  /\  B  =/=  A )  /\  E  e. 
_V ) )  ->  E. a E. b ( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) ) )
7058, 69mpd 15 . . . . . . . . . . . 12  |-  ( ( x  =  <. B ,  E >.  /\  ph )  ->  E. a E. b ( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) )
71 tpres.c . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  V )
72 elex 3066 . . . . . . . . . . . . . . . 16  |-  ( C  e.  V  ->  C  e.  _V )
7371, 72syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  _V )
74 tpres.2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  =/=  A )
75 tpres.f . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F  e.  V )
76 elex 3066 . . . . . . . . . . . . . . . 16  |-  ( F  e.  V  ->  F  e.  _V )
7775, 76syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  _V )
7873, 74, 77jca31 541 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( C  e. 
_V  /\  C  =/=  A )  /\  F  e. 
_V ) )
7978anim2i 577 . . . . . . . . . . . . 13  |-  ( ( x  =  <. C ,  F >.  /\  ph )  -> 
( x  =  <. C ,  F >.  /\  (
( C  e.  _V  /\  C  =/=  A )  /\  F  e.  _V ) ) )
80 opeq12 4182 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  =  C  /\  b  =  F )  -> 
<. a ,  b >.  =  <. C ,  F >. )
8180eqeq2d 2472 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  C  /\  b  =  F )  ->  ( x  =  <. a ,  b >.  <->  x  =  <. C ,  F >. ) )
82 eleq1 2528 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  C  ->  (
a  e.  _V  <->  C  e.  _V ) )
83 neeq1 2698 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  C  ->  (
a  =/=  A  <->  C  =/=  A ) )
8482, 83anbi12d 722 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  C  ->  (
( a  e.  _V  /\  a  =/=  A )  <-> 
( C  e.  _V  /\  C  =/=  A ) ) )
85 eleq1 2528 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  F  ->  (
b  e.  _V  <->  F  e.  _V ) )
8684, 85bi2anan9 889 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  C  /\  b  =  F )  ->  ( ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V )  <->  ( ( C  e.  _V  /\  C  =/=  A )  /\  F  e.  _V ) ) )
8781, 86anbi12d 722 . . . . . . . . . . . . . . . 16  |-  ( ( a  =  C  /\  b  =  F )  ->  ( ( x  = 
<. a ,  b >.  /\  ( ( a  e. 
_V  /\  a  =/=  A )  /\  b  e. 
_V ) )  <->  ( x  =  <. C ,  F >.  /\  ( ( C  e.  _V  /\  C  =/=  A )  /\  F  e.  _V ) ) ) )
8887spc2egv 3148 . . . . . . . . . . . . . . 15  |-  ( ( C  e.  V  /\  F  e.  V )  ->  ( ( x  = 
<. C ,  F >.  /\  ( ( C  e. 
_V  /\  C  =/=  A )  /\  F  e. 
_V ) )  ->  E. a E. b ( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) ) )
8971, 75, 88syl2anc 671 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( x  = 
<. C ,  F >.  /\  ( ( C  e. 
_V  /\  C  =/=  A )  /\  F  e. 
_V ) )  ->  E. a E. b ( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) ) )
9089adantl 472 . . . . . . . . . . . . 13  |-  ( ( x  =  <. C ,  F >.  /\  ph )  -> 
( ( x  = 
<. C ,  F >.  /\  ( ( C  e. 
_V  /\  C  =/=  A )  /\  F  e. 
_V ) )  ->  E. a E. b ( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) ) )
9179, 90mpd 15 . . . . . . . . . . . 12  |-  ( ( x  =  <. C ,  F >.  /\  ph )  ->  E. a E. b ( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) )
9270, 91jaoian 798 . . . . . . . . . . 11  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  E. a E. b
( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) )
939anbi1i 706 . . . . . . . . . . . . 13  |-  ( ( a  e.  ( _V 
\  { A }
)  /\  b  e.  _V )  <->  ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) )
9493anbi2i 705 . . . . . . . . . . . 12  |-  ( ( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) )  <->  ( x  =  <. a ,  b
>.  /\  ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) )
95942exbii 1730 . . . . . . . . . . 11  |-  ( E. a E. b ( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) )  <->  E. a E. b ( x  = 
<. a ,  b >.  /\  ( ( a  e. 
_V  /\  a  =/=  A )  /\  b  e. 
_V ) ) )
9692, 95sylibr 217 . . . . . . . . . 10  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  E. a E. b
( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) )
9749, 96jca 539 . . . . . . . . 9  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  ( x  e.  T  /\  E. a E. b
( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) ) )
9897ex 440 . . . . . . . 8  |-  ( ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. )  ->  ( ph  ->  ( x  e.  T  /\  E. a E. b ( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) ) ) )
9937, 98sylbi 200 . . . . . . 7  |-  ( x  e.  { <. B ,  E >. ,  <. C ,  F >. }  ->  ( ph  ->  ( x  e.  T  /\  E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) ) ) ) )
10099com12 32 . . . . . 6  |-  ( ph  ->  ( x  e.  { <. B ,  E >. , 
<. C ,  F >. }  ->  ( x  e.  T  /\  E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) ) ) ) )
10142, 100impbid 195 . . . . 5  |-  ( ph  ->  ( ( x  e.  T  /\  E. a E. b ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) ) )  <-> 
x  e.  { <. B ,  E >. ,  <. C ,  F >. } ) )
1024, 101syl5bb 265 . . . 4  |-  ( ph  ->  ( ( x  e.  T  /\  x  e.  ( ( _V  \  { A } )  X. 
_V ) )  <->  x  e.  {
<. B ,  E >. , 
<. C ,  F >. } ) )
1032, 102syl5bb 265 . . 3  |-  ( ph  ->  ( x  e.  ( T  i^i  ( ( _V  \  { A } )  X.  _V ) )  <->  x  e.  {
<. B ,  E >. , 
<. C ,  F >. } ) )
104103eqrdv 2460 . 2  |-  ( ph  ->  ( T  i^i  (
( _V  \  { A } )  X.  _V ) )  =  { <. B ,  E >. , 
<. C ,  F >. } )
1051, 104syl5eq 2508 1  |-  ( ph  ->  ( T  |`  ( _V  \  { A }
) )  =  { <. B ,  E >. , 
<. C ,  F >. } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    \/ w3o 990    = wceq 1455   E.wex 1674    e. wcel 1898    =/= wne 2633   _Vcvv 3057    \ cdif 3413    i^i cin 3415   {csn 3980   {cpr 3982   {ctp 3984   <.cop 3986    X. cxp 4854    |` cres 4858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-opab 4478  df-xp 4862  df-res 4868
This theorem is referenced by:  estrres  16079
  Copyright terms: Public domain W3C validator