Metamath Proof Explorer

Theorem inagbtwn

Description: A flat sub-angle forces the containing angle flat: if W is inside angle <" D E F "> and E lies between D and W , then E lies between D and F . This is GeoCoq bet__in__angle__bet. Proved by unfolding isinag and following its segment point. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses inagbtwn.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
inagbtwn.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
inagbtwn.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
inagbtwn.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
inagbtwn.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
inagbtwn.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
inagbtwn.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
inagbtwn.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
inagbtwn.in ⊢ ( 𝜑 → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
inagbtwn.1 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) )
Assertion inagbtwn ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )

Proof

Step Hyp Ref Expression
1 inagbtwn.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 inagbtwn.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 inagbtwn.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 inagbtwn.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 inagbtwn.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
6 inagbtwn.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
7 inagbtwn.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
8 inagbtwn.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
9 inagbtwn.in ⊢ ( 𝜑 → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
10 inagbtwn.1 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) )
11 simpl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 = 𝐸 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) )
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) )
13 12 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) )
14 11 13 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 = 𝐸 ) → 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) )
15 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 = 𝐸 ) → 𝑥 = 𝐸 )
16 15 eleq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 = 𝐸 ) → ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ↔ 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) ) )
17 14 16 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 = 𝐸 ) → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
18 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
19 simpl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) )
20 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → 𝜑 )
21 20 4 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → 𝐺 ∈ TarskiG )
22 19 21 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐺 ∈ TarskiG )
23 20 5 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → 𝐷 ∈ 𝑃 )
24 19 23 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐷 ∈ 𝑃 )
25 20 6 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → 𝐸 ∈ 𝑃 )
26 19 25 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐸 ∈ 𝑃 )
27 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → 𝑥 ∈ 𝑃 )
28 19 27 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑥 ∈ 𝑃 )
29 20 7 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → 𝐹 ∈ 𝑃 )
30 19 29 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐹 ∈ 𝑃 )
31 simpl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) )
32 31 22 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ) → 𝐺 ∈ TarskiG )
33 31 28 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ) → 𝑥 ∈ 𝑃 )
34 31 26 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ) → 𝐸 ∈ 𝑃 )
35 31 24 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ) → 𝐷 ∈ 𝑃 )
36 20 8 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → 𝑊 ∈ 𝑃 )
37 19 36 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑊 ∈ 𝑃 )
38 31 37 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ) → 𝑊 ∈ 𝑃 )
39 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ) → 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) )
40 20 10 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) )
41 19 40 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) )
42 31 41 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) )
43 1 18 2 32 33 34 35 38 39 42 tgbtwnintr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ) → 𝐸 ∈ ( 𝑥 𝐼 𝐷 ) )
44 1 18 2 32 33 34 35 43 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝑥 ) )
45 simpl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) )
46 45 22 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) → 𝐺 ∈ TarskiG )
47 45 24 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) → 𝐷 ∈ 𝑃 )
48 45 26 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) → 𝐸 ∈ 𝑃 )
49 45 37 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) → 𝑊 ∈ 𝑃 )
50 45 28 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) → 𝑥 ∈ 𝑃 )
51 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 )
52 1 2 3 28 37 26 22 ishlg ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ↔ ( 𝑥 ≠ 𝐸 ∧ 𝑊 ≠ 𝐸 ∧ ( 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ∨ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) ) ) )
53 51 52 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → ( 𝑥 ≠ 𝐸 ∧ 𝑊 ≠ 𝐸 ∧ ( 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ∨ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) ) )
54 53 simp2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑊 ≠ 𝐸 )
55 54 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐸 ≠ 𝑊 )
56 45 55 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) → 𝐸 ≠ 𝑊 )
57 45 41 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) )
58 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) → 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) )
59 1 18 2 46 47 48 49 50 56 57 58 tgbtwnouttr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ∧ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝑥 ) )
60 53 simp3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → ( 𝑥 ∈ ( 𝐸 𝐼 𝑊 ) ∨ 𝑊 ∈ ( 𝐸 𝐼 𝑥 ) ) )
61 44 59 60 mpjaodan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐸 ∈ ( 𝐷 𝐼 𝑥 ) )
62 19 13 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) )
63 1 18 2 22 24 26 28 30 61 62 tgbtwnexch ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
64 12 simprd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) )
65 17 63 64 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
66 1 2 3 8 5 6 7 4 isinag ⊢ ( 𝜑 → ( 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ 𝑊 ≠ 𝐸 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) ) )
67 9 66 mpbid ⊢ ( 𝜑 → ( ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ 𝑊 ≠ 𝐸 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) ) )
68 67 simprd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐸 ∨ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑊 ) ) )
69 65 68 r19.29a ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )