Metamath Proof Explorer

Theorem grtrif1o

Description: Any bijection onto a triangle preserves the edges of the triangle. (Contributed by AV, 25-Jul-2025)

Ref Expression
Hypotheses grtri.v ⊢ V = Vtx ⁡ G
grtri.e ⊢ E = Edg ⁡ G
Assertion grtrif1o Could not format assertion : No typesetting found for |- ( ( T e. ( GrTriangles ` G ) /\ F : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 grtri.v ⊢ V = Vtx ⁡ G
2 grtri.e ⊢ E = Edg ⁡ G
3 1 2 grtriprop Could not format ( T e. ( GrTriangles ` G ) -> E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) : No typesetting found for |- ( T e. ( GrTriangles ` G ) -> E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) with typecode |-
4 f1oeq3 ⊢ T = x y z → F : 0 ..^ 3 ⟶ 1-1 onto T ↔ F : 0 ..^ 3 ⟶ 1-1 onto x y z
5 4 adantr ⊢ T = x y z ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F : 0 ..^ 3 ⟶ 1-1 onto T ↔ F : 0 ..^ 3 ⟶ 1-1 onto x y z
6 preq12 ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = y → F ⁡ 0 F ⁡ 1 = x y
7 6 eleq1d ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = y → F ⁡ 0 F ⁡ 1 ∈ E ↔ x y ∈ E
8 7 3adant3 ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = y ∧ F ⁡ 2 = z → F ⁡ 0 F ⁡ 1 ∈ E ↔ x y ∈ E
9 preq12 ⊢ F ⁡ 0 = x ∧ F ⁡ 2 = z → F ⁡ 0 F ⁡ 2 = x z
10 9 eleq1d ⊢ F ⁡ 0 = x ∧ F ⁡ 2 = z → F ⁡ 0 F ⁡ 2 ∈ E ↔ x z ∈ E
11 10 3adant2 ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = y ∧ F ⁡ 2 = z → F ⁡ 0 F ⁡ 2 ∈ E ↔ x z ∈ E
12 preq12 ⊢ F ⁡ 1 = y ∧ F ⁡ 2 = z → F ⁡ 1 F ⁡ 2 = y z
13 12 eleq1d ⊢ F ⁡ 1 = y ∧ F ⁡ 2 = z → F ⁡ 1 F ⁡ 2 ∈ E ↔ y z ∈ E
14 13 3adant1 ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = y ∧ F ⁡ 2 = z → F ⁡ 1 F ⁡ 2 ∈ E ↔ y z ∈ E
15 8 11 14 3anbi123d ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = y ∧ F ⁡ 2 = z → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E ↔ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E
16 15 biimprd ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = y ∧ F ⁡ 2 = z → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
17 3ancoma ⊢ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E ↔ x z ∈ E ∧ x y ∈ E ∧ y z ∈ E
18 prcom ⊢ y z = z y
19 18 eleq1i ⊢ y z ∈ E ↔ z y ∈ E
20 19 3anbi3i ⊢ x z ∈ E ∧ x y ∈ E ∧ y z ∈ E ↔ x z ∈ E ∧ x y ∈ E ∧ z y ∈ E
21 17 20 sylbb ⊢ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → x z ∈ E ∧ x y ∈ E ∧ z y ∈ E
22 preq12 ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = z → F ⁡ 0 F ⁡ 1 = x z
23 22 eleq1d ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = z → F ⁡ 0 F ⁡ 1 ∈ E ↔ x z ∈ E
24 23 3adant3 ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = z ∧ F ⁡ 2 = y → F ⁡ 0 F ⁡ 1 ∈ E ↔ x z ∈ E
25 preq12 ⊢ F ⁡ 0 = x ∧ F ⁡ 2 = y → F ⁡ 0 F ⁡ 2 = x y
26 25 eleq1d ⊢ F ⁡ 0 = x ∧ F ⁡ 2 = y → F ⁡ 0 F ⁡ 2 ∈ E ↔ x y ∈ E
27 26 3adant2 ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = z ∧ F ⁡ 2 = y → F ⁡ 0 F ⁡ 2 ∈ E ↔ x y ∈ E
28 preq12 ⊢ F ⁡ 1 = z ∧ F ⁡ 2 = y → F ⁡ 1 F ⁡ 2 = z y
29 28 eleq1d ⊢ F ⁡ 1 = z ∧ F ⁡ 2 = y → F ⁡ 1 F ⁡ 2 ∈ E ↔ z y ∈ E
30 29 3adant1 ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = z ∧ F ⁡ 2 = y → F ⁡ 1 F ⁡ 2 ∈ E ↔ z y ∈ E
31 24 27 30 3anbi123d ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = z ∧ F ⁡ 2 = y → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E ↔ x z ∈ E ∧ x y ∈ E ∧ z y ∈ E
32 21 31 imbitrrid ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = z ∧ F ⁡ 2 = y → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
33 16 32 jaoi ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = y ∧ F ⁡ 2 = z ∨ F ⁡ 0 = x ∧ F ⁡ 1 = z ∧ F ⁡ 2 = y → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
34 3ancomb ⊢ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E ↔ x y ∈ E ∧ y z ∈ E ∧ x z ∈ E
35 prcom ⊢ x y = y x
36 35 eleq1i ⊢ x y ∈ E ↔ y x ∈ E
37 36 3anbi1i ⊢ x y ∈ E ∧ y z ∈ E ∧ x z ∈ E ↔ y x ∈ E ∧ y z ∈ E ∧ x z ∈ E
38 34 37 sylbb ⊢ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → y x ∈ E ∧ y z ∈ E ∧ x z ∈ E
39 preq12 ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = x → F ⁡ 0 F ⁡ 1 = y x
40 39 eleq1d ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = x → F ⁡ 0 F ⁡ 1 ∈ E ↔ y x ∈ E
41 40 3adant3 ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = x ∧ F ⁡ 2 = z → F ⁡ 0 F ⁡ 1 ∈ E ↔ y x ∈ E
42 preq12 ⊢ F ⁡ 0 = y ∧ F ⁡ 2 = z → F ⁡ 0 F ⁡ 2 = y z
43 42 eleq1d ⊢ F ⁡ 0 = y ∧ F ⁡ 2 = z → F ⁡ 0 F ⁡ 2 ∈ E ↔ y z ∈ E
44 43 3adant2 ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = x ∧ F ⁡ 2 = z → F ⁡ 0 F ⁡ 2 ∈ E ↔ y z ∈ E
45 preq12 ⊢ F ⁡ 1 = x ∧ F ⁡ 2 = z → F ⁡ 1 F ⁡ 2 = x z
46 45 eleq1d ⊢ F ⁡ 1 = x ∧ F ⁡ 2 = z → F ⁡ 1 F ⁡ 2 ∈ E ↔ x z ∈ E
47 46 3adant1 ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = x ∧ F ⁡ 2 = z → F ⁡ 1 F ⁡ 2 ∈ E ↔ x z ∈ E
48 41 44 47 3anbi123d ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = x ∧ F ⁡ 2 = z → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E ↔ y x ∈ E ∧ y z ∈ E ∧ x z ∈ E
49 38 48 imbitrrid ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = x ∧ F ⁡ 2 = z → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
50 3anrot ⊢ y z ∈ E ∧ x y ∈ E ∧ x z ∈ E ↔ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E
51 biid ⊢ y z ∈ E ↔ y z ∈ E
52 prcom ⊢ x z = z x
53 52 eleq1i ⊢ x z ∈ E ↔ z x ∈ E
54 51 36 53 3anbi123i ⊢ y z ∈ E ∧ x y ∈ E ∧ x z ∈ E ↔ y z ∈ E ∧ y x ∈ E ∧ z x ∈ E
55 50 54 sylbb1 ⊢ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → y z ∈ E ∧ y x ∈ E ∧ z x ∈ E
56 preq12 ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = z → F ⁡ 0 F ⁡ 1 = y z
57 56 eleq1d ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = z → F ⁡ 0 F ⁡ 1 ∈ E ↔ y z ∈ E
58 57 3adant3 ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = z ∧ F ⁡ 2 = x → F ⁡ 0 F ⁡ 1 ∈ E ↔ y z ∈ E
59 preq12 ⊢ F ⁡ 0 = y ∧ F ⁡ 2 = x → F ⁡ 0 F ⁡ 2 = y x
60 59 eleq1d ⊢ F ⁡ 0 = y ∧ F ⁡ 2 = x → F ⁡ 0 F ⁡ 2 ∈ E ↔ y x ∈ E
61 60 3adant2 ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = z ∧ F ⁡ 2 = x → F ⁡ 0 F ⁡ 2 ∈ E ↔ y x ∈ E
62 preq12 ⊢ F ⁡ 1 = z ∧ F ⁡ 2 = x → F ⁡ 1 F ⁡ 2 = z x
63 62 eleq1d ⊢ F ⁡ 1 = z ∧ F ⁡ 2 = x → F ⁡ 1 F ⁡ 2 ∈ E ↔ z x ∈ E
64 63 3adant1 ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = z ∧ F ⁡ 2 = x → F ⁡ 1 F ⁡ 2 ∈ E ↔ z x ∈ E
65 58 61 64 3anbi123d ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = z ∧ F ⁡ 2 = x → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E ↔ y z ∈ E ∧ y x ∈ E ∧ z x ∈ E
66 55 65 imbitrrid ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = z ∧ F ⁡ 2 = x → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
67 49 66 jaoi ⊢ F ⁡ 0 = y ∧ F ⁡ 1 = x ∧ F ⁡ 2 = z ∨ F ⁡ 0 = y ∧ F ⁡ 1 = z ∧ F ⁡ 2 = x → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
68 3anrot ⊢ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E ↔ x z ∈ E ∧ y z ∈ E ∧ x y ∈ E
69 biid ⊢ x y ∈ E ↔ x y ∈ E
70 53 19 69 3anbi123i ⊢ x z ∈ E ∧ y z ∈ E ∧ x y ∈ E ↔ z x ∈ E ∧ z y ∈ E ∧ x y ∈ E
71 68 70 sylbb ⊢ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → z x ∈ E ∧ z y ∈ E ∧ x y ∈ E
72 preq12 ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = x → F ⁡ 0 F ⁡ 1 = z x
73 72 eleq1d ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = x → F ⁡ 0 F ⁡ 1 ∈ E ↔ z x ∈ E
74 73 3adant3 ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = x ∧ F ⁡ 2 = y → F ⁡ 0 F ⁡ 1 ∈ E ↔ z x ∈ E
75 preq12 ⊢ F ⁡ 0 = z ∧ F ⁡ 2 = y → F ⁡ 0 F ⁡ 2 = z y
76 75 eleq1d ⊢ F ⁡ 0 = z ∧ F ⁡ 2 = y → F ⁡ 0 F ⁡ 2 ∈ E ↔ z y ∈ E
77 76 3adant2 ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = x ∧ F ⁡ 2 = y → F ⁡ 0 F ⁡ 2 ∈ E ↔ z y ∈ E
78 preq12 ⊢ F ⁡ 1 = x ∧ F ⁡ 2 = y → F ⁡ 1 F ⁡ 2 = x y
79 78 eleq1d ⊢ F ⁡ 1 = x ∧ F ⁡ 2 = y → F ⁡ 1 F ⁡ 2 ∈ E ↔ x y ∈ E
80 79 3adant1 ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = x ∧ F ⁡ 2 = y → F ⁡ 1 F ⁡ 2 ∈ E ↔ x y ∈ E
81 74 77 80 3anbi123d ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = x ∧ F ⁡ 2 = y → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E ↔ z x ∈ E ∧ z y ∈ E ∧ x y ∈ E
82 71 81 imbitrrid ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = x ∧ F ⁡ 2 = y → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
83 3anrev ⊢ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E ↔ y z ∈ E ∧ x z ∈ E ∧ x y ∈ E
84 19 53 36 3anbi123i ⊢ y z ∈ E ∧ x z ∈ E ∧ x y ∈ E ↔ z y ∈ E ∧ z x ∈ E ∧ y x ∈ E
85 83 84 sylbb ⊢ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → z y ∈ E ∧ z x ∈ E ∧ y x ∈ E
86 preq12 ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = y → F ⁡ 0 F ⁡ 1 = z y
87 86 eleq1d ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = y → F ⁡ 0 F ⁡ 1 ∈ E ↔ z y ∈ E
88 87 3adant3 ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = y ∧ F ⁡ 2 = x → F ⁡ 0 F ⁡ 1 ∈ E ↔ z y ∈ E
89 preq12 ⊢ F ⁡ 0 = z ∧ F ⁡ 2 = x → F ⁡ 0 F ⁡ 2 = z x
90 89 eleq1d ⊢ F ⁡ 0 = z ∧ F ⁡ 2 = x → F ⁡ 0 F ⁡ 2 ∈ E ↔ z x ∈ E
91 90 3adant2 ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = y ∧ F ⁡ 2 = x → F ⁡ 0 F ⁡ 2 ∈ E ↔ z x ∈ E
92 preq12 ⊢ F ⁡ 1 = y ∧ F ⁡ 2 = x → F ⁡ 1 F ⁡ 2 = y x
93 92 eleq1d ⊢ F ⁡ 1 = y ∧ F ⁡ 2 = x → F ⁡ 1 F ⁡ 2 ∈ E ↔ y x ∈ E
94 93 3adant1 ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = y ∧ F ⁡ 2 = x → F ⁡ 1 F ⁡ 2 ∈ E ↔ y x ∈ E
95 88 91 94 3anbi123d ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = y ∧ F ⁡ 2 = x → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E ↔ z y ∈ E ∧ z x ∈ E ∧ y x ∈ E
96 85 95 imbitrrid ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = y ∧ F ⁡ 2 = x → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
97 82 96 jaoi ⊢ F ⁡ 0 = z ∧ F ⁡ 1 = x ∧ F ⁡ 2 = y ∨ F ⁡ 0 = z ∧ F ⁡ 1 = y ∧ F ⁡ 2 = x → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
98 33 67 97 3jaoi ⊢ F ⁡ 0 = x ∧ F ⁡ 1 = y ∧ F ⁡ 2 = z ∨ F ⁡ 0 = x ∧ F ⁡ 1 = z ∧ F ⁡ 2 = y ∨ F ⁡ 0 = y ∧ F ⁡ 1 = x ∧ F ⁡ 2 = z ∨ F ⁡ 0 = y ∧ F ⁡ 1 = z ∧ F ⁡ 2 = x ∨ F ⁡ 0 = z ∧ F ⁡ 1 = x ∧ F ⁡ 2 = y ∨ F ⁡ 0 = z ∧ F ⁡ 1 = y ∧ F ⁡ 2 = x → x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
99 f1of1 ⊢ F : 0 ..^ 3 ⟶ 1-1 onto x y z → F : 0 ..^ 3 ⟶ 1-1 x y z
100 fvf1tp ⊢ F : 0 ..^ 3 ⟶ 1-1 x y z → F ⁡ 0 = x ∧ F ⁡ 1 = y ∧ F ⁡ 2 = z ∨ F ⁡ 0 = x ∧ F ⁡ 1 = z ∧ F ⁡ 2 = y ∨ F ⁡ 0 = y ∧ F ⁡ 1 = x ∧ F ⁡ 2 = z ∨ F ⁡ 0 = y ∧ F ⁡ 1 = z ∧ F ⁡ 2 = x ∨ F ⁡ 0 = z ∧ F ⁡ 1 = x ∧ F ⁡ 2 = y ∨ F ⁡ 0 = z ∧ F ⁡ 1 = y ∧ F ⁡ 2 = x
101 99 100 syl ⊢ F : 0 ..^ 3 ⟶ 1-1 onto x y z → F ⁡ 0 = x ∧ F ⁡ 1 = y ∧ F ⁡ 2 = z ∨ F ⁡ 0 = x ∧ F ⁡ 1 = z ∧ F ⁡ 2 = y ∨ F ⁡ 0 = y ∧ F ⁡ 1 = x ∧ F ⁡ 2 = z ∨ F ⁡ 0 = y ∧ F ⁡ 1 = z ∧ F ⁡ 2 = x ∨ F ⁡ 0 = z ∧ F ⁡ 1 = x ∧ F ⁡ 2 = y ∨ F ⁡ 0 = z ∧ F ⁡ 1 = y ∧ F ⁡ 2 = x
102 98 101 syl11 ⊢ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F : 0 ..^ 3 ⟶ 1-1 onto x y z → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
103 102 adantl ⊢ T = x y z ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F : 0 ..^ 3 ⟶ 1-1 onto x y z → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
104 5 103 sylbid ⊢ T = x y z ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F : 0 ..^ 3 ⟶ 1-1 onto T → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
105 104 3adant2 ⊢ T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F : 0 ..^ 3 ⟶ 1-1 onto T → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
106 105 a1i ⊢ y ∈ V ∧ z ∈ V → T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F : 0 ..^ 3 ⟶ 1-1 onto T → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
107 106 rexlimivv ⊢ ∃ y ∈ V ∃ z ∈ V T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F : 0 ..^ 3 ⟶ 1-1 onto T → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
108 107 rexlimivw ⊢ ∃ x ∈ V ∃ y ∈ V ∃ z ∈ V T = x y z ∧ T = 3 ∧ x y ∈ E ∧ x z ∈ E ∧ y z ∈ E → F : 0 ..^ 3 ⟶ 1-1 onto T → F ⁡ 0 F ⁡ 1 ∈ E ∧ F ⁡ 0 F ⁡ 2 ∈ E ∧ F ⁡ 1 F ⁡ 2 ∈ E
109 3 108 syl Could not format ( T e. ( GrTriangles ` G ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> T -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) ) : No typesetting found for |- ( T e. ( GrTriangles ` G ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> T -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) ) with typecode |-
110 109 imp Could not format ( ( T e. ( GrTriangles ` G ) /\ F : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) : No typesetting found for |- ( ( T e. ( GrTriangles ` G ) /\ F : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) with typecode |-