Metamath Proof Explorer

Theorem inagcgratrgn

Description: In-angle transport, non-collinear case: unfold isinag , eliminate its segment-point existential, and dispatch on the disjunct it carries -- x = E to inagcgrabtwn , x ( KE ) W to inagcgratrgncol . (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses inagcgratrgncol.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
inagcgratrgncol.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
inagcgratrgncol.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
inagcgratrgncol.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
inagcgratrgncol.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
inagcgratrgncol.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
inagcgratrgncol.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
inagcgratrgncol.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
inagcgratrgncol.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
inagcgratrgncol.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
inagcgratrgncol.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
inagcgratrgncol.cgb ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
inagcgratrgn.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
inagcgratrgn.in ⊢ ( 𝜑 → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
inagcgratrgn.1 ⊢ ( 𝜑 → ¬ ( 𝑊 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
Assertion inagcgratrgn ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )

Proof

Step Hyp Ref Expression
1 inagcgratrgncol.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 inagcgratrgncol.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 inagcgratrgncol.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 inagcgratrgncol.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 inagcgratrgncol.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
6 inagcgratrgncol.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
7 inagcgratrgncol.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
8 inagcgratrgncol.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
9 inagcgratrgncol.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 inagcgratrgncol.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
11 inagcgratrgncol.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
12 inagcgratrgncol.cgb ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
13 inagcgratrgn.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
14 inagcgratrgn.in ⊢ ( 𝜑 → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
15 inagcgratrgn.1 ⊢ ( 𝜑 → ¬ ( 𝑊 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
16 1 2 3 8 5 6 7 4 isinag ⊢ ( 𝜑 → ( 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ 𝑊 ≠ 𝐸 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) )
17 14 16 mpbid ⊢ ( 𝜑 → ( ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ 𝑊 ≠ 𝐸 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) )
18 17 simprd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) )
19 simpl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝜑 )
20 19 4 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝐺 ∈ TarskiG )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝐺 ∈ TarskiG )
22 19 5 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝐷 ∈ 𝑃 )
23 22 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝐷 ∈ 𝑃 )
24 19 6 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝐸 ∈ 𝑃 )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝐸 ∈ 𝑃 )
26 19 7 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝐹 ∈ 𝑃 )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝐹 ∈ 𝑃 )
28 19 8 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝑊 ∈ 𝑃 )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝑊 ∈ 𝑃 )
30 19 9 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝑋 ∈ 𝑃 )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝑋 ∈ 𝑃 )
32 19 10 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝑌 ∈ 𝑃 )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝑌 ∈ 𝑃 )
34 19 11 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝑍 ∈ 𝑃 )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝑍 ∈ 𝑃 )
36 19 12 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
38 simpr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) )
39 38 simprd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) )
40 39 simpld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) )
41 40 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) )
42 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝑥 = 𝐸 )
43 42 eleq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ↔ 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ) )
44 41 43 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
45 19 15 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → ¬ ( 𝑊 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → ¬ ( 𝑊 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
47 1 2 3 13 21 23 25 27 29 31 33 35 37 44 46 inagcgrabtwn ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 = 𝐸 ) → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
48 20 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐺 ∈ TarskiG )
49 22 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐷 ∈ 𝑃 )
50 24 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐸 ∈ 𝑃 )
51 26 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐹 ∈ 𝑃 )
52 28 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑊 ∈ 𝑃 )
53 30 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑋 ∈ 𝑃 )
54 32 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑌 ∈ 𝑃 )
55 34 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑍 ∈ 𝑃 )
56 36 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
57 38 simpld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝑥 ∈ 𝑃 )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑥 ∈ 𝑃 )
59 1 2 3 8 5 6 7 4 14 inagne1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
60 19 59 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → 𝐷 ≠ 𝐸 )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐷 ≠ 𝐸 )
62 40 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) )
63 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 )
64 1 2 3 48 49 50 51 52 53 54 55 56 58 61 62 63 inagcgratrgncol ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
65 39 simprd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) )
66 47 64 65 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
67 18 66 rexlimddv ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )