Metamath Proof Explorer

Theorem tpres

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)

Ref Expression
Hypotheses 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 tpres 
|- ( ph -> ( T |` ( _V \ { A } ) ) = { <. B , E >. , <. C , F >. } )

Proof

Step Hyp Ref Expression
1 tpres.t 
 |-  ( ph -> T = { <. A , D >. , <. B , E >. , <. C , F >. } )
2 tpres.b 
 |-  ( ph -> B e. V )
3 tpres.c 
 |-  ( ph -> C e. V )
4 tpres.e 
 |-  ( ph -> E e. V )
5 tpres.f 
 |-  ( ph -> F e. V )
6 tpres.1 
 |-  ( ph -> B =/= A )
7 tpres.2 
 |-  ( ph -> C =/= A )
8 df-res 
 |-  ( T |` ( _V \ { A } ) ) = ( T i^i ( ( _V \ { A } ) X. _V ) )
9 elin 
 |-  ( x e. ( T i^i ( ( _V \ { A } ) X. _V ) ) <-> ( x e. T /\ x e. ( ( _V \ { A } ) X. _V ) ) )
10 elxp 
 |-  ( x e. ( ( _V \ { A } ) X. _V ) <-> E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) )
11 10 anbi2i 
 |-  ( ( 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 ) ) ) )
12 1 eleq2d 
 |-  ( ph -> ( x e. T <-> x e. { <. A , D >. , <. B , E >. , <. C , F >. } ) )
13 vex 
 |-  x e. _V
14 13 eltp 
 |-  ( x e. { <. A , D >. , <. B , E >. , <. C , F >. } <-> ( x = <. A , D >. \/ x = <. B , E >. \/ x = <. C , F >. ) )
15 eldifsn 
 |-  ( a e. ( _V \ { A } ) <-> ( a e. _V /\ a =/= A ) )
16 eqeq1 
 |-  ( x = <. a , b >. -> ( x = <. A , D >. <-> <. a , b >. = <. A , D >. ) )
17 16 adantl 
 |-  ( ( a =/= A /\ x = <. a , b >. ) -> ( x = <. A , D >. <-> <. a , b >. = <. A , D >. ) )
18 vex 
 |-  a e. _V
19 vex 
 |-  b e. _V
20 18 19 opth 
 |-  ( <. a , b >. = <. A , D >. <-> ( a = A /\ b = D ) )
21 eqneqall 
 |-  ( a = A -> ( a =/= A -> ( b = D -> ( ph -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) ) )
22 21 com12 
 |-  ( a =/= A -> ( a = A -> ( b = D -> ( ph -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) ) )
23 22 impd 
 |-  ( a =/= A -> ( ( a = A /\ b = D ) -> ( ph -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) )
24 20 23 syl5bi 
 |-  ( a =/= A -> ( <. a , b >. = <. A , D >. -> ( ph -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) )
25 24 adantr 
 |-  ( ( a =/= A /\ x = <. a , b >. ) -> ( <. a , b >. = <. A , D >. -> ( ph -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) )
26 17 25 sylbid 
 |-  ( ( a =/= A /\ x = <. a , b >. ) -> ( x = <. A , D >. -> ( ph -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) )
27 26 impd 
 |-  ( ( a =/= A /\ x = <. a , b >. ) -> ( ( x = <. A , D >. /\ ph ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) )
28 27 ex 
 |-  ( a =/= A -> ( x = <. a , b >. -> ( ( x = <. A , D >. /\ ph ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) )
29 28 adantl 
 |-  ( ( a e. _V /\ a =/= A ) -> ( x = <. a , b >. -> ( ( x = <. A , D >. /\ ph ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) )
30 15 29 sylbi 
 |-  ( a e. ( _V \ { A } ) -> ( x = <. a , b >. -> ( ( x = <. A , D >. /\ ph ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) )
31 30 adantr 
 |-  ( ( a e. ( _V \ { A } ) /\ b e. _V ) -> ( x = <. a , b >. -> ( ( x = <. A , D >. /\ ph ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) )
32 31 impcom 
 |-  ( ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) -> ( ( x = <. A , D >. /\ ph ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) )
33 32 com12 
 |-  ( ( x = <. A , D >. /\ ph ) -> ( ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) )
34 33 exlimdvv 
 |-  ( ( x = <. A , D >. /\ ph ) -> ( E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) )
35 34 ex 
 |-  ( x = <. A , D >. -> ( ph -> ( E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) ) )
36 35 impd 
 |-  ( x = <. A , D >. -> ( ( ph /\ E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) )
37 orc 
 |-  ( x = <. B , E >. -> ( x = <. B , E >. \/ x = <. C , F >. ) )
38 37 a1d 
 |-  ( x = <. B , E >. -> ( ( ph /\ E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) )
39 olc 
 |-  ( x = <. C , F >. -> ( x = <. B , E >. \/ x = <. C , F >. ) )
40 39 a1d 
 |-  ( x = <. C , F >. -> ( ( ph /\ E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) ) -> ( x = <. B , E >. \/ x = <. C , F >. ) ) )
41 36 38 40 3jaoi 
 |-  ( ( 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 >. ) ) )
42 14 41 sylbi 
 |-  ( 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 >. ) ) )
43 13 elpr 
 |-  ( x e. { <. B , E >. , <. C , F >. } <-> ( x = <. B , E >. \/ x = <. C , F >. ) )
44 42 43 syl6ibr 
 |-  ( 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 >. } ) )
45 44 expd 
 |-  ( 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 >. } ) ) )
46 45 com12 
 |-  ( 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 >. } ) ) )
47 12 46 sylbid 
 |-  ( ph -> ( x e. T -> ( E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) -> x e. { <. B , E >. , <. C , F >. } ) ) )
48 47 impd 
 |-  ( ph -> ( ( x e. T /\ E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) ) -> x e. { <. B , E >. , <. C , F >. } ) )
49 3mix2 
 |-  ( x = <. B , E >. -> ( x = <. A , D >. \/ x = <. B , E >. \/ x = <. C , F >. ) )
50 3mix3 
 |-  ( x = <. C , F >. -> ( x = <. A , D >. \/ x = <. B , E >. \/ x = <. C , F >. ) )
51 49 50 jaoi 
 |-  ( ( x = <. B , E >. \/ x = <. C , F >. ) -> ( x = <. A , D >. \/ x = <. B , E >. \/ x = <. C , F >. ) )
52 51 adantr 
 |-  ( ( ( x = <. B , E >. \/ x = <. C , F >. ) /\ ph ) -> ( x = <. A , D >. \/ x = <. B , E >. \/ x = <. C , F >. ) )
53 12 14 bitrdi 
 |-  ( ph -> ( x e. T <-> ( x = <. A , D >. \/ x = <. B , E >. \/ x = <. C , F >. ) ) )
54 53 adantl 
 |-  ( ( ( x = <. B , E >. \/ x = <. C , F >. ) /\ ph ) -> ( x e. T <-> ( x = <. A , D >. \/ x = <. B , E >. \/ x = <. C , F >. ) ) )
55 52 54 mpbird 
 |-  ( ( ( x = <. B , E >. \/ x = <. C , F >. ) /\ ph ) -> x e. T )
56 2 elexd 
 |-  ( ph -> B e. _V )
57 4 elexd 
 |-  ( ph -> E e. _V )
58 56 6 57 jca31 
 |-  ( ph -> ( ( B e. _V /\ B =/= A ) /\ E e. _V ) )
59 58 anim2i 
 |-  ( ( x = <. B , E >. /\ ph ) -> ( x = <. B , E >. /\ ( ( B e. _V /\ B =/= A ) /\ E e. _V ) ) )
60 opeq12 
 |-  ( ( a = B /\ b = E ) -> <. a , b >. = <. B , E >. )
61 60 eqeq2d 
 |-  ( ( a = B /\ b = E ) -> ( x = <. a , b >. <-> x = <. B , E >. ) )
62 eleq1 
 |-  ( a = B -> ( a e. _V <-> B e. _V ) )
63 neeq1 
 |-  ( a = B -> ( a =/= A <-> B =/= A ) )
64 62 63 anbi12d 
 |-  ( a = B -> ( ( a e. _V /\ a =/= A ) <-> ( B e. _V /\ B =/= A ) ) )
65 eleq1 
 |-  ( b = E -> ( b e. _V <-> E e. _V ) )
66 64 65 bi2anan9 
 |-  ( ( a = B /\ b = E ) -> ( ( ( a e. _V /\ a =/= A ) /\ b e. _V ) <-> ( ( B e. _V /\ B =/= A ) /\ E e. _V ) ) )
67 61 66 anbi12d 
 |-  ( ( 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 ) ) ) )
68 67 spc2egv 
 |-  ( ( 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 ) ) ) )
69 2 4 68 syl2anc 
 |-  ( 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 ) ) ) )
70 69 adantl 
 |-  ( ( 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 ) ) ) )
71 59 70 mpd 
 |-  ( ( x = <. B , E >. /\ ph ) -> E. a E. b ( x = <. a , b >. /\ ( ( a e. _V /\ a =/= A ) /\ b e. _V ) ) )
72 3 elexd 
 |-  ( ph -> C e. _V )
73 5 elexd 
 |-  ( ph -> F e. _V )
74 72 7 73 jca31 
 |-  ( ph -> ( ( C e. _V /\ C =/= A ) /\ F e. _V ) )
75 74 anim2i 
 |-  ( ( x = <. C , F >. /\ ph ) -> ( x = <. C , F >. /\ ( ( C e. _V /\ C =/= A ) /\ F e. _V ) ) )
76 opeq12 
 |-  ( ( a = C /\ b = F ) -> <. a , b >. = <. C , F >. )
77 76 eqeq2d 
 |-  ( ( a = C /\ b = F ) -> ( x = <. a , b >. <-> x = <. C , F >. ) )
78 eleq1 
 |-  ( a = C -> ( a e. _V <-> C e. _V ) )
79 neeq1 
 |-  ( a = C -> ( a =/= A <-> C =/= A ) )
80 78 79 anbi12d 
 |-  ( a = C -> ( ( a e. _V /\ a =/= A ) <-> ( C e. _V /\ C =/= A ) ) )
81 eleq1 
 |-  ( b = F -> ( b e. _V <-> F e. _V ) )
82 80 81 bi2anan9 
 |-  ( ( a = C /\ b = F ) -> ( ( ( a e. _V /\ a =/= A ) /\ b e. _V ) <-> ( ( C e. _V /\ C =/= A ) /\ F e. _V ) ) )
83 77 82 anbi12d 
 |-  ( ( 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 ) ) ) )
84 83 spc2egv 
 |-  ( ( 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 ) ) ) )
85 3 5 84 syl2anc 
 |-  ( 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 ) ) ) )
86 85 adantl 
 |-  ( ( 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 ) ) ) )
87 75 86 mpd 
 |-  ( ( x = <. C , F >. /\ ph ) -> E. a E. b ( x = <. a , b >. /\ ( ( a e. _V /\ a =/= A ) /\ b e. _V ) ) )
88 71 87 jaoian 
 |-  ( ( ( x = <. B , E >. \/ x = <. C , F >. ) /\ ph ) -> E. a E. b ( x = <. a , b >. /\ ( ( a e. _V /\ a =/= A ) /\ b e. _V ) ) )
89 15 anbi1i 
 |-  ( ( a e. ( _V \ { A } ) /\ b e. _V ) <-> ( ( a e. _V /\ a =/= A ) /\ b e. _V ) )
90 89 anbi2i 
 |-  ( ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) <-> ( x = <. a , b >. /\ ( ( a e. _V /\ a =/= A ) /\ b e. _V ) ) )
91 90 2exbii 
 |-  ( 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 ) ) )
92 88 91 sylibr 
 |-  ( ( ( x = <. B , E >. \/ x = <. C , F >. ) /\ ph ) -> E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) )
93 55 92 jca 
 |-  ( ( ( x = <. B , E >. \/ x = <. C , F >. ) /\ ph ) -> ( x e. T /\ E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) ) )
94 93 ex 
 |-  ( ( x = <. B , E >. \/ x = <. C , F >. ) -> ( ph -> ( x e. T /\ E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) ) ) )
95 43 94 sylbi 
 |-  ( x e. { <. B , E >. , <. C , F >. } -> ( ph -> ( x e. T /\ E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) ) ) )
96 95 com12 
 |-  ( ph -> ( x e. { <. B , E >. , <. C , F >. } -> ( x e. T /\ E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) ) ) )
97 48 96 impbid 
 |-  ( ph -> ( ( x e. T /\ E. a E. b ( x = <. a , b >. /\ ( a e. ( _V \ { A } ) /\ b e. _V ) ) ) <-> x e. { <. B , E >. , <. C , F >. } ) )
98 11 97 syl5bb 
 |-  ( ph -> ( ( x e. T /\ x e. ( ( _V \ { A } ) X. _V ) ) <-> x e. { <. B , E >. , <. C , F >. } ) )
99 9 98 syl5bb 
 |-  ( ph -> ( x e. ( T i^i ( ( _V \ { A } ) X. _V ) ) <-> x e. { <. B , E >. , <. C , F >. } ) )
100 99 eqrdv 
 |-  ( ph -> ( T i^i ( ( _V \ { A } ) X. _V ) ) = { <. B , E >. , <. C , F >. } )
101 8 100 syl5eq 
 |-  ( ph -> ( T |` ( _V \ { A } ) ) = { <. B , E >. , <. C , F >. } )