Metamath Proof Explorer

Theorem ishpg

Description: Value of the half-plane relation for a given line D . (Contributed by Thierry Arnoux, 4-Mar-2020)

Ref Expression
Hypotheses ishpg.p 
|- P = ( Base ` G )
ishpg.i 
|- I = ( Itv ` G )
ishpg.l 
|- L = ( LineG ` G )
ishpg.o 
|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
ishpg.g 
|- ( ph -> G e. TarskiG )
ishpg.d 
|- ( ph -> D e. ran L )
Assertion ishpg 
|- ( ph -> ( ( hpG ` G ) ` D ) = { <. a , b >. | E. c e. P ( a O c /\ b O c ) } )

Proof

Step Hyp Ref Expression
1 ishpg.p 
 |-  P = ( Base ` G )
2 ishpg.i 
 |-  I = ( Itv ` G )
3 ishpg.l 
 |-  L = ( LineG ` G )
4 ishpg.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5 ishpg.g 
 |-  ( ph -> G e. TarskiG )
6 ishpg.d 
 |-  ( ph -> D e. ran L )
7 elex 
 |-  ( G e. TarskiG -> G e. _V )
8 fveq2 
 |-  ( g = G -> ( LineG ` g ) = ( LineG ` G ) )
9 8 3 eqtr4di 
 |-  ( g = G -> ( LineG ` g ) = L )
10 9 rneqd 
 |-  ( g = G -> ran ( LineG ` g ) = ran L )
11 simpl 
 |-  ( ( p = P /\ i = I ) -> p = P )
12 11 eqcomd 
 |-  ( ( p = P /\ i = I ) -> P = p )
13 12 difeq1d 
 |-  ( ( p = P /\ i = I ) -> ( P \ d ) = ( p \ d ) )
14 13 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( a e. ( P \ d ) <-> a e. ( p \ d ) ) )
15 13 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( c e. ( P \ d ) <-> c e. ( p \ d ) ) )
16 14 15 anbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) <-> ( a e. ( p \ d ) /\ c e. ( p \ d ) ) ) )
17 simpr 
 |-  ( ( p = P /\ i = I ) -> i = I )
18 17 eqcomd 
 |-  ( ( p = P /\ i = I ) -> I = i )
19 18 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( a I c ) = ( a i c ) )
20 19 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( t e. ( a I c ) <-> t e. ( a i c ) ) )
21 20 rexbidv 
 |-  ( ( p = P /\ i = I ) -> ( E. t e. d t e. ( a I c ) <-> E. t e. d t e. ( a i c ) ) )
22 16 21 anbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) <-> ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) ) )
23 13 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( b e. ( P \ d ) <-> b e. ( p \ d ) ) )
24 23 15 anbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) <-> ( b e. ( p \ d ) /\ c e. ( p \ d ) ) ) )
25 18 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( b I c ) = ( b i c ) )
26 25 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( t e. ( b I c ) <-> t e. ( b i c ) ) )
27 26 rexbidv 
 |-  ( ( p = P /\ i = I ) -> ( E. t e. d t e. ( b I c ) <-> E. t e. d t e. ( b i c ) ) )
28 24 27 anbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) <-> ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) )
29 22 28 anbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) <-> ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) ) )
30 12 29 rexeqbidv 
 |-  ( ( p = P /\ i = I ) -> ( E. c e. P ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) <-> E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) ) )
31 1 2 30 sbcie2s 
 |-  ( g = G -> ( [. ( Base ` g ) / p ]. [. ( Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) <-> E. c e. P ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) ) )
32 31 opabbidv 
 |-  ( g = G -> { <. a , b >. | [. ( Base ` g ) / p ]. [. ( Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) } = { <. a , b >. | E. c e. P ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) } )
33 10 32 mpteq12dv 
 |-  ( g = G -> ( d e. ran ( LineG ` g ) |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. ( Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) } ) = ( d e. ran L |-> { <. a , b >. | E. c e. P ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) } ) )
34 df-hpg 
 |-  hpG = ( g e. _V |-> ( d e. ran ( LineG ` g ) |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. ( Itv ` g ) / i ]. E. c e. p ( ( ( a e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( a i c ) ) /\ ( ( b e. ( p \ d ) /\ c e. ( p \ d ) ) /\ E. t e. d t e. ( b i c ) ) ) } ) )
35 3 fvexi 
 |-  L e. _V
36 35 rnex 
 |-  ran L e. _V
37 36 mptex 
 |-  ( d e. ran L |-> { <. a , b >. | E. c e. P ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) } ) e. _V
38 33 34 37 fvmpt 
 |-  ( G e. _V -> ( hpG ` G ) = ( d e. ran L |-> { <. a , b >. | E. c e. P ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) } ) )
39 5 7 38 3syl 
 |-  ( ph -> ( hpG ` G ) = ( d e. ran L |-> { <. a , b >. | E. c e. P ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) } ) )
40 difeq2 
 |-  ( d = D -> ( P \ d ) = ( P \ D ) )
41 40 eleq2d 
 |-  ( d = D -> ( a e. ( P \ d ) <-> a e. ( P \ D ) ) )
42 40 eleq2d 
 |-  ( d = D -> ( c e. ( P \ d ) <-> c e. ( P \ D ) ) )
43 41 42 anbi12d 
 |-  ( d = D -> ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) <-> ( a e. ( P \ D ) /\ c e. ( P \ D ) ) ) )
44 rexeq 
 |-  ( d = D -> ( E. t e. d t e. ( a I c ) <-> E. t e. D t e. ( a I c ) ) )
45 43 44 anbi12d 
 |-  ( d = D -> ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) <-> ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) ) )
46 40 eleq2d 
 |-  ( d = D -> ( b e. ( P \ d ) <-> b e. ( P \ D ) ) )
47 46 42 anbi12d 
 |-  ( d = D -> ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) <-> ( b e. ( P \ D ) /\ c e. ( P \ D ) ) ) )
48 rexeq 
 |-  ( d = D -> ( E. t e. d t e. ( b I c ) <-> E. t e. D t e. ( b I c ) ) )
49 47 48 anbi12d 
 |-  ( d = D -> ( ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) <-> ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) )
50 45 49 anbi12d 
 |-  ( d = D -> ( ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) <-> ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) ) )
51 50 rexbidv 
 |-  ( d = D -> ( E. c e. P ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) <-> E. c e. P ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) ) )
52 51 opabbidv 
 |-  ( d = D -> { <. a , b >. | E. c e. P ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) } = { <. a , b >. | E. c e. P ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) } )
53 52 adantl 
 |-  ( ( ph /\ d = D ) -> { <. a , b >. | E. c e. P ( ( ( a e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( a I c ) ) /\ ( ( b e. ( P \ d ) /\ c e. ( P \ d ) ) /\ E. t e. d t e. ( b I c ) ) ) } = { <. a , b >. | E. c e. P ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) } )
54 df-xp 
 |-  ( P X. P ) = { <. a , b >. | ( a e. P /\ b e. P ) }
55 1 fvexi 
 |-  P e. _V
56 55 55 xpex 
 |-  ( P X. P ) e. _V
57 54 56 eqeltrri 
 |-  { <. a , b >. | ( a e. P /\ b e. P ) } e. _V
58 eldifi 
 |-  ( a e. ( P \ D ) -> a e. P )
59 eldifi 
 |-  ( b e. ( P \ D ) -> b e. P )
60 58 59 anim12i 
 |-  ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) -> ( a e. P /\ b e. P ) )
61 60 ad2ant2r 
 |-  ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ ( b e. ( P \ D ) /\ c e. ( P \ D ) ) ) -> ( a e. P /\ b e. P ) )
62 61 ad2ant2r 
 |-  ( ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) -> ( a e. P /\ b e. P ) )
63 62 rexlimivw 
 |-  ( E. c e. P ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) -> ( a e. P /\ b e. P ) )
64 63 ssopab2i 
 |-  { <. a , b >. | E. c e. P ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) } C_ { <. a , b >. | ( a e. P /\ b e. P ) }
65 57 64 ssexi 
 |-  { <. a , b >. | E. c e. P ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) } e. _V
66 65 a1i 
 |-  ( ph -> { <. a , b >. | E. c e. P ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) } e. _V )
67 39 53 6 66 fvmptd 
 |-  ( ph -> ( ( hpG ` G ) ` D ) = { <. a , b >. | E. c e. P ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) } )
68 vex 
 |-  a e. _V
69 vex 
 |-  c e. _V
70 eleq1w 
 |-  ( e = a -> ( e e. ( P \ D ) <-> a e. ( P \ D ) ) )
71 70 anbi1d 
 |-  ( e = a -> ( ( e e. ( P \ D ) /\ f e. ( P \ D ) ) <-> ( a e. ( P \ D ) /\ f e. ( P \ D ) ) ) )
72 oveq1 
 |-  ( e = a -> ( e I f ) = ( a I f ) )
73 72 eleq2d 
 |-  ( e = a -> ( t e. ( e I f ) <-> t e. ( a I f ) ) )
74 73 rexbidv 
 |-  ( e = a -> ( E. t e. D t e. ( e I f ) <-> E. t e. D t e. ( a I f ) ) )
75 71 74 anbi12d 
 |-  ( e = a -> ( ( ( e e. ( P \ D ) /\ f e. ( P \ D ) ) /\ E. t e. D t e. ( e I f ) ) <-> ( ( a e. ( P \ D ) /\ f e. ( P \ D ) ) /\ E. t e. D t e. ( a I f ) ) ) )
76 eleq1w 
 |-  ( f = c -> ( f e. ( P \ D ) <-> c e. ( P \ D ) ) )
77 76 anbi2d 
 |-  ( f = c -> ( ( a e. ( P \ D ) /\ f e. ( P \ D ) ) <-> ( a e. ( P \ D ) /\ c e. ( P \ D ) ) ) )
78 oveq2 
 |-  ( f = c -> ( a I f ) = ( a I c ) )
79 78 eleq2d 
 |-  ( f = c -> ( t e. ( a I f ) <-> t e. ( a I c ) ) )
80 79 rexbidv 
 |-  ( f = c -> ( E. t e. D t e. ( a I f ) <-> E. t e. D t e. ( a I c ) ) )
81 77 80 anbi12d 
 |-  ( f = c -> ( ( ( a e. ( P \ D ) /\ f e. ( P \ D ) ) /\ E. t e. D t e. ( a I f ) ) <-> ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) ) )
82 simpl 
 |-  ( ( a = e /\ b = f ) -> a = e )
83 82 eleq1d 
 |-  ( ( a = e /\ b = f ) -> ( a e. ( P \ D ) <-> e e. ( P \ D ) ) )
84 simpr 
 |-  ( ( a = e /\ b = f ) -> b = f )
85 84 eleq1d 
 |-  ( ( a = e /\ b = f ) -> ( b e. ( P \ D ) <-> f e. ( P \ D ) ) )
86 83 85 anbi12d 
 |-  ( ( a = e /\ b = f ) -> ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) <-> ( e e. ( P \ D ) /\ f e. ( P \ D ) ) ) )
87 oveq12 
 |-  ( ( a = e /\ b = f ) -> ( a I b ) = ( e I f ) )
88 87 eleq2d 
 |-  ( ( a = e /\ b = f ) -> ( t e. ( a I b ) <-> t e. ( e I f ) ) )
89 88 rexbidv 
 |-  ( ( a = e /\ b = f ) -> ( E. t e. D t e. ( a I b ) <-> E. t e. D t e. ( e I f ) ) )
90 86 89 anbi12d 
 |-  ( ( a = e /\ b = f ) -> ( ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) <-> ( ( e e. ( P \ D ) /\ f e. ( P \ D ) ) /\ E. t e. D t e. ( e I f ) ) ) )
91 90 cbvopabv 
 |-  { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) } = { <. e , f >. | ( ( e e. ( P \ D ) /\ f e. ( P \ D ) ) /\ E. t e. D t e. ( e I f ) ) }
92 4 91 eqtri 
 |-  O = { <. e , f >. | ( ( e e. ( P \ D ) /\ f e. ( P \ D ) ) /\ E. t e. D t e. ( e I f ) ) }
93 68 69 75 81 92 brab 
 |-  ( a O c <-> ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) )
94 vex 
 |-  b e. _V
95 eleq1w 
 |-  ( e = b -> ( e e. ( P \ D ) <-> b e. ( P \ D ) ) )
96 95 anbi1d 
 |-  ( e = b -> ( ( e e. ( P \ D ) /\ f e. ( P \ D ) ) <-> ( b e. ( P \ D ) /\ f e. ( P \ D ) ) ) )
97 oveq1 
 |-  ( e = b -> ( e I f ) = ( b I f ) )
98 97 eleq2d 
 |-  ( e = b -> ( t e. ( e I f ) <-> t e. ( b I f ) ) )
99 98 rexbidv 
 |-  ( e = b -> ( E. t e. D t e. ( e I f ) <-> E. t e. D t e. ( b I f ) ) )
100 96 99 anbi12d 
 |-  ( e = b -> ( ( ( e e. ( P \ D ) /\ f e. ( P \ D ) ) /\ E. t e. D t e. ( e I f ) ) <-> ( ( b e. ( P \ D ) /\ f e. ( P \ D ) ) /\ E. t e. D t e. ( b I f ) ) ) )
101 76 anbi2d 
 |-  ( f = c -> ( ( b e. ( P \ D ) /\ f e. ( P \ D ) ) <-> ( b e. ( P \ D ) /\ c e. ( P \ D ) ) ) )
102 oveq2 
 |-  ( f = c -> ( b I f ) = ( b I c ) )
103 102 eleq2d 
 |-  ( f = c -> ( t e. ( b I f ) <-> t e. ( b I c ) ) )
104 103 rexbidv 
 |-  ( f = c -> ( E. t e. D t e. ( b I f ) <-> E. t e. D t e. ( b I c ) ) )
105 101 104 anbi12d 
 |-  ( f = c -> ( ( ( b e. ( P \ D ) /\ f e. ( P \ D ) ) /\ E. t e. D t e. ( b I f ) ) <-> ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) )
106 94 69 100 105 92 brab 
 |-  ( b O c <-> ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) )
107 93 106 anbi12i 
 |-  ( ( a O c /\ b O c ) <-> ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) )
108 107 rexbii 
 |-  ( E. c e. P ( a O c /\ b O c ) <-> E. c e. P ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) )
109 108 opabbii 
 |-  { <. a , b >. | E. c e. P ( a O c /\ b O c ) } = { <. a , b >. | E. c e. P ( ( ( a e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( a I c ) ) /\ ( ( b e. ( P \ D ) /\ c e. ( P \ D ) ) /\ E. t e. D t e. ( b I c ) ) ) }
110 67 109 eqtr4di 
 |-  ( ph -> ( ( hpG ` G ) ` D ) = { <. a , b >. | E. c e. P ( a O c /\ b O c ) } )