Metamath Proof Explorer

Theorem plngcplem

Description: Lemma for plngcp . (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
plngcp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
plngcp.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
plngcp.s ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝐴 𝐸 𝑅 ) ∖ 𝐴 ) )
plngcplem.1 ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
Assertion plngcplem ( 𝜑 → ( 𝐴 𝐸 𝑅 ) = ( 𝐴 𝐸 𝑆 ) )

Proof

Step Hyp Ref Expression
1 plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
5 plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 plngcp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7 plngcp.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
8 plngcp.s ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝐴 𝐸 𝑅 ) ∖ 𝐴 ) )
9 plngcplem.1 ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
10 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑆 𝑂 𝑅 ) → 𝐺 ∈ TarskiG )
11 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑆 𝑂 𝑅 ) → 𝐴 ∈ ran 𝐿 )
12 7 eldifad ⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑆 𝑂 𝑅 ) → 𝑅 ∈ 𝑃 )
14 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑆 𝑂 𝑅 ) → 𝑥 ∈ 𝑃 )
15 8 eldifad ⊢ ( 𝜑 → 𝑆 ∈ ( 𝐴 𝐸 𝑅 ) )
16 1 2 3 4 5 6 7 15 plngssp ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
17 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑆 𝑂 𝑅 ) → 𝑆 ∈ 𝑃 )
18 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
19 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑆 𝑂 𝑅 ) → 𝑆 𝑂 𝑅 )
20 1 18 2 9 3 11 10 17 13 19 oppcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑆 𝑂 𝑅 ) → 𝑅 𝑂 𝑆 )
21 1 2 3 9 10 11 13 14 17 20 lnopp2hpgb ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑆 𝑂 𝑅 ) → ( 𝑥 𝑂 𝑆 ↔ 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) )
22 21 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) → ( 𝑥 𝑂 𝑆 ↔ 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) )
23 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝐺 ∈ TarskiG )
24 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝐴 ∈ ran 𝐿 )
25 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝑅 ∈ 𝑃 )
26 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝑥 ∈ 𝑃 )
27 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 )
28 1 2 3 23 24 25 9 26 27 hpgcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 )
29 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝐺 ∈ TarskiG )
30 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝐴 ∈ ran 𝐿 )
31 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑥 ∈ 𝑃 )
32 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑅 ∈ 𝑃 )
33 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 )
34 1 2 3 29 30 31 9 32 33 hpgcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 )
35 28 34 impbida ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) → ( 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ↔ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) )
36 22 35 bitr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) → ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ↔ 𝑥 𝑂 𝑆 ) )
37 1 2 3 9 10 11 17 14 13 19 lnopp2hpgb ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑆 𝑂 𝑅 ) → ( 𝑥 𝑂 𝑅 ↔ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) )
38 37 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) → ( 𝑥 𝑂 𝑅 ↔ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) )
39 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝐺 ∈ TarskiG )
40 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝐴 ∈ ran 𝐿 )
41 16 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝑆 ∈ 𝑃 )
42 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝑥 ∈ 𝑃 )
43 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 )
44 1 2 3 39 40 41 9 42 43 hpgcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ) → 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 )
45 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝐺 ∈ TarskiG )
46 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝐴 ∈ ran 𝐿 )
47 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝑥 ∈ 𝑃 )
48 16 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝑆 ∈ 𝑃 )
49 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 )
50 1 2 3 45 46 47 9 48 49 hpgcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 )
51 44 50 impbida ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) → ( 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑥 ↔ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) )
52 38 51 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) → ( 𝑥 𝑂 𝑅 ↔ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) )
53 36 52 orbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) → ( ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑥 𝑂 𝑅 ) ↔ ( 𝑥 𝑂 𝑆 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) ) )
54 orcom ⊢ ( ( 𝑥 𝑂 𝑆 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) ↔ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ 𝑥 𝑂 𝑆 ) )
55 53 54 bitrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 𝑂 𝑅 ) → ( ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑥 𝑂 𝑅 ) ↔ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ 𝑥 𝑂 𝑆 ) ) )
56 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝐺 ∈ TarskiG )
57 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝐴 ∈ ran 𝐿 )
58 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑥 ∈ 𝑃 )
59 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑅 ∈ 𝑃 )
60 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 )
61 16 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑆 ∈ 𝑃 )
62 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 )
63 1 2 3 56 57 61 9 59 62 hpgcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 )
64 1 2 3 56 57 58 9 59 60 61 63 hpgtr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 )
65 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝐺 ∈ TarskiG )
66 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝐴 ∈ ran 𝐿 )
67 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝑥 ∈ 𝑃 )
68 16 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝑆 ∈ 𝑃 )
69 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 )
70 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝑅 ∈ 𝑃 )
71 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 )
72 1 2 3 65 66 67 9 68 69 70 71 hpgtr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) → 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 )
73 64 72 impbida ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ↔ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) )
74 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝐴 ∈ ran 𝐿 )
75 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝐺 ∈ TarskiG )
76 16 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝑆 ∈ 𝑃 )
77 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝑥 ∈ 𝑃 )
78 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝑅 ∈ 𝑃 )
79 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 )
80 1 2 3 75 74 76 9 78 79 hpgcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 )
81 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝑥 𝑂 𝑅 )
82 1 18 2 9 3 74 75 77 78 81 oppcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝑅 𝑂 𝑥 )
83 1 2 3 9 75 74 78 76 77 82 lnopp2hpgb ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → ( 𝑆 𝑂 𝑥 ↔ 𝑅 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ) )
84 80 83 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝑆 𝑂 𝑥 )
85 1 18 2 9 3 74 75 76 77 84 oppcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑅 ) → 𝑥 𝑂 𝑆 )
86 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → 𝐴 ∈ ran 𝐿 )
87 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → 𝐺 ∈ TarskiG )
88 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → 𝑅 ∈ 𝑃 )
89 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → 𝑥 ∈ 𝑃 )
90 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 )
91 16 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → 𝑆 ∈ 𝑃 )
92 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → 𝑥 𝑂 𝑆 )
93 1 18 2 9 3 86 87 89 91 92 oppcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → 𝑆 𝑂 𝑥 )
94 1 2 3 9 87 86 91 88 89 93 lnopp2hpgb ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → ( 𝑅 𝑂 𝑥 ↔ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) )
95 90 94 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → 𝑅 𝑂 𝑥 )
96 1 18 2 9 3 86 87 88 89 95 oppcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) ∧ 𝑥 𝑂 𝑆 ) → 𝑥 𝑂 𝑅 )
97 85 96 impbida ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → ( 𝑥 𝑂 𝑅 ↔ 𝑥 𝑂 𝑆 ) )
98 73 97 orbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) → ( ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑥 𝑂 𝑅 ) ↔ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ 𝑥 𝑂 𝑆 ) ) )
99 eleq1 ⊢ ( 𝑦 = 𝑆 → ( 𝑦 ∈ 𝐴 ↔ 𝑆 ∈ 𝐴 ) )
100 breq1 ⊢ ( 𝑦 = 𝑆 → ( 𝑦 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ↔ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) )
101 oveq1 ⊢ ( 𝑦 = 𝑆 → ( 𝑦 𝐼 𝑅 ) = ( 𝑆 𝐼 𝑅 ) )
102 101 eleq2d ⊢ ( 𝑦 = 𝑆 → ( 𝑡 ∈ ( 𝑦 𝐼 𝑅 ) ↔ 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) )
103 102 rexbidv ⊢ ( 𝑦 = 𝑆 → ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑦 𝐼 𝑅 ) ↔ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) )
104 99 100 103 3orbi123d ⊢ ( 𝑦 = 𝑆 → ( ( 𝑦 ∈ 𝐴 ∨ 𝑦 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑦 𝐼 𝑅 ) ) ↔ ( 𝑆 ∈ 𝐴 ∨ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) ) )
105 1 2 3 4 5 6 7 plngval ⊢ ( 𝜑 → ( 𝐴 𝐸 𝑅 ) = { 𝑦 ∈ 𝑃 ∣ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑦 𝐼 𝑅 ) ) } )
106 15 105 eleqtrd ⊢ ( 𝜑 → 𝑆 ∈ { 𝑦 ∈ 𝑃 ∣ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑦 𝐼 𝑅 ) ) } )
107 104 106 elrabrd ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐴 ∨ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) )
108 3orass ⊢ ( ( 𝑆 ∈ 𝐴 ∨ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) ↔ ( 𝑆 ∈ 𝐴 ∨ ( 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) ) )
109 107 108 sylib ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐴 ∨ ( 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) ) )
110 8 eldifbd ⊢ ( 𝜑 → ¬ 𝑆 ∈ 𝐴 )
111 109 110 orcnd ⊢ ( 𝜑 → ( 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) )
112 1 18 2 9 16 12 islnopp ⊢ ( 𝜑 → ( 𝑆 𝑂 𝑅 ↔ ( ( ¬ 𝑆 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) ) )
113 7 eldifbd ⊢ ( 𝜑 → ¬ 𝑅 ∈ 𝐴 )
114 110 113 jca ⊢ ( 𝜑 → ( ¬ 𝑆 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴 ) )
115 114 biantrurd ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ↔ ( ( ¬ 𝑆 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) ) )
116 112 115 bitr4d ⊢ ( 𝜑 → ( 𝑆 𝑂 𝑅 ↔ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) )
117 116 orbi2d ⊢ ( 𝜑 → ( ( 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑆 𝑂 𝑅 ) ↔ ( 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑆 𝐼 𝑅 ) ) ) )
118 111 117 mpbird ⊢ ( 𝜑 → ( 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑆 𝑂 𝑅 ) )
119 118 orcomd ⊢ ( 𝜑 → ( 𝑆 𝑂 𝑅 ∨ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) )
120 119 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑆 𝑂 𝑅 ∨ 𝑆 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) )
121 55 98 120 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑥 𝑂 𝑅 ) ↔ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ 𝑥 𝑂 𝑆 ) ) )
122 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
123 113 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ¬ 𝑅 ∈ 𝐴 )
124 122 123 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴 ) )
125 124 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ↔ ( ( ¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ) )
126 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝑥 ∈ 𝑃 )
127 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝑅 ∈ 𝑃 )
128 1 18 2 9 126 127 islnopp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝑥 𝑂 𝑅 ↔ ( ( ¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ) )
129 128 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑂 𝑅 ↔ ( ( ¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ) )
130 125 129 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ↔ 𝑥 𝑂 𝑅 ) )
131 130 orbi2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ↔ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ 𝑥 𝑂 𝑅 ) ) )
132 110 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ¬ 𝑆 ∈ 𝐴 )
133 122 132 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑆 ∈ 𝐴 ) )
134 133 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ↔ ( ( ¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑆 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ) )
135 16 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝑆 ∈ 𝑃 )
136 1 18 2 9 126 135 islnopp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝑥 𝑂 𝑆 ↔ ( ( ¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑆 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ) )
137 136 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑂 𝑆 ↔ ( ( ¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑆 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ) )
138 134 137 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ↔ 𝑥 𝑂 𝑆 ) )
139 138 orbi2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ↔ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ 𝑥 𝑂 𝑆 ) ) )
140 121 131 139 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ↔ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ) )
141 140 pm5.74da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ) ↔ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ) ) )
142 3orass ⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ) )
143 df-or ⊢ ( ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ) ↔ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ) )
144 142 143 bitri ⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ↔ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ) )
145 3orass ⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ) )
146 df-or ⊢ ( ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ) ↔ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ) )
147 145 146 bitri ⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ↔ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ) )
148 141 144 147 3bitr4g ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) ) )
149 148 rabbidva ⊢ ( 𝜑 → { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) } )
150 1 2 3 4 5 6 7 plngval ⊢ ( 𝜑 → ( 𝐴 𝐸 𝑅 ) = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } )
151 16 110 eldifd ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑃 ∖ 𝐴 ) )
152 1 2 3 4 5 6 151 plngval ⊢ ( 𝜑 → ( 𝐴 𝐸 𝑆 ) = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑆 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑆 ) ) } )
153 149 150 152 3eqtr4d ⊢ ( 𝜑 → ( 𝐴 𝐸 𝑅 ) = ( 𝐴 𝐸 𝑆 ) )