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

Theorem tpres 6103
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 4834 . 2  |-  ( T  |`  ( _V  \  { A } ) )  =  ( T  i^i  (
( _V  \  { A } )  X.  _V ) )
2 elin 3625 . . . 4  |-  ( x  e.  ( T  i^i  ( ( _V  \  { A } )  X. 
_V ) )  <->  ( x  e.  T  /\  x  e.  ( ( _V  \  { A } )  X. 
_V ) ) )
3 elxp 4839 . . . . . 6  |-  ( x  e.  ( ( _V 
\  { A }
)  X.  _V )  <->  E. a E. b ( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) )
43anbi2i 692 . . . . 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 2472 . . . . . . . 8  |-  ( ph  ->  ( x  e.  T  <->  x  e.  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. } ) )
7 vex 3061 . . . . . . . . . . . . 13  |-  x  e. 
_V
87eltp 4016 . . . . . . . . . . . 12  |-  ( x  e.  { <. A ,  D >. ,  <. B ,  E >. ,  <. C ,  F >. }  <->  ( x  =  <. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) )
9 eldifsn 4096 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  e.  ( _V  \  { A } )  <->  ( a  e.  _V  /\  a  =/= 
A ) )
10 eqeq1 2406 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  <. a ,  b
>.  ->  ( x  = 
<. A ,  D >.  <->  <. a ,  b >.  =  <. A ,  D >. )
)
1110adantl 464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  (
x  =  <. A ,  D >. 
<-> 
<. a ,  b >.  =  <. A ,  D >. ) )
12 vex 3061 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  a  e. 
_V
13 vex 3061 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  b  e. 
_V
1412, 13opth 4664 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( <.
a ,  b >.  =  <. A ,  D >.  <-> 
( a  =  A  /\  b  =  D ) )
15 eqneqall 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  A  ->  (
a  =/=  A  -> 
( b  =  D  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) ) )
1615com12 29 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =/=  A  ->  (
a  =  A  -> 
( b  =  D  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) ) )
1716impd 429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =/=  A  ->  (
( a  =  A  /\  b  =  D )  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
1814, 17syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =/=  A  ->  ( <. a ,  b >.  =  <. A ,  D >.  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) )
1918adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  ( <. a ,  b >.  =  <. A ,  D >.  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) ) ) )
2011, 19sylbid 215 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  (
x  =  <. A ,  D >.  ->  ( ph  ->  ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2120impd 429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  =/=  A  /\  x  =  <. a ,  b >. )  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
2221ex 432 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =/=  A  ->  (
x  =  <. a ,  b >.  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2322adantl 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  _V  /\  a  =/=  A )  -> 
( x  =  <. a ,  b >.  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
249, 23sylbi 195 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  ( _V  \  { A } )  -> 
( x  =  <. a ,  b >.  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2524adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  ( _V 
\  { A }
)  /\  b  e.  _V )  ->  ( x  =  <. a ,  b
>.  ->  ( ( x  =  <. A ,  D >.  /\  ph )  -> 
( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) ) )
2625impcom 428 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) )  ->  (
( x  =  <. A ,  D >.  /\  ph )  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
2726com12 29 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  <. A ,  D >.  /\  ph )  -> 
( ( x  = 
<. a ,  b >.  /\  ( a  e.  ( _V  \  { A } )  /\  b  e.  _V ) )  -> 
( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
2827exlimdvv 1746 . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . 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 383 . . . . . . . . . . . . . 14  |-  ( x  =  <. B ,  E >.  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) )
3231a1d 25 . . . . . . . . . . . . 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 382 . . . . . . . . . . . . . 14  |-  ( x  =  <. C ,  F >.  ->  ( x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) )
3433a1d 25 . . . . . . . . . . . . 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 1293 . . . . . . . . . . . 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 195 . . . . . . . . . . 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 3989 . . . . . . . . . . 11  |-  ( x  e.  { <. B ,  E >. ,  <. C ,  F >. }  <->  ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )
)
3836, 37syl6ibr 227 . . . . . . . . . 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 434 . . . . . . . . 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 29 . . . . . . . 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 215 . . . . . . 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 429 . . . . . 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 1167 . . . . . . . . . . . . 13  |-  ( x  =  <. B ,  E >.  ->  ( x  = 
<. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) )
44 3mix3 1168 . . . . . . . . . . . . 13  |-  ( x  =  <. C ,  F >.  ->  ( x  = 
<. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) )
4543, 44jaoi 377 . . . . . . . . . . . 12  |-  ( ( x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. )  ->  ( x  = 
<. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  = 
<. C ,  F >. ) )
4645adantr 463 . . . . . . . . . . 11  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  ( x  =  <. A ,  D >.  \/  x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )
)
476, 8syl6bb 261 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  T  <->  ( x  =  <. A ,  D >.  \/  x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
4847adantl 464 . . . . . . . . . . 11  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  ( x  e.  T  <->  ( x  =  <. A ,  D >.  \/  x  = 
<. B ,  E >.  \/  x  =  <. C ,  F >. ) ) )
4946, 48mpbird 232 . . . . . . . . . 10  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  x  e.  T )
50 tpres.b . . . . . . . . . . . . . . . 16  |-  ( ph  ->  B  e.  V )
51 elex 3067 . . . . . . . . . . . . . . . 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 3067 . . . . . . . . . . . . . . . 16  |-  ( E  e.  V  ->  E  e.  _V )
5654, 55syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  e.  _V )
5752, 53, 56jca31 532 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( B  e. 
_V  /\  B  =/=  A )  /\  E  e. 
_V ) )
5857anim2i 567 . . . . . . . . . . . . 13  |-  ( ( x  =  <. B ,  E >.  /\  ph )  -> 
( x  =  <. B ,  E >.  /\  (
( B  e.  _V  /\  B  =/=  A )  /\  E  e.  _V ) ) )
59 opeq12 4160 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  =  B  /\  b  =  E )  -> 
<. a ,  b >.  =  <. B ,  E >. )
6059eqeq2d 2416 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  B  /\  b  =  E )  ->  ( x  =  <. a ,  b >.  <->  x  =  <. B ,  E >. ) )
61 eleq1 2474 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  B  ->  (
a  e.  _V  <->  B  e.  _V ) )
62 neeq1 2684 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  B  ->  (
a  =/=  A  <->  B  =/=  A ) )
6361, 62anbi12d 709 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  B  ->  (
( a  e.  _V  /\  a  =/=  A )  <-> 
( B  e.  _V  /\  B  =/=  A ) ) )
64 eleq1 2474 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  E  ->  (
b  e.  _V  <->  E  e.  _V ) )
6563, 64bi2anan9 874 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  B  /\  b  =  E )  ->  ( ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V )  <->  ( ( B  e.  _V  /\  B  =/=  A )  /\  E  e.  _V ) ) )
6660, 65anbi12d 709 . . . . . . . . . . . . . . . 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 3145 . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . 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 3067 . . . . . . . . . . . . . . . 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 3067 . . . . . . . . . . . . . . . 16  |-  ( F  e.  V  ->  F  e.  _V )
7775, 76syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  _V )
7873, 74, 77jca31 532 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( C  e. 
_V  /\  C  =/=  A )  /\  F  e. 
_V ) )
7978anim2i 567 . . . . . . . . . . . . 13  |-  ( ( x  =  <. C ,  F >.  /\  ph )  -> 
( x  =  <. C ,  F >.  /\  (
( C  e.  _V  /\  C  =/=  A )  /\  F  e.  _V ) ) )
80 opeq12 4160 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  =  C  /\  b  =  F )  -> 
<. a ,  b >.  =  <. C ,  F >. )
8180eqeq2d 2416 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  C  /\  b  =  F )  ->  ( x  =  <. a ,  b >.  <->  x  =  <. C ,  F >. ) )
82 eleq1 2474 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  C  ->  (
a  e.  _V  <->  C  e.  _V ) )
83 neeq1 2684 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  C  ->  (
a  =/=  A  <->  C  =/=  A ) )
8482, 83anbi12d 709 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  C  ->  (
( a  e.  _V  /\  a  =/=  A )  <-> 
( C  e.  _V  /\  C  =/=  A ) ) )
85 eleq1 2474 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  F  ->  (
b  e.  _V  <->  F  e.  _V ) )
8684, 85bi2anan9 874 . . . . . . . . . . . . . . . . 17  |-  ( ( a  =  C  /\  b  =  F )  ->  ( ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V )  <->  ( ( C  e.  _V  /\  C  =/=  A )  /\  F  e.  _V ) ) )
8781, 86anbi12d 709 . . . . . . . . . . . . . . . 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 3145 . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . 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 785 . . . . . . . . . . 11  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  E. a E. b
( x  =  <. a ,  b >.  /\  (
( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) )
939anbi1i 693 . . . . . . . . . . . . 13  |-  ( ( a  e.  ( _V 
\  { A }
)  /\  b  e.  _V )  <->  ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) )
9493anbi2i 692 . . . . . . . . . . . 12  |-  ( ( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) )  <->  ( x  =  <. a ,  b
>.  /\  ( ( a  e.  _V  /\  a  =/=  A )  /\  b  e.  _V ) ) )
95942exbii 1689 . . . . . . . . . . 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 212 . . . . . . . . . 10  |-  ( ( ( x  =  <. B ,  E >.  \/  x  =  <. C ,  F >. )  /\  ph )  ->  E. a E. b
( x  =  <. a ,  b >.  /\  (
a  e.  ( _V 
\  { A }
)  /\  b  e.  _V ) ) )
9749, 96jca 530 . . . . . . . . 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 432 . . . . . . . 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 195 . . . . . . 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 29 . . . . . 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 191 . . . . 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 257 . . . 4  |-  ( ph  ->  ( ( x  e.  T  /\  x  e.  ( ( _V  \  { A } )  X. 
_V ) )  <->  x  e.  {
<. B ,  E >. , 
<. C ,  F >. } ) )
1032, 102syl5bb 257 . . 3  |-  ( ph  ->  ( x  e.  ( T  i^i  ( ( _V  \  { A } )  X.  _V ) )  <->  x  e.  {
<. B ,  E >. , 
<. C ,  F >. } ) )
104103eqrdv 2399 . 2  |-  ( ph  ->  ( T  i^i  (
( _V  \  { A } )  X.  _V ) )  =  { <. B ,  E >. , 
<. C ,  F >. } )
1051, 104syl5eq 2455 1  |-  ( ph  ->  ( T  |`  ( _V  \  { A }
) )  =  { <. B ,  E >. , 
<. C ,  F >. } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367    \/ w3o 973    = wceq 1405   E.wex 1633    e. wcel 1842    =/= wne 2598   _Vcvv 3058    \ cdif 3410    i^i cin 3412   {csn 3971   {cpr 3973   {ctp 3975   <.cop 3977    X. cxp 4820    |` cres 4824
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-opab 4453  df-xp 4828  df-res 4834
This theorem is referenced by:  estrres  15730
  Copyright terms: Public domain W3C validator