Metamath Proof Explorer

Theorem isinag

Description: Property for point X to lie in the angle <" A B C "> . Definition 11.23 of Schwabhauser p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020)

Ref Expression
Hypotheses isinag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isinag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isinag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
isinag.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
isinag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
isinag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
isinag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
isinag.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
Assertion isinag ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isinag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isinag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 isinag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 isinag.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
5 isinag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 isinag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 isinag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 isinag.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
9 simpr ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
10 9 fveq1d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( 𝑡 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) )
11 9 fveq1d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( 𝑡 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) )
12 10 11 neeq12d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) )
13 9 fveq1d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( 𝑡 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) )
14 13 11 neeq12d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) )
15 simpl ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → 𝑝 = 𝑋 )
16 15 11 neeq12d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( 𝑝 ≠ ( 𝑡 ‘ 1 ) ↔ 𝑋 ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) )
17 12 14 16 3anbi123d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝑋 ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ) )
18 10 13 oveq12d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) = ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) )
19 18 eleq2d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ↔ 𝑥 ∈ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ) )
20 11 eqeq2d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( 𝑥 = ( 𝑡 ‘ 1 ) ↔ 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) )
21 eqidd ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → 𝑥 = 𝑥 )
22 11 fveq2d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) = ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) )
23 21 22 15 breq123d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ↔ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) )
24 20 23 orbi12d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ↔ ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) ) )
25 19 24 anbi12d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ↔ ( 𝑥 ∈ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ∧ ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) ) ) )
26 25 rexbidv ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ∧ ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) ) ) )
27 17 26 anbi12d ⊢ ( ( 𝑝 = 𝑋 ∧ 𝑡 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) → ( ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ↔ ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝑋 ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ∧ ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) ) ) ) )
28 eqid ⊢ { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } = { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) }
29 27 28 brab2a ⊢ ( 𝑋 { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( 𝑋 ∈ 𝑃 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝑋 ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ∧ ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) ) ) ) )
30 s3fv0 ⊢ ( 𝐴 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
31 5 30 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
32 s3fv1 ⊢ ( 𝐵 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
33 6 32 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
34 31 33 neeq12d ⊢ ( 𝜑 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ↔ 𝐴 ≠ 𝐵 ) )
35 s3fv2 ⊢ ( 𝐶 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
36 7 35 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
37 36 33 neeq12d ⊢ ( 𝜑 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ↔ 𝐶 ≠ 𝐵 ) )
38 33 neeq2d ⊢ ( 𝜑 → ( 𝑋 ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ↔ 𝑋 ≠ 𝐵 ) )
39 34 37 38 3anbi123d ⊢ ( 𝜑 → ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝑋 ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ↔ ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ) )
40 31 36 oveq12d ⊢ ( 𝜑 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) = ( 𝐴 𝐼 𝐶 ) )
41 40 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ↔ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) )
42 33 eqeq2d ⊢ ( 𝜑 → ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ↔ 𝑥 = 𝐵 ) )
43 33 fveq2d ⊢ ( 𝜑 → ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) = ( 𝐾 ‘ 𝐵 ) )
44 43 breqd ⊢ ( 𝜑 → ( 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ↔ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) )
45 42 44 orbi12d ⊢ ( 𝜑 → ( ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) ↔ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) )
46 41 45 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ∧ ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) ) ↔ ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) )
47 46 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ∧ ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) )
48 39 47 anbi12d ⊢ ( 𝜑 → ( ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝑋 ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ∧ ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) ) ) ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) )
49 48 anbi2d ⊢ ( 𝜑 → ( ( ( 𝑋 ∈ 𝑃 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∧ 𝑋 ≠ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) 𝐼 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ) ∧ ( 𝑥 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ) 𝑋 ) ) ) ) ↔ ( ( 𝑋 ∈ 𝑃 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) ) )
50 29 49 syl5bb ⊢ ( 𝜑 → ( 𝑋 { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( 𝑋 ∈ 𝑃 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) ) )
51 elex ⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V )
52 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
53 52 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
54 53 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑝 ∈ ( Base ‘ 𝑔 ) ↔ 𝑝 ∈ 𝑃 ) )
55 53 oveq1d ⊢ ( 𝑔 = 𝐺 → ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) = ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
56 55 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ↔ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
57 54 56 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑝 ∈ ( Base ‘ 𝑔 ) ∧ 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ↔ ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ) )
58 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = ( Itv ‘ 𝐺 ) )
59 58 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = 𝐼 )
60 59 oveqd ⊢ ( 𝑔 = 𝐺 → ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) = ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) )
61 60 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ↔ 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ) )
62 fveq2 ⊢ ( 𝑔 = 𝐺 → ( hlG ‘ 𝑔 ) = ( hlG ‘ 𝐺 ) )
63 62 3 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( hlG ‘ 𝑔 ) = 𝐾 )
64 63 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) = ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) )
65 64 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ↔ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) )
66 65 orbi2d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ↔ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) )
67 61 66 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ↔ ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) )
68 53 67 rexeqbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) )
69 68 anbi2d ⊢ ( 𝑔 = 𝐺 → ( ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ↔ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) )
70 57 69 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑝 ∈ ( Base ‘ 𝑔 ) ∧ 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) ↔ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) ) )
71 70 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ ( Base ‘ 𝑔 ) ∧ 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } = { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } )
72 df-inag ⊢ inA = ( 𝑔 ∈ V ↦ { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ ( Base ‘ 𝑔 ) ∧ 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } )
73 1 fvexi ⊢ 𝑃 ∈ V
74 ovex ⊢ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∈ V
75 73 74 xpex ⊢ ( 𝑃 × ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∈ V
76 opabssxp ⊢ { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } ⊆ ( 𝑃 × ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
77 75 76 ssexi ⊢ { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } ∈ V
78 71 72 77 fvmpt ⊢ ( 𝐺 ∈ V → ( inA ‘ 𝐺 ) = { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } )
79 8 51 78 3syl ⊢ ( 𝜑 → ( inA ‘ 𝐺 ) = { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } )
80 79 breqd ⊢ ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ 𝑋 { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ 𝑃 ∧ 𝑡 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) 𝐼 ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( 𝐾 ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) )
81 5 6 7 s3cld ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 )
82 s3len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
83 3nn0 ⊢ 3 ∈ ℕ0
84 wrdmap ⊢ ( ( 𝑃 ∈ V ∧ 3 ∈ ℕ0 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
85 73 83 84 mp2an ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
86 81 82 85 sylanblc ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
87 4 86 jca ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑃 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
88 87 biantrurd ⊢ ( 𝜑 → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ↔ ( ( 𝑋 ∈ 𝑃 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) ) )
89 50 80 88 3bitr4d ⊢ ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) )