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 𝑃 = ( Base ‘ 𝐺 )
ishpg.i 𝐼 = ( Itv ‘ 𝐺 )
ishpg.l 𝐿 = ( LineG ‘ 𝐺 )
ishpg.o 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
ishpg.g ( 𝜑𝐺 ∈ TarskiG )
ishpg.d ( 𝜑𝐷 ∈ ran 𝐿 )
Assertion ishpg ( 𝜑 → ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( 𝑎 𝑂 𝑐𝑏 𝑂 𝑐 ) } )

Proof

Step Hyp Ref Expression
1 ishpg.p 𝑃 = ( Base ‘ 𝐺 )
2 ishpg.i 𝐼 = ( Itv ‘ 𝐺 )
3 ishpg.l 𝐿 = ( LineG ‘ 𝐺 )
4 ishpg.o 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5 ishpg.g ( 𝜑𝐺 ∈ TarskiG )
6 ishpg.d ( 𝜑𝐷 ∈ ran 𝐿 )
7 elex ( 𝐺 ∈ TarskiG → 𝐺 ∈ V )
8 fveq2 ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) )
9 8 3 eqtr4di ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = 𝐿 )
10 9 rneqd ( 𝑔 = 𝐺 → ran ( LineG ‘ 𝑔 ) = ran 𝐿 )
11 simpl ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → 𝑝 = 𝑃 )
12 11 difeq1d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑝𝑑 ) = ( 𝑃𝑑 ) )
13 12 eleq2d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑎 ∈ ( 𝑝𝑑 ) ↔ 𝑎 ∈ ( 𝑃𝑑 ) ) )
14 12 eleq2d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑐 ∈ ( 𝑝𝑑 ) ↔ 𝑐 ∈ ( 𝑃𝑑 ) ) )
15 13 14 anbi12d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ↔ ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ) )
16 simpr ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
17 16 oveqd ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑎 𝑖 𝑐 ) = ( 𝑎 𝐼 𝑐 ) )
18 17 eleq2d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ↔ 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) )
19 18 rexbidv ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ↔ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) )
20 15 19 anbi12d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ) )
21 12 eleq2d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑏 ∈ ( 𝑝𝑑 ) ↔ 𝑏 ∈ ( 𝑃𝑑 ) ) )
22 21 14 anbi12d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ↔ ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ) )
23 16 oveqd ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑏 𝑖 𝑐 ) = ( 𝑏 𝐼 𝑐 ) )
24 23 eleq2d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ↔ 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) )
25 24 rexbidv ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ↔ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) )
26 22 25 anbi12d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ↔ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) )
27 20 26 anbi12d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) ↔ ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) ) )
28 11 27 rexeqbidv ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( ∃ 𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) ↔ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) ) )
29 1 2 28 sbcie2s ( 𝑔 = 𝐺 → ( [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) ↔ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) ) )
30 29 opabbidv ( 𝑔 = 𝐺 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } )
31 10 30 mpteq12dv ( 𝑔 = 𝐺 → ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } ) = ( 𝑑 ∈ ran 𝐿 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } ) )
32 df-hpg hpG = ( 𝑔 ∈ V ↦ ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ]𝑐𝑝 ( ( ( 𝑎 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝𝑑 ) ∧ 𝑐 ∈ ( 𝑝𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } ) )
33 3 fvexi 𝐿 ∈ V
34 33 rnex ran 𝐿 ∈ V
35 34 mptex ( 𝑑 ∈ ran 𝐿 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } ) ∈ V
36 31 32 35 fvmpt ( 𝐺 ∈ V → ( hpG ‘ 𝐺 ) = ( 𝑑 ∈ ran 𝐿 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } ) )
37 5 7 36 3syl ( 𝜑 → ( hpG ‘ 𝐺 ) = ( 𝑑 ∈ ran 𝐿 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } ) )
38 difeq2 ( 𝑑 = 𝐷 → ( 𝑃𝑑 ) = ( 𝑃𝐷 ) )
39 38 eleq2d ( 𝑑 = 𝐷 → ( 𝑎 ∈ ( 𝑃𝑑 ) ↔ 𝑎 ∈ ( 𝑃𝐷 ) ) )
40 38 eleq2d ( 𝑑 = 𝐷 → ( 𝑐 ∈ ( 𝑃𝑑 ) ↔ 𝑐 ∈ ( 𝑃𝐷 ) ) )
41 39 40 anbi12d ( 𝑑 = 𝐷 → ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ↔ ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ) )
42 rexeq ( 𝑑 = 𝐷 → ( ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ↔ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) )
43 41 42 anbi12d ( 𝑑 = 𝐷 → ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ) )
44 38 eleq2d ( 𝑑 = 𝐷 → ( 𝑏 ∈ ( 𝑃𝑑 ) ↔ 𝑏 ∈ ( 𝑃𝐷 ) ) )
45 44 40 anbi12d ( 𝑑 = 𝐷 → ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ↔ ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ) )
46 rexeq ( 𝑑 = 𝐷 → ( ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ↔ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) )
47 45 46 anbi12d ( 𝑑 = 𝐷 → ( ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ↔ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) )
48 43 47 anbi12d ( 𝑑 = 𝐷 → ( ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) ↔ ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) ) )
49 48 rexbidv ( 𝑑 = 𝐷 → ( ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) ↔ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) ) )
50 49 opabbidv ( 𝑑 = 𝐷 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } )
51 50 adantl ( ( 𝜑𝑑 = 𝐷 ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝑑 ) ∧ 𝑐 ∈ ( 𝑃𝑑 ) ) ∧ ∃ 𝑡𝑑 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } )
52 df-xp ( 𝑃 × 𝑃 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎𝑃𝑏𝑃 ) }
53 1 fvexi 𝑃 ∈ V
54 53 53 xpex ( 𝑃 × 𝑃 ) ∈ V
55 52 54 eqeltrri { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎𝑃𝑏𝑃 ) } ∈ V
56 eldifi ( 𝑎 ∈ ( 𝑃𝐷 ) → 𝑎𝑃 )
57 eldifi ( 𝑏 ∈ ( 𝑃𝐷 ) → 𝑏𝑃 )
58 56 57 anim12i ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) → ( 𝑎𝑃𝑏𝑃 ) )
59 58 ad2ant2r ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ) → ( 𝑎𝑃𝑏𝑃 ) )
60 59 ad2ant2r ( ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) → ( 𝑎𝑃𝑏𝑃 ) )
61 60 rexlimivw ( ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) → ( 𝑎𝑃𝑏𝑃 ) )
62 61 ssopab2i { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } ⊆ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎𝑃𝑏𝑃 ) }
63 55 62 ssexi { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } ∈ V
64 63 a1i ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } ∈ V )
65 37 51 6 64 fvmptd ( 𝜑 → ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) } )
66 vex 𝑎 ∈ V
67 vex 𝑐 ∈ V
68 eleq1w ( 𝑒 = 𝑎 → ( 𝑒 ∈ ( 𝑃𝐷 ) ↔ 𝑎 ∈ ( 𝑃𝐷 ) ) )
69 68 anbi1d ( 𝑒 = 𝑎 → ( ( 𝑒 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ↔ ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ) )
70 oveq1 ( 𝑒 = 𝑎 → ( 𝑒 𝐼 𝑓 ) = ( 𝑎 𝐼 𝑓 ) )
71 70 eleq2d ( 𝑒 = 𝑎 → ( 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ↔ 𝑡 ∈ ( 𝑎 𝐼 𝑓 ) ) )
72 71 rexbidv ( 𝑒 = 𝑎 → ( ∃ 𝑡𝐷 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ↔ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑓 ) ) )
73 69 72 anbi12d ( 𝑒 = 𝑎 → ( ( ( 𝑒 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑓 ) ) ) )
74 eleq1w ( 𝑓 = 𝑐 → ( 𝑓 ∈ ( 𝑃𝐷 ) ↔ 𝑐 ∈ ( 𝑃𝐷 ) ) )
75 74 anbi2d ( 𝑓 = 𝑐 → ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ↔ ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ) )
76 oveq2 ( 𝑓 = 𝑐 → ( 𝑎 𝐼 𝑓 ) = ( 𝑎 𝐼 𝑐 ) )
77 76 eleq2d ( 𝑓 = 𝑐 → ( 𝑡 ∈ ( 𝑎 𝐼 𝑓 ) ↔ 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) )
78 77 rexbidv ( 𝑓 = 𝑐 → ( ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑓 ) ↔ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) )
79 75 78 anbi12d ( 𝑓 = 𝑐 → ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑓 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ) )
80 simpl ( ( 𝑎 = 𝑒𝑏 = 𝑓 ) → 𝑎 = 𝑒 )
81 80 eleq1d ( ( 𝑎 = 𝑒𝑏 = 𝑓 ) → ( 𝑎 ∈ ( 𝑃𝐷 ) ↔ 𝑒 ∈ ( 𝑃𝐷 ) ) )
82 simpr ( ( 𝑎 = 𝑒𝑏 = 𝑓 ) → 𝑏 = 𝑓 )
83 82 eleq1d ( ( 𝑎 = 𝑒𝑏 = 𝑓 ) → ( 𝑏 ∈ ( 𝑃𝐷 ) ↔ 𝑓 ∈ ( 𝑃𝐷 ) ) )
84 81 83 anbi12d ( ( 𝑎 = 𝑒𝑏 = 𝑓 ) → ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ↔ ( 𝑒 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ) )
85 oveq12 ( ( 𝑎 = 𝑒𝑏 = 𝑓 ) → ( 𝑎 𝐼 𝑏 ) = ( 𝑒 𝐼 𝑓 ) )
86 85 eleq2d ( ( 𝑎 = 𝑒𝑏 = 𝑓 ) → ( 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ) )
87 86 rexbidv ( ( 𝑎 = 𝑒𝑏 = 𝑓 ) → ( ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ) )
88 84 87 anbi12d ( ( 𝑎 = 𝑒𝑏 = 𝑓 ) → ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑒 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ) ) )
89 88 cbvopabv { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ) }
90 4 89 eqtri 𝑂 = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ) }
91 66 67 73 79 90 brab ( 𝑎 𝑂 𝑐 ↔ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) )
92 vex 𝑏 ∈ V
93 eleq1w ( 𝑒 = 𝑏 → ( 𝑒 ∈ ( 𝑃𝐷 ) ↔ 𝑏 ∈ ( 𝑃𝐷 ) ) )
94 93 anbi1d ( 𝑒 = 𝑏 → ( ( 𝑒 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ↔ ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ) )
95 oveq1 ( 𝑒 = 𝑏 → ( 𝑒 𝐼 𝑓 ) = ( 𝑏 𝐼 𝑓 ) )
96 95 eleq2d ( 𝑒 = 𝑏 → ( 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ↔ 𝑡 ∈ ( 𝑏 𝐼 𝑓 ) ) )
97 96 rexbidv ( 𝑒 = 𝑏 → ( ∃ 𝑡𝐷 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ↔ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑓 ) ) )
98 94 97 anbi12d ( 𝑒 = 𝑏 → ( ( ( 𝑒 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑒 𝐼 𝑓 ) ) ↔ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑓 ) ) ) )
99 74 anbi2d ( 𝑓 = 𝑐 → ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ↔ ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ) )
100 oveq2 ( 𝑓 = 𝑐 → ( 𝑏 𝐼 𝑓 ) = ( 𝑏 𝐼 𝑐 ) )
101 100 eleq2d ( 𝑓 = 𝑐 → ( 𝑡 ∈ ( 𝑏 𝐼 𝑓 ) ↔ 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) )
102 101 rexbidv ( 𝑓 = 𝑐 → ( ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑓 ) ↔ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) )
103 99 102 anbi12d ( 𝑓 = 𝑐 → ( ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑓 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑓 ) ) ↔ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) )
104 92 67 98 103 90 brab ( 𝑏 𝑂 𝑐 ↔ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) )
105 91 104 anbi12i ( ( 𝑎 𝑂 𝑐𝑏 𝑂 𝑐 ) ↔ ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) )
106 105 rexbii ( ∃ 𝑐𝑃 ( 𝑎 𝑂 𝑐𝑏 𝑂 𝑐 ) ↔ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) )
107 106 opabbii { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( 𝑎 𝑂 𝑐𝑏 𝑂 𝑐 ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑃𝐷 ) ∧ 𝑐 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑏 𝐼 𝑐 ) ) ) }
108 65 107 eqtr4di ( 𝜑 → ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐𝑃 ( 𝑎 𝑂 𝑐𝑏 𝑂 𝑐 ) } )