Metamath Proof Explorer

Theorem grimgrtri

Description: Graph isomorphisms map triangles onto triangles. (Contributed by AV, 27-Jul-2025) (Proof shortened by AV, 24-Aug-2025)

Ref Expression
Hypotheses grimgrtri.g ⊢ φ → G ∈ UHGraph
grimgrtri.h ⊢ φ → H ∈ UHGraph
grimgrtri.n ⊢ φ → F ∈ G GraphIso H
grimgrtri.t No typesetting found for |- ( ph -> T e. ( GrTriangles ` G ) ) with typecode |-
Assertion grimgrtri Could not format assertion : No typesetting found for |- ( ph -> ( F " T ) e. ( GrTriangles ` H ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 grimgrtri.g ⊢ φ → G ∈ UHGraph
2 grimgrtri.h ⊢ φ → H ∈ UHGraph
3 grimgrtri.n ⊢ φ → F ∈ G GraphIso H
4 grimgrtri.t Could not format ( ph -> T e. ( GrTriangles ` G ) ) : No typesetting found for |- ( ph -> T e. ( GrTriangles ` G ) ) with typecode |-
5 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
6 eqid ⊢ Edg ⁡ G = Edg ⁡ G
7 5 6 grtriprop Could not format ( T e. ( GrTriangles ` G ) -> E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) E. c e. ( Vtx ` G ) ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) : No typesetting found for |- ( T e. ( GrTriangles ` G ) -> E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) E. c e. ( Vtx ` G ) ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) with typecode |-
8 4 7 syl ⊢ φ → ∃ a ∈ Vtx ⁡ G ∃ b ∈ Vtx ⁡ G ∃ c ∈ Vtx ⁡ G T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G
9 eqid ⊢ Vtx ⁡ H = Vtx ⁡ H
10 5 9 grimf1o ⊢ F ∈ G GraphIso H → F : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H
11 f1of1 ⊢ F : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H → F : Vtx ⁡ G ⟶ 1-1 Vtx ⁡ H
12 3 10 11 3syl ⊢ φ → F : Vtx ⁡ G ⟶ 1-1 Vtx ⁡ H
13 12 ad3antrrr ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → F : Vtx ⁡ G ⟶ 1-1 Vtx ⁡ H
14 simplrl ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → a ∈ Vtx ⁡ G
15 14 adantr ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → a ∈ Vtx ⁡ G
16 simprr ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G → b ∈ Vtx ⁡ G
17 16 adantr ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → b ∈ Vtx ⁡ G
18 17 adantr ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → b ∈ Vtx ⁡ G
19 simplr ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → c ∈ Vtx ⁡ G
20 15 18 19 3jca ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G
21 3simpa ⊢ T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → T = a b c ∧ T = 3
22 21 adantl ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → T = a b c ∧ T = 3
23 grtrimap ⊢ F : Vtx ⁡ G ⟶ 1-1 Vtx ⁡ H → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 → F ⁡ a ∈ Vtx ⁡ H ∧ F ⁡ b ∈ Vtx ⁡ H ∧ F ⁡ c ∈ Vtx ⁡ H ∧ F T = F ⁡ a F ⁡ b F ⁡ c ∧ F T = 3
24 23 imp ⊢ F : Vtx ⁡ G ⟶ 1-1 Vtx ⁡ H ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 → F ⁡ a ∈ Vtx ⁡ H ∧ F ⁡ b ∈ Vtx ⁡ H ∧ F ⁡ c ∈ Vtx ⁡ H ∧ F T = F ⁡ a F ⁡ b F ⁡ c ∧ F T = 3
25 13 20 22 24 syl12anc ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → F ⁡ a ∈ Vtx ⁡ H ∧ F ⁡ b ∈ Vtx ⁡ H ∧ F ⁡ c ∈ Vtx ⁡ H ∧ F T = F ⁡ a F ⁡ b F ⁡ c ∧ F T = 3
26 eqid ⊢ Edg ⁡ H = Edg ⁡ H
27 5 6 26 grimedg ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → a b ∈ Edg ⁡ G ↔ F a b ∈ Edg ⁡ H ∧ a b ⊆ Vtx ⁡ G
28 5 6 26 grimedg ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → a c ∈ Edg ⁡ G ↔ F a c ∈ Edg ⁡ H ∧ a c ⊆ Vtx ⁡ G
29 5 6 26 grimedg ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → b c ∈ Edg ⁡ G ↔ F b c ∈ Edg ⁡ H ∧ b c ⊆ Vtx ⁡ G
30 27 28 29 3anbi123d ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ↔ F a b ∈ Edg ⁡ H ∧ a b ⊆ Vtx ⁡ G ∧ F a c ∈ Edg ⁡ H ∧ a c ⊆ Vtx ⁡ G ∧ F b c ∈ Edg ⁡ H ∧ b c ⊆ Vtx ⁡ G
31 f1ofn ⊢ F : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H → F Fn Vtx ⁡ G
32 simpl ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F Fn Vtx ⁡ G
33 simprll ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → a ∈ Vtx ⁡ G
34 simprlr ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → b ∈ Vtx ⁡ G
35 fnimapr ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G → F a b = F ⁡ a F ⁡ b
36 32 33 34 35 syl3anc ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a b = F ⁡ a F ⁡ b
37 36 eleq1d ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a b ∈ Edg ⁡ H ↔ F ⁡ a F ⁡ b ∈ Edg ⁡ H
38 37 biimpd ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a b ∈ Edg ⁡ H → F ⁡ a F ⁡ b ∈ Edg ⁡ H
39 38 adantrd ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a b ∈ Edg ⁡ H ∧ a b ⊆ Vtx ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H
40 simprr ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → c ∈ Vtx ⁡ G
41 fnimapr ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a c = F ⁡ a F ⁡ c
42 32 33 40 41 syl3anc ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a c = F ⁡ a F ⁡ c
43 42 eleq1d ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a c ∈ Edg ⁡ H ↔ F ⁡ a F ⁡ c ∈ Edg ⁡ H
44 43 biimpd ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a c ∈ Edg ⁡ H → F ⁡ a F ⁡ c ∈ Edg ⁡ H
45 44 adantrd ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a c ∈ Edg ⁡ H ∧ a c ⊆ Vtx ⁡ G → F ⁡ a F ⁡ c ∈ Edg ⁡ H
46 fnimapr ⊢ F Fn Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F b c = F ⁡ b F ⁡ c
47 32 34 40 46 syl3anc ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F b c = F ⁡ b F ⁡ c
48 47 eleq1d ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F b c ∈ Edg ⁡ H ↔ F ⁡ b F ⁡ c ∈ Edg ⁡ H
49 48 biimpd ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F b c ∈ Edg ⁡ H → F ⁡ b F ⁡ c ∈ Edg ⁡ H
50 49 adantrd ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F b c ∈ Edg ⁡ H ∧ b c ⊆ Vtx ⁡ G → F ⁡ b F ⁡ c ∈ Edg ⁡ H
51 39 45 50 3anim123d ⊢ F Fn Vtx ⁡ G ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a b ∈ Edg ⁡ H ∧ a b ⊆ Vtx ⁡ G ∧ F a c ∈ Edg ⁡ H ∧ a c ⊆ Vtx ⁡ G ∧ F b c ∈ Edg ⁡ H ∧ b c ⊆ Vtx ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
52 51 ex ⊢ F Fn Vtx ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F a b ∈ Edg ⁡ H ∧ a b ⊆ Vtx ⁡ G ∧ F a c ∈ Edg ⁡ H ∧ a c ⊆ Vtx ⁡ G ∧ F b c ∈ Edg ⁡ H ∧ b c ⊆ Vtx ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
53 52 com23 ⊢ F Fn Vtx ⁡ G → F a b ∈ Edg ⁡ H ∧ a b ⊆ Vtx ⁡ G ∧ F a c ∈ Edg ⁡ H ∧ a c ⊆ Vtx ⁡ G ∧ F b c ∈ Edg ⁡ H ∧ b c ⊆ Vtx ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
54 10 31 53 3syl ⊢ F ∈ G GraphIso H → F a b ∈ Edg ⁡ H ∧ a b ⊆ Vtx ⁡ G ∧ F a c ∈ Edg ⁡ H ∧ a c ⊆ Vtx ⁡ G ∧ F b c ∈ Edg ⁡ H ∧ b c ⊆ Vtx ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
55 54 3ad2ant3 ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → F a b ∈ Edg ⁡ H ∧ a b ⊆ Vtx ⁡ G ∧ F a c ∈ Edg ⁡ H ∧ a c ⊆ Vtx ⁡ G ∧ F b c ∈ Edg ⁡ H ∧ b c ⊆ Vtx ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
56 30 55 sylbid ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
57 56 2a1d ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → T = a b c → T = 3 → a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
58 57 3impd ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
59 58 com23 ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ F ∈ G GraphIso H → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
60 1 2 3 59 syl3anc ⊢ φ → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
61 60 impl ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G → T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
62 61 imp ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
63 tpeq1 ⊢ x = F ⁡ a → x y z = F ⁡ a y z
64 63 eqeq2d ⊢ x = F ⁡ a → F T = x y z ↔ F T = F ⁡ a y z
65 preq1 ⊢ x = F ⁡ a → x y = F ⁡ a y
66 65 eleq1d ⊢ x = F ⁡ a → x y ∈ Edg ⁡ H ↔ F ⁡ a y ∈ Edg ⁡ H
67 preq1 ⊢ x = F ⁡ a → x z = F ⁡ a z
68 67 eleq1d ⊢ x = F ⁡ a → x z ∈ Edg ⁡ H ↔ F ⁡ a z ∈ Edg ⁡ H
69 66 68 3anbi12d ⊢ x = F ⁡ a → x y ∈ Edg ⁡ H ∧ x z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H ↔ F ⁡ a y ∈ Edg ⁡ H ∧ F ⁡ a z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H
70 64 69 3anbi13d ⊢ x = F ⁡ a → F T = x y z ∧ F T = 3 ∧ x y ∈ Edg ⁡ H ∧ x z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H ↔ F T = F ⁡ a y z ∧ F T = 3 ∧ F ⁡ a y ∈ Edg ⁡ H ∧ F ⁡ a z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H
71 tpeq2 ⊢ y = F ⁡ b → F ⁡ a y z = F ⁡ a F ⁡ b z
72 71 eqeq2d ⊢ y = F ⁡ b → F T = F ⁡ a y z ↔ F T = F ⁡ a F ⁡ b z
73 preq2 ⊢ y = F ⁡ b → F ⁡ a y = F ⁡ a F ⁡ b
74 73 eleq1d ⊢ y = F ⁡ b → F ⁡ a y ∈ Edg ⁡ H ↔ F ⁡ a F ⁡ b ∈ Edg ⁡ H
75 preq1 ⊢ y = F ⁡ b → y z = F ⁡ b z
76 75 eleq1d ⊢ y = F ⁡ b → y z ∈ Edg ⁡ H ↔ F ⁡ b z ∈ Edg ⁡ H
77 74 76 3anbi13d ⊢ y = F ⁡ b → F ⁡ a y ∈ Edg ⁡ H ∧ F ⁡ a z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H ↔ F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a z ∈ Edg ⁡ H ∧ F ⁡ b z ∈ Edg ⁡ H
78 72 77 3anbi13d ⊢ y = F ⁡ b → F T = F ⁡ a y z ∧ F T = 3 ∧ F ⁡ a y ∈ Edg ⁡ H ∧ F ⁡ a z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H ↔ F T = F ⁡ a F ⁡ b z ∧ F T = 3 ∧ F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a z ∈ Edg ⁡ H ∧ F ⁡ b z ∈ Edg ⁡ H
79 tpeq3 ⊢ z = F ⁡ c → F ⁡ a F ⁡ b z = F ⁡ a F ⁡ b F ⁡ c
80 79 eqeq2d ⊢ z = F ⁡ c → F T = F ⁡ a F ⁡ b z ↔ F T = F ⁡ a F ⁡ b F ⁡ c
81 preq2 ⊢ z = F ⁡ c → F ⁡ a z = F ⁡ a F ⁡ c
82 81 eleq1d ⊢ z = F ⁡ c → F ⁡ a z ∈ Edg ⁡ H ↔ F ⁡ a F ⁡ c ∈ Edg ⁡ H
83 preq2 ⊢ z = F ⁡ c → F ⁡ b z = F ⁡ b F ⁡ c
84 83 eleq1d ⊢ z = F ⁡ c → F ⁡ b z ∈ Edg ⁡ H ↔ F ⁡ b F ⁡ c ∈ Edg ⁡ H
85 82 84 3anbi23d ⊢ z = F ⁡ c → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a z ∈ Edg ⁡ H ∧ F ⁡ b z ∈ Edg ⁡ H ↔ F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
86 80 85 3anbi13d ⊢ z = F ⁡ c → F T = F ⁡ a F ⁡ b z ∧ F T = 3 ∧ F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a z ∈ Edg ⁡ H ∧ F ⁡ b z ∈ Edg ⁡ H ↔ F T = F ⁡ a F ⁡ b F ⁡ c ∧ F T = 3 ∧ F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H
87 70 78 86 rspc3ev ⊢ F ⁡ a ∈ Vtx ⁡ H ∧ F ⁡ b ∈ Vtx ⁡ H ∧ F ⁡ c ∈ Vtx ⁡ H ∧ F T = F ⁡ a F ⁡ b F ⁡ c ∧ F T = 3 ∧ F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H → ∃ x ∈ Vtx ⁡ H ∃ y ∈ Vtx ⁡ H ∃ z ∈ Vtx ⁡ H F T = x y z ∧ F T = 3 ∧ x y ∈ Edg ⁡ H ∧ x z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H
88 87 3exp2 ⊢ F ⁡ a ∈ Vtx ⁡ H ∧ F ⁡ b ∈ Vtx ⁡ H ∧ F ⁡ c ∈ Vtx ⁡ H → F T = F ⁡ a F ⁡ b F ⁡ c → F T = 3 → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H → ∃ x ∈ Vtx ⁡ H ∃ y ∈ Vtx ⁡ H ∃ z ∈ Vtx ⁡ H F T = x y z ∧ F T = 3 ∧ x y ∈ Edg ⁡ H ∧ x z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H
89 88 3imp ⊢ F ⁡ a ∈ Vtx ⁡ H ∧ F ⁡ b ∈ Vtx ⁡ H ∧ F ⁡ c ∈ Vtx ⁡ H ∧ F T = F ⁡ a F ⁡ b F ⁡ c ∧ F T = 3 → F ⁡ a F ⁡ b ∈ Edg ⁡ H ∧ F ⁡ a F ⁡ c ∈ Edg ⁡ H ∧ F ⁡ b F ⁡ c ∈ Edg ⁡ H → ∃ x ∈ Vtx ⁡ H ∃ y ∈ Vtx ⁡ H ∃ z ∈ Vtx ⁡ H F T = x y z ∧ F T = 3 ∧ x y ∈ Edg ⁡ H ∧ x z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H
90 25 62 89 sylc ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ c ∈ Vtx ⁡ G ∧ T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → ∃ x ∈ Vtx ⁡ H ∃ y ∈ Vtx ⁡ H ∃ z ∈ Vtx ⁡ H F T = x y z ∧ F T = 3 ∧ x y ∈ Edg ⁡ H ∧ x z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H
91 90 rexlimdva2 ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G → ∃ c ∈ Vtx ⁡ G T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → ∃ x ∈ Vtx ⁡ H ∃ y ∈ Vtx ⁡ H ∃ z ∈ Vtx ⁡ H F T = x y z ∧ F T = 3 ∧ x y ∈ Edg ⁡ H ∧ x z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H
92 91 rexlimdvva ⊢ φ → ∃ a ∈ Vtx ⁡ G ∃ b ∈ Vtx ⁡ G ∃ c ∈ Vtx ⁡ G T = a b c ∧ T = 3 ∧ a b ∈ Edg ⁡ G ∧ a c ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G → ∃ x ∈ Vtx ⁡ H ∃ y ∈ Vtx ⁡ H ∃ z ∈ Vtx ⁡ H F T = x y z ∧ F T = 3 ∧ x y ∈ Edg ⁡ H ∧ x z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H
93 8 92 mpd ⊢ φ → ∃ x ∈ Vtx ⁡ H ∃ y ∈ Vtx ⁡ H ∃ z ∈ Vtx ⁡ H F T = x y z ∧ F T = 3 ∧ x y ∈ Edg ⁡ H ∧ x z ∈ Edg ⁡ H ∧ y z ∈ Edg ⁡ H
94 9 26 isgrtri Could not format ( ( F " T ) e. ( GrTriangles ` H ) <-> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) : No typesetting found for |- ( ( F " T ) e. ( GrTriangles ` H ) <-> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) with typecode |-
95 93 94 sylibr Could not format ( ph -> ( F " T ) e. ( GrTriangles ` H ) ) : No typesetting found for |- ( ph -> ( F " T ) e. ( GrTriangles ` H ) ) with typecode |-