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 ⊢ P = Base G
isleag.g ⊢ φ → G ∈ 𝒢 Tarski
isleag.a ⊢ φ → A ∈ P
isleag.b ⊢ φ → B ∈ P
isleag.c ⊢ φ → C ∈ P
isleag.d ⊢ φ → D ∈ P
isleag.e ⊢ φ → E ∈ P
isleag.f ⊢ φ → F ∈ P
Assertion isleag ⊢ φ → ⟨“ ABC ”⟩ ≤ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩ ↔ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩ ∧ ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ DEx ”⟩

Proof

Step Hyp Ref Expression
1 isleag.p ⊢ P = Base G
2 isleag.g ⊢ φ → G ∈ 𝒢 Tarski
3 isleag.a ⊢ φ → A ∈ P
4 isleag.b ⊢ φ → B ∈ P
5 isleag.c ⊢ φ → C ∈ P
6 isleag.d ⊢ φ → D ∈ P
7 isleag.e ⊢ φ → E ∈ P
8 isleag.f ⊢ φ → F ∈ P
9 3 4 5 s3cld ⊢ φ → ⟨“ ABC ”⟩ ∈ Word P
10 s3len ⊢ ⟨“ ABC ”⟩ = 3
11 1 fvexi ⊢ P ∈ V
12 3nn0 ⊢ 3 ∈ ℕ 0
13 wrdmap ⊢ P ∈ V ∧ 3 ∈ ℕ 0 → ⟨“ ABC ”⟩ ∈ Word P ∧ ⟨“ ABC ”⟩ = 3 ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3
14 11 12 13 mp2an ⊢ ⟨“ ABC ”⟩ ∈ Word P ∧ ⟨“ ABC ”⟩ = 3 ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3
15 9 10 14 sylanblc ⊢ φ → ⟨“ ABC ”⟩ ∈ P 0 ..^ 3
16 6 7 8 s3cld ⊢ φ → ⟨“ DEF ”⟩ ∈ Word P
17 s3len ⊢ ⟨“ DEF ”⟩ = 3
18 wrdmap ⊢ P ∈ V ∧ 3 ∈ ℕ 0 → ⟨“ DEF ”⟩ ∈ Word P ∧ ⟨“ DEF ”⟩ = 3 ↔ ⟨“ DEF ”⟩ ∈ P 0 ..^ 3
19 11 12 18 mp2an ⊢ ⟨“ DEF ”⟩ ∈ Word P ∧ ⟨“ DEF ”⟩ = 3 ↔ ⟨“ DEF ”⟩ ∈ P 0 ..^ 3
20 16 17 19 sylanblc ⊢ φ → ⟨“ DEF ”⟩ ∈ P 0 ..^ 3
21 15 20 jca ⊢ φ → ⟨“ ABC ”⟩ ∈ P 0 ..^ 3 ∧ ⟨“ DEF ”⟩ ∈ P 0 ..^ 3
22 elex ⊢ G ∈ 𝒢 Tarski → G ∈ V
23 fveq2 ⊢ g = G → Base g = Base G
24 23 1 eqtr4di ⊢ g = G → Base g = P
25 24 oveq1d ⊢ g = G → Base g 0 ..^ 3 = P 0 ..^ 3
26 25 eleq2d ⊢ g = G → a ∈ Base g 0 ..^ 3 ↔ a ∈ P 0 ..^ 3
27 25 eleq2d ⊢ g = G → b ∈ Base g 0 ..^ 3 ↔ b ∈ P 0 ..^ 3
28 26 27 anbi12d ⊢ g = G → a ∈ Base g 0 ..^ 3 ∧ b ∈ Base g 0 ..^ 3 ↔ a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3
29 fveq2 ⊢ g = G → ∈ 𝒢 ∠ ⁡ g = ∈ 𝒢 ∠ ⁡ G
30 29 breqd ⊢ g = G → x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ↔ x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩
31 fveq2 ⊢ g = G → ∼ 𝒢 ∠ ⁡ g = ∼ 𝒢 ∠ ⁡ G
32 31 breqd ⊢ g = G → ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ↔ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
33 30 32 anbi12d ⊢ g = G → x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ↔ x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
34 24 33 rexeqbidv ⊢ g = G → ∃ x ∈ Base g x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ↔ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
35 28 34 anbi12d ⊢ g = G → a ∈ Base g 0 ..^ 3 ∧ b ∈ Base g 0 ..^ 3 ∧ ∃ x ∈ Base g x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ↔ a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
36 35 opabbidv ⊢ g = G → a b | a ∈ Base g 0 ..^ 3 ∧ b ∈ Base g 0 ..^ 3 ∧ ∃ x ∈ Base g x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ = a b | a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
37 df-leag ⊢ ≤ 𝒢 ∠ = g ∈ V ⟼ a b | a ∈ Base g 0 ..^ 3 ∧ b ∈ Base g 0 ..^ 3 ∧ ∃ x ∈ Base g x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
38 ovex ⊢ P 0 ..^ 3 ∈ V
39 38 38 xpex ⊢ P 0 ..^ 3 × P 0 ..^ 3 ∈ V
40 opabssxp ⊢ a b | a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ⊆ P 0 ..^ 3 × P 0 ..^ 3
41 39 40 ssexi ⊢ a b | a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ∈ V
42 36 37 41 fvmpt ⊢ G ∈ V → ≤ 𝒢 ∠ ⁡ G = a b | a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
43 2 22 42 3syl ⊢ φ → ≤ 𝒢 ∠ ⁡ G = a b | a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
44 43 breqd ⊢ φ → ⟨“ ABC ”⟩ ≤ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩ ↔ ⟨“ ABC ”⟩ a b | a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ⟨“ DEF ”⟩
45 simpr ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → b = ⟨“ DEF ”⟩
46 45 fveq1d ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → b ⁡ 0 = ⟨“ DEF ”⟩ ⁡ 0
47 45 fveq1d ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → b ⁡ 1 = ⟨“ DEF ”⟩ ⁡ 1
48 45 fveq1d ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → b ⁡ 2 = ⟨“ DEF ”⟩ ⁡ 2
49 46 47 48 s3eqd ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ = ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩
50 49 breq2d ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ↔ x ∈ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩
51 simpl ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → a = ⟨“ ABC ”⟩
52 51 fveq1d ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → a ⁡ 0 = ⟨“ ABC ”⟩ ⁡ 0
53 51 fveq1d ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → a ⁡ 1 = ⟨“ ABC ”⟩ ⁡ 1
54 51 fveq1d ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → a ⁡ 2 = ⟨“ ABC ”⟩ ⁡ 2
55 52 53 54 s3eqd ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ = ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩
56 eqidd ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → x = x
57 46 47 56 s3eqd ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ = ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩
58 55 57 breq12d ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ↔ ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩
59 50 58 anbi12d ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ↔ x ∈ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩ ∧ ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩
60 59 rexbidv ⊢ a = ⟨“ ABC ”⟩ ∧ b = ⟨“ DEF ”⟩ → ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ↔ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩ ∧ ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩
61 eqid ⊢ a b | a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ = a b | a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
62 60 61 brab2a ⊢ ⟨“ ABC ”⟩ a b | a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ⟨“ DEF ”⟩ ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3 ∧ ⟨“ DEF ”⟩ ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩ ∧ ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩
63 62 a1i ⊢ φ → ⟨“ ABC ”⟩ a b | a ∈ P 0 ..^ 3 ∧ b ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩ ⟨“ DEF ”⟩ ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3 ∧ ⟨“ DEF ”⟩ ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩ ∧ ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩
64 s3fv0 ⊢ D ∈ P → ⟨“ DEF ”⟩ ⁡ 0 = D
65 6 64 syl ⊢ φ → ⟨“ DEF ”⟩ ⁡ 0 = D
66 s3fv1 ⊢ E ∈ P → ⟨“ DEF ”⟩ ⁡ 1 = E
67 7 66 syl ⊢ φ → ⟨“ DEF ”⟩ ⁡ 1 = E
68 s3fv2 ⊢ F ∈ P → ⟨“ DEF ”⟩ ⁡ 2 = F
69 8 68 syl ⊢ φ → ⟨“ DEF ”⟩ ⁡ 2 = F
70 65 67 69 s3eqd ⊢ φ → ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩ = ⟨“ DEF ”⟩
71 70 breq2d ⊢ φ → x ∈ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩ ↔ x ∈ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩
72 s3fv0 ⊢ A ∈ P → ⟨“ ABC ”⟩ ⁡ 0 = A
73 3 72 syl ⊢ φ → ⟨“ ABC ”⟩ ⁡ 0 = A
74 s3fv1 ⊢ B ∈ P → ⟨“ ABC ”⟩ ⁡ 1 = B
75 4 74 syl ⊢ φ → ⟨“ ABC ”⟩ ⁡ 1 = B
76 s3fv2 ⊢ C ∈ P → ⟨“ ABC ”⟩ ⁡ 2 = C
77 5 76 syl ⊢ φ → ⟨“ ABC ”⟩ ⁡ 2 = C
78 73 75 77 s3eqd ⊢ φ → ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩ = ⟨“ ABC ”⟩
79 eqidd ⊢ φ → x = x
80 65 67 79 s3eqd ⊢ φ → ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩ = ⟨“ DEx ”⟩
81 78 80 breq12d ⊢ φ → ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩ ↔ ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ DEx ”⟩
82 71 81 anbi12d ⊢ φ → x ∈ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩ ∧ ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩ ↔ x ∈ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩ ∧ ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ DEx ”⟩
83 82 rexbidv ⊢ φ → ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩ ∧ ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩ ↔ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩ ∧ ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ DEx ”⟩
84 83 anbi2d ⊢ φ → ⟨“ ABC ”⟩ ∈ P 0 ..^ 3 ∧ ⟨“ DEF ”⟩ ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 ⟨“ DEF ”⟩ ⁡ 2 ”⟩ ∧ ⟨“ ⟨“ ABC ”⟩ ⁡ 0 ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ ⟨“ DEF ”⟩ ⁡ 0 ⟨“ DEF ”⟩ ⁡ 1 x ”⟩ ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3 ∧ ⟨“ DEF ”⟩ ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩ ∧ ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ DEx ”⟩
85 44 63 84 3bitrd ⊢ φ → ⟨“ ABC ”⟩ ≤ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩ ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3 ∧ ⟨“ DEF ”⟩ ∈ P 0 ..^ 3 ∧ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩ ∧ ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ DEx ”⟩
86 21 85 mpbirand ⊢ φ → ⟨“ ABC ”⟩ ≤ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩ ↔ ∃ x ∈ P x ∈ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩ ∧ ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ DEx ”⟩