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