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

Theorem tpres 6132
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 4865 . 2  |-  ( T  |`  ( _V  \  { A } ) )  =  ( T  i^i  (
( _V  \  { A } )  X.  _V ) )
2 elin 3649 . . . 4  |-  ( x  e.  ( T  i^i  ( ( _V  \  { A } )  X. 
_V ) )  <->  ( x  e.  T  /\  x  e.  ( ( _V  \  { A } )  X. 
_V ) ) )
3 elxp 4870 . . . . . 6  |-  ( x  e.  ( ( _V 
\  { A }
)  X.  _V )  <->  E. a E. b ( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) )
43anbi2i 698 . . . . 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 2492 . . . . . . . 8  |-  ( ph  ->  ( x  e.  T  <->  x  e.  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. } ) )
7 vex 3083 . . . . . . . . . . . . 13  |-  x  e. 
_V
87eltp 4045 . . . . . . . . . . . 12  |-  ( x  e.  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. }  <->  ( x  =  <. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) )
9 eldifsn 4125 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  e.  ( _V  \  { A } )  <->  ( a  e.  _V  /\  a  =/= 
A ) )
10 eqeq1 2426 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  <. a ,  b
>.  ->  ( x  = 
<. A ,  D >.  <->  <. a ,  b >.  =  <. A ,  D >. )
)
1110adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  (
x  =  <. A ,  D >. 
<-> 
<. a ,  b >.  =  <. A ,  D >. ) )
12 vex 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  a  e. 
_V
13 vex 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  b  e. 
_V
1412, 13opth 4695 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
a ,  b >.  =  <. A ,  D >.  <-> 
( a  =  A  /\  b  =  D ) )
15 eqneqall 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =/=  A  ->  (
( a  =  A  /\  b  =  D )  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
1814, 17syl5bi 220 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =/=  A  ->  ( <. a ,  b >.  =  <. A ,  D >.  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) )
1918adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  ( <. a ,  b >.  =  <. A ,  D >.  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) )
2011, 19sylbid 218 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  (
x  =  <. A ,  D >.  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2120impd 432 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
2221ex 435 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =/=  A  ->  (
x  =  <. a ,  b >.  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2322adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  _V  /\  a  =/=  A )  -> 
( x  =  <. a ,  b >.  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
249, 23sylbi 198 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  ( _V  \  { A } )  -> 
( x  =  <. a ,  b >.  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2524adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  ( _V 
\  { A }
)  /\  b  e.  _V )  ->  ( x  =  <. a ,  b
>.  ->  ( ( x  =  <. A ,  D >.  /\  ph )  -> 
( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2625impcom 431 . . . . . . . . . . . . . . . . 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 1773 . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . 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 386 . . . . . . . . . . . . . 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 385 . . . . . . . . . . . . . 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 1327 . . . . . . . . . . . 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 198 . . . . . . . . . . 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 4016 . . . . . . . . . . 11  |-  ( x  e.  { <. B ,  E >. ,  <. C ,  F >. }  <->  ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )
)
3836, 37syl6ibr 230 . . . . . . . . . 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 437 . . . . . . . . 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 218 . . . . . . 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 432 . . . . . 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 1175 . . . . . . . . . . . . 13  |-  ( x  =  <. B ,  E >.  ->  ( x  = 
<. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) )
44 3mix3 1176 . . . . . . . . . . . . 13  |-  ( x  =  <. C ,  F >.  ->  ( x  = 
<. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) )
4543, 44jaoi 380 . . . . . . . . . . . 12  |-  ( ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. )  ->  ( x  = 
<. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) )
4645adantr 466 . . . . . . . . . . 11  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  ( x  =  <. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )
)
476, 8syl6bb 264 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  T  <->  ( x  =  <. A ,  D >.  \/  x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
4847adantl 467 . . . . . . . . . . 11  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  ( x  e.  T  <->  ( x  =  <. A ,  D >.  \/  x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
4946, 48mpbird 235 . . . . . . . . . 10  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  x  e.  T )
50 tpres.b . . . . . . . . . . . . . . . 16  |-  ( ph  ->  B  e.  V )
51 elex 3089 . . . . . . . . . . . . . . . 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 3089 . . . . . . . . . . . . . . . 16  |-  ( E  e.  V  ->  E  e.  _V )
5654, 55syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  e.  _V )
5752, 53, 56jca31 536 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( B  e. 
_V  /\  B  =/=  A )  /\  E  e. 
_V ) )
5857anim2i 571 . . . . . . . . . . . . 13  |-  ( ( x  =  <. B ,  E >.  /\  ph )  -> 
( x  =  <. B ,  E >.  /\  (
( B  e.  _V  /\  B  =/=  A )  /\  E  e.  _V ) ) )
59 opeq12 4189 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  =  B  /\  b  =  E )  -> 
<. a ,  b >.  =  <. B ,  E >. )
6059eqeq2d 2436 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  B  /\  b  =  E )  ->  ( x  =  <. a ,  b >.  <->  x  =  <. B ,  E >. ) )
61 eleq1 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  B  ->  (
a  e.  _V  <->  B  e.  _V ) )
62 neeq1 2701 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  B  ->  (
a  =/=  A  <->  B  =/=  A ) )
6361, 62anbi12d 715 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  B  ->  (
( a  e.  _V  /\  a  =/=  A )  <-> 
( B  e.  _V  /\  B  =/=  A ) ) )
64 eleq1 2495 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  E  ->  (
b  e.  _V  <->  E  e.  _V ) )
6563, 64bi2anan9 881 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  B  /\  b  =  E )  ->  ( ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V )  <->  ( ( B  e.  _V  /\  B  =/=  A )  /\  E  e.  _V ) ) )
6660, 65anbi12d 715 . . . . . . . . . . . . . . . 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 3168 . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . 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 3089 . . . . . . . . . . . . . . . 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 3089 . . . . . . . . . . . . . . . 16  |-  ( F  e.  V  ->  F  e.  _V )
7775, 76syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  _V )
7873, 74, 77jca31 536 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( C  e. 
_V  /\  C  =/=  A )  /\  F  e. 
_V ) )
7978anim2i 571 . . . . . . . . . . . . 13  |-  ( ( x  =  <. C ,  F >.  /\  ph )  -> 
( x  =  <. C ,  F >.  /\  (
( C  e.  _V  /\  C  =/=  A )  /\  F  e.  _V ) ) )
80 opeq12 4189 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  =  C  /\  b  =  F )  -> 
<. a ,  b >.  =  <. C ,  F >. )
8180eqeq2d 2436 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  C  /\  b  =  F )  ->  ( x  =  <. a ,  b >.  <->  x  =  <. C ,  F >. ) )
82 eleq1 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  C  ->  (
a  e.  _V  <->  C  e.  _V ) )
83 neeq1 2701 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  C  ->  (
a  =/=  A  <->  C  =/=  A ) )
8482, 83anbi12d 715 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  C  ->  (
( a  e.  _V  /\  a  =/=  A )  <-> 
( C  e.  _V  /\  C  =/=  A ) ) )
85 eleq1 2495 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  F  ->  (
b  e.  _V  <->  F  e.  _V ) )
8684, 85bi2anan9 881 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  C  /\  b  =  F )  ->  ( ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V )  <->  ( ( C  e.  _V  /\  C  =/=  A )  /\  F  e.  _V ) ) )
8781, 86anbi12d 715 . . . . . . . . . . . . . . . 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 3168 . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . 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 791 . . . . . . . . . . 11  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  E. a E. b
( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) )
939anbi1i 699 . . . . . . . . . . . . 13  |-  ( ( a  e.  ( _V 
\  { A }
)  /\  b  e.  _V )  <->  ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) )
9493anbi2i 698 . . . . . . . . . . . 12  |-  ( ( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) )  <->  ( x  =  <. a ,  b
>.  /\  ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) )
95942exbii 1713 . . . . . . . . . . 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 215 . . . . . . . . . 10  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  E. a E. b
( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) )
9749, 96jca 534 . . . . . . . . 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 435 . . . . . . . 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 198 . . . . . . 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 193 . . . . 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 260 . . . 4  |-  ( ph  ->  ( ( x  e.  T  /\  x  e.  ( ( _V  \  { A } )  X. 
_V ) )  <->  x  e.  {
<. B ,  E >. , 
<. C ,  F >. } ) )
1032, 102syl5bb 260 . . 3  |-  ( ph  ->  ( x  e.  ( T  i^i  ( ( _V  \  { A } )  X.  _V ) )  <->  x  e.  {
<. B ,  E >. , 
<. C ,  F >. } ) )
104103eqrdv 2419 . 2  |-  ( ph  ->  ( T  i^i  (
( _V  \  { A } )  X.  _V ) )  =  { <. B ,  E >. , 
<. C ,  F >. } )
1051, 104syl5eq 2475 1  |-  ( ph  ->  ( T  |`  ( _V  \  { A }
) )  =  { <. B ,  E >. , 
<. C ,  F >. } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    \/ w3o 981    = wceq 1437   E.wex 1657    e. wcel 1872    =/= wne 2614   _Vcvv 3080    \ cdif 3433    i^i cin 3435   {csn 3998   {cpr 4000   {ctp 4002   <.cop 4004    X. cxp 4851    |` cres 4855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-opab 4483  df-xp 4859  df-res 4865
This theorem is referenced by:  estrres  16023
  Copyright terms: Public domain W3C validator