Metamath Proof Explorer

Theorem isleag

Description: Geometrical "less than" property for angles. Definition 11.27 of Schwabhauser p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020)

Ref Expression
Hypotheses isleag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isleag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isleag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
isleag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
isleag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
isleag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
isleag.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
isleag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
Assertion isleag ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) )

Proof

Step Hyp Ref Expression
1 isleag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isleag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
3 isleag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
4 isleag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
5 isleag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
6 isleag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
7 isleag.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
8 isleag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
9 3 4 5 s3cld ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 )
10 s3len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
11 1 fvexi ⊢ 𝑃 ∈ V
12 3nn0 ⊢ 3 ∈ ℕ0
13 wrdmap ⊢ ( ( 𝑃 ∈ V ∧ 3 ∈ ℕ0 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
14 11 12 13 mp2an ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
15 9 10 14 sylanblc ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
16 6 7 8 s3cld ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ Word 𝑃 )
17 s3len ⊢ ( ♯ ‘ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) = 3
18 wrdmap ⊢ ( ( 𝑃 ∈ V ∧ 3 ∈ ℕ0 ) → ( ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) = 3 ) ↔ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
19 11 12 18 mp2an ⊢ ( ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ Word 𝑃 ∧ ( ♯ ‘ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) = 3 ) ↔ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
20 16 17 19 sylanblc ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
21 15 20 jca ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
22 elex ⊢ ( 𝐺 ∈ TarskiG → 𝐺 ∈ V )
23 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
24 23 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
25 24 oveq1d ⊢ ( 𝑔 = 𝐺 → ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) = ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
26 25 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ↔ 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
27 25 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ↔ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) )
28 26 27 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ↔ ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ) )
29 fveq2 ⊢ ( 𝑔 = 𝐺 → ( inA ‘ 𝑔 ) = ( inA ‘ 𝐺 ) )
30 29 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ↔ 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ) )
31 fveq2 ⊢ ( 𝑔 = 𝐺 → ( cgrA ‘ 𝑔 ) = ( cgrA ‘ 𝐺 ) )
32 31 breqd ⊢ ( 𝑔 = 𝐺 → ( ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ↔ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) )
33 30 32 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ↔ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) )
34 24 33 rexeqbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) )
35 28 34 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) ) )
36 35 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } )
37 df-leag ⊢ ≤∠ = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } )
38 ovex ⊢ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∈ V
39 38 38 xpex ⊢ ( ( 𝑃 ↑m ( 0 ..^ 3 ) ) × ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∈ V
40 opabssxp ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } ⊆ ( ( 𝑃 ↑m ( 0 ..^ 3 ) ) × ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
41 39 40 ssexi ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } ∈ V
42 36 37 41 fvmpt ⊢ ( 𝐺 ∈ V → ( ≤∠ ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } )
43 2 22 42 3syl ⊢ ( 𝜑 → ( ≤∠ ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } )
44 43 breqd ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) )
45 simpr ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
46 45 fveq1d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑏 ‘ 0 ) = ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) )
47 45 fveq1d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑏 ‘ 1 ) = ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) )
48 45 fveq1d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑏 ‘ 2 ) = ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) )
49 46 47 48 s3eqd ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ = ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ )
50 49 breq2d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ↔ 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ ) )
51 simpl ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
52 51 fveq1d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑎 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) )
53 51 fveq1d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑎 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) )
54 51 fveq1d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝑎 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) )
55 52 53 54 s3eqd ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ = ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ )
56 eqidd ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝑥 = 𝑥 )
57 46 47 56 s3eqd ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ = ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ )
58 55 57 breq12d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ↔ ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ ) )
59 50 58 anbi12d ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ↔ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ ∧ ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ ) ) )
60 59 rexbidv ⊢ ( ( 𝑎 = ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∧ 𝑏 = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ ∧ ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ ) ) )
61 eqid ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) }
62 60 61 brab2a ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ ∧ ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ ) ) )
63 62 a1i ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ ∧ ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ ) ) ) )
64 s3fv0 ⊢ ( 𝐷 ∈ 𝑃 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) = 𝐷 )
65 6 64 syl ⊢ ( 𝜑 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) = 𝐷 )
66 s3fv1 ⊢ ( 𝐸 ∈ 𝑃 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) = 𝐸 )
67 7 66 syl ⊢ ( 𝜑 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) = 𝐸 )
68 s3fv2 ⊢ ( 𝐹 ∈ 𝑃 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) = 𝐹 )
69 8 68 syl ⊢ ( 𝜑 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) = 𝐹 )
70 65 67 69 s3eqd ⊢ ( 𝜑 → ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ = ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
71 70 breq2d ⊢ ( 𝜑 → ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ ↔ 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) )
72 s3fv0 ⊢ ( 𝐴 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
73 3 72 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
74 s3fv1 ⊢ ( 𝐵 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
75 4 74 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
76 s3fv2 ⊢ ( 𝐶 ∈ 𝑃 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
77 5 76 syl ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
78 73 75 77 s3eqd ⊢ ( 𝜑 → ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ = ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
79 eqidd ⊢ ( 𝜑 → 𝑥 = 𝑥 )
80 65 67 79 s3eqd ⊢ ( 𝜑 → ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ = ⟨“ 𝐷 𝐸 𝑥 ”⟩ )
81 78 80 breq12d ⊢ ( 𝜑 → ( ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) )
82 71 81 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ ∧ ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ ) ↔ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) )
83 82 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ ∧ ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) )
84 83 anbi2d ⊢ ( 𝜑 → ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 2 ) ”⟩ ∧ ⟨“ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 0 ) ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ‘ 1 ) 𝑥 ”⟩ ) ) ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) ) )
85 44 63 84 3bitrd ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∧ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) ) )
86 21 85 mpbirand ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) )