cycl3grtri

Description: The vertices of a cycle of size 3 are a triangle in a graph. (Contributed by AV, 5-Oct-2025)

	Ref	Expression
Hypotheses	cycl3grtri.g	$⊢ φ \to G \in UPGraph$
	cycl3grtri.c	$⊢ φ \to F Cycles (G) P$
	cycl3grtri.n	$⊢ φ \to \|F\| = 3$
Assertion	cycl3grtri	Could not format assertion : No typesetting found for \|- ( ph -> ran P e. ( GrTriangles ` G ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		cycl3grtri.g	$⊢ φ \to G \in UPGraph$
2		cycl3grtri.c	$⊢ φ \to F Cycles (G) P$
3		cycl3grtri.n	$⊢ φ \to \|F\| = 3$
4		cyclprop	$⊢ F Cycles (G) P \to (F Paths (G) P \land P (0) = P (\|F\|))$
5		tpeq1	$⊢ x = P (0) \to \{x, y, z\} = \{P (0), y, z\}$
6	5	eqeq2d	$⊢ x = P (0) \to (ran P = \{x, y, z\} \leftrightarrow ran P = \{P (0), y, z\})$
7		preq1	$⊢ x = P (0) \to \{x, y\} = \{P (0), y\}$
8	7	eleq1d	$⊢ x = P (0) \to (\{x, y\} \in Edg (G) \leftrightarrow \{P (0), y\} \in Edg (G))$
9		preq1	$⊢ x = P (0) \to \{x, z\} = \{P (0), z\}$
10	9	eleq1d	$⊢ x = P (0) \to (\{x, z\} \in Edg (G) \leftrightarrow \{P (0), z\} \in Edg (G))$
11	8 10	3anbi12d	$⊢ x = P (0) \to ((\{x, y\} \in Edg (G) \land \{x, z\} \in Edg (G) \land \{y, z\} \in Edg (G)) \leftrightarrow (\{P (0), y\} \in Edg (G) \land \{P (0), z\} \in Edg (G) \land \{y, z\} \in Edg (G)))$
12	6 11	3anbi13d	$⊢ x = P (0) \to ((ran P = \{x, y, z\} \land \|ran P\| = 3 \land (\{x, y\} \in Edg (G) \land \{x, z\} \in Edg (G) \land \{y, z\} \in Edg (G))) \leftrightarrow (ran P = \{P (0), y, z\} \land \|ran P\| = 3 \land (\{P (0), y\} \in Edg (G) \land \{P (0), z\} \in Edg (G) \land \{y, z\} \in Edg (G))))$
13		tpeq2	$⊢ y = P (1) \to \{P (0), y, z\} = \{P (0), P (1), z\}$
14	13	eqeq2d	$⊢ y = P (1) \to (ran P = \{P (0), y, z\} \leftrightarrow ran P = \{P (0), P (1), z\})$
15		preq2	$⊢ y = P (1) \to \{P (0), y\} = \{P (0), P (1)\}$
16	15	eleq1d	$⊢ y = P (1) \to (\{P (0), y\} \in Edg (G) \leftrightarrow \{P (0), P (1)\} \in Edg (G))$
17		preq1	$⊢ y = P (1) \to \{y, z\} = \{P (1), z\}$
18	17	eleq1d	$⊢ y = P (1) \to (\{y, z\} \in Edg (G) \leftrightarrow \{P (1), z\} \in Edg (G))$
19	16 18	3anbi13d	$⊢ y = P (1) \to ((\{P (0), y\} \in Edg (G) \land \{P (0), z\} \in Edg (G) \land \{y, z\} \in Edg (G)) \leftrightarrow (\{P (0), P (1)\} \in Edg (G) \land \{P (0), z\} \in Edg (G) \land \{P (1), z\} \in Edg (G)))$
20	14 19	3anbi13d	$⊢ y = P (1) \to ((ran P = \{P (0), y, z\} \land \|ran P\| = 3 \land (\{P (0), y\} \in Edg (G) \land \{P (0), z\} \in Edg (G) \land \{y, z\} \in Edg (G))) \leftrightarrow (ran P = \{P (0), P (1), z\} \land \|ran P\| = 3 \land (\{P (0), P (1)\} \in Edg (G) \land \{P (0), z\} \in Edg (G) \land \{P (1), z\} \in Edg (G))))$
21		tpeq3	$⊢ z = P (2) \to \{P (0), P (1), z\} = \{P (0), P (1), P (2)\}$
22	21	eqeq2d	$⊢ z = P (2) \to (ran P = \{P (0), P (1), z\} \leftrightarrow ran P = \{P (0), P (1), P (2)\})$
23		preq2	$⊢ z = P (2) \to \{P (0), z\} = \{P (0), P (2)\}$
24	23	eleq1d	$⊢ z = P (2) \to (\{P (0), z\} \in Edg (G) \leftrightarrow \{P (0), P (2)\} \in Edg (G))$
25		preq2	$⊢ z = P (2) \to \{P (1), z\} = \{P (1), P (2)\}$
26	25	eleq1d	$⊢ z = P (2) \to (\{P (1), z\} \in Edg (G) \leftrightarrow \{P (1), P (2)\} \in Edg (G))$
27	24 26	3anbi23d	$⊢ z = P (2) \to ((\{P (0), P (1)\} \in Edg (G) \land \{P (0), z\} \in Edg (G) \land \{P (1), z\} \in Edg (G)) \leftrightarrow (\{P (0), P (1)\} \in Edg (G) \land \{P (0), P (2)\} \in Edg (G) \land \{P (1), P (2)\} \in Edg (G)))$
28	22 27	3anbi13d	$⊢ z = P (2) \to ((ran P = \{P (0), P (1), z\} \land \|ran P\| = 3 \land (\{P (0), P (1)\} \in Edg (G) \land \{P (0), z\} \in Edg (G) \land \{P (1), z\} \in Edg (G))) \leftrightarrow (ran P = \{P (0), P (1), P (2)\} \land \|ran P\| = 3 \land (\{P (0), P (1)\} \in Edg (G) \land \{P (0), P (2)\} \in Edg (G) \land \{P (1), P (2)\} \in Edg (G))))$
29		pthiswlk	$⊢ F Paths (G) P \to F Walks (G) P$
30		eqid	$⊢ Vtx (G) = Vtx (G)$
31	30	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
32		simpl	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
33		3nn0	$⊢ 3 \in ℕ_{0}$
34		0elfz	$⊢ 3 \in ℕ_{0} \to 0 \in (0 \dots 3)$
35	33 34	ax-mp	$⊢ 0 \in (0 \dots 3)$
36		oveq2	$⊢ \|F\| = 3 \to (0 \dots \|F\|) = (0 \dots 3)$
37	35 36	eleqtrrid	$⊢ \|F\| = 3 \to 0 \in (0 \dots \|F\|)$
38	37	ad2antll	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to 0 \in (0 \dots \|F\|)$
39	32 38	ffvelcdmd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P (0) \in Vtx (G)$
40	39	ex	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to P (0) \in Vtx (G))$
41	29 31 40	3syl	$⊢ F Paths (G) P \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to P (0) \in Vtx (G))$
42	41	adantl	$⊢ (φ \land F Paths (G) P) \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to P (0) \in Vtx (G))$
43	42	imp	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P (0) \in Vtx (G)$
44		1nn0	$⊢ 1 \in ℕ_{0}$
45		1le3	$⊢ 1 \leq 3$
46		elfz2nn0	$⊢ 1 \in (0 \dots 3) \leftrightarrow (1 \in ℕ_{0} \land 3 \in ℕ_{0} \land 1 \leq 3)$
47	44 33 45 46	mpbir3an	$⊢ 1 \in (0 \dots 3)$
48	47 36	eleqtrrid	$⊢ \|F\| = 3 \to 1 \in (0 \dots \|F\|)$
49	48	ad2antll	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to 1 \in (0 \dots \|F\|)$
50	32 49	ffvelcdmd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P (1) \in Vtx (G)$
51	50	ex	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to P (1) \in Vtx (G))$
52	29 31 51	3syl	$⊢ F Paths (G) P \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to P (1) \in Vtx (G))$
53	52	adantl	$⊢ (φ \land F Paths (G) P) \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to P (1) \in Vtx (G))$
54	53	imp	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P (1) \in Vtx (G)$
55		2nn0	$⊢ 2 \in ℕ_{0}$
56		2re	$⊢ 2 \in ℝ$
57		3re	$⊢ 3 \in ℝ$
58		2lt3	$⊢ 2 < 3$
59	56 57 58	ltleii	$⊢ 2 \leq 3$
60		elfz2nn0	$⊢ 2 \in (0 \dots 3) \leftrightarrow (2 \in ℕ_{0} \land 3 \in ℕ_{0} \land 2 \leq 3)$
61	55 33 59 60	mpbir3an	$⊢ 2 \in (0 \dots 3)$
62	61 36	eleqtrrid	$⊢ \|F\| = 3 \to 2 \in (0 \dots \|F\|)$
63	62	ad2antll	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to 2 \in (0 \dots \|F\|)$
64	32 63	ffvelcdmd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P (2) \in Vtx (G)$
65	64	ex	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to P (2) \in Vtx (G))$
66	29 31 65	3syl	$⊢ F Paths (G) P \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to P (2) \in Vtx (G))$
67	66	adantl	$⊢ (φ \land F Paths (G) P) \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to P (2) \in Vtx (G))$
68	67	imp	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P (2) \in Vtx (G)$
69		fdm	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to dom P = (0 \dots \|F\|)$
70		elnn0uz	$⊢ 3 \in ℕ_{0} \leftrightarrow 3 \in ℤ_{\geq 0}$
71	33 70	mpbi	$⊢ 3 \in ℤ_{\geq 0}$
72		fzisfzounsn	$⊢ 3 \in ℤ_{\geq 0} \to (0 \dots 3) = (0 ..^3) \cup \{3\}$
73	71 72	ax-mp	$⊢ (0 \dots 3) = (0 ..^3) \cup \{3\}$
74		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
75	74	uneq1i	$⊢ (0 ..^3) \cup \{3\} = \{0, 1, 2\} \cup \{3\}$
76	73 75	eqtri	$⊢ (0 \dots 3) = \{0, 1, 2\} \cup \{3\}$
77	36 76	eqtrdi	$⊢ \|F\| = 3 \to (0 \dots \|F\|) = \{0, 1, 2\} \cup \{3\}$
78	77	adantl	$⊢ (P (0) = P (\|F\|) \land \|F\| = 3) \to (0 \dots \|F\|) = \{0, 1, 2\} \cup \{3\}$
79	69 78	sylan9eq	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to dom P = \{0, 1, 2\} \cup \{3\}$
80	79	imaeq2d	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P [dom P] = P [\{0, 1, 2\} \cup \{3\}]$
81		imadmrn	$⊢ P [dom P] = ran P$
82		imaundi	$⊢ P [\{0, 1, 2\} \cup \{3\}] = P [\{0, 1, 2\}] \cup P [\{3\}]$
83	80 81 82	3eqtr3g	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to ran P = P [\{0, 1, 2\}] \cup P [\{3\}]$
84		ffn	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to P Fn (0 \dots \|F\|)$
85	84	adantr	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P Fn (0 \dots \|F\|)$
86	85 38 49 63	fnimatpd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P [\{0, 1, 2\}] = \{P (0), P (1), P (2)\}$
87		nn0fz0	$⊢ 3 \in ℕ_{0} \leftrightarrow 3 \in (0 \dots 3)$
88	33 87	mpbi	$⊢ 3 \in (0 \dots 3)$
89	88 36	eleqtrrid	$⊢ \|F\| = 3 \to 3 \in (0 \dots \|F\|)$
90	89	adantl	$⊢ (P (0) = P (\|F\|) \land \|F\| = 3) \to 3 \in (0 \dots \|F\|)$
91		fnsnfv	$⊢ (P Fn (0 \dots \|F\|) \land 3 \in (0 \dots \|F\|)) \to \{P (3)\} = P [\{3\}]$
92	84 90 91	syl2an	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to \{P (3)\} = P [\{3\}]$
93	92	eqcomd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P [\{3\}] = \{P (3)\}$
94	86 93	uneq12d	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to P [\{0, 1, 2\}] \cup P [\{3\}] = \{P (0), P (1), P (2)\} \cup \{P (3)\}$
95		fveq2	$⊢ \|F\| = 3 \to P (\|F\|) = P (3)$
96	95	eqeq2d	$⊢ \|F\| = 3 \to (P (0) = P (\|F\|) \leftrightarrow P (0) = P (3))$
97		sneq	$⊢ P (3) = P (0) \to \{P (3)\} = \{P (0)\}$
98	97	eqcoms	$⊢ P (0) = P (3) \to \{P (3)\} = \{P (0)\}$
99	98	uneq2d	$⊢ P (0) = P (3) \to \{P (0), P (1), P (2)\} \cup \{P (3)\} = \{P (0), P (1), P (2)\} \cup \{P (0)\}$
100		snsstp1	$⊢ \{P (0)\} \subseteq \{P (0), P (1), P (2)\}$
101	100	a1i	$⊢ P (0) = P (3) \to \{P (0)\} \subseteq \{P (0), P (1), P (2)\}$
102		ssequn2	$⊢ \{P (0)\} \subseteq \{P (0), P (1), P (2)\} \leftrightarrow \{P (0), P (1), P (2)\} \cup \{P (0)\} = \{P (0), P (1), P (2)\}$
103	101 102	sylib	$⊢ P (0) = P (3) \to \{P (0), P (1), P (2)\} \cup \{P (0)\} = \{P (0), P (1), P (2)\}$
104	99 103	eqtrd	$⊢ P (0) = P (3) \to \{P (0), P (1), P (2)\} \cup \{P (3)\} = \{P (0), P (1), P (2)\}$
105	96 104	biimtrdi	$⊢ \|F\| = 3 \to (P (0) = P (\|F\|) \to \{P (0), P (1), P (2)\} \cup \{P (3)\} = \{P (0), P (1), P (2)\})$
106	105	impcom	$⊢ (P (0) = P (\|F\|) \land \|F\| = 3) \to \{P (0), P (1), P (2)\} \cup \{P (3)\} = \{P (0), P (1), P (2)\}$
107	106	adantl	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to \{P (0), P (1), P (2)\} \cup \{P (3)\} = \{P (0), P (1), P (2)\}$
108	83 94 107	3eqtrd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to ran P = \{P (0), P (1), P (2)\}$
109	108	ex	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to ran P = \{P (0), P (1), P (2)\})$
110	29 31 109	3syl	$⊢ F Paths (G) P \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to ran P = \{P (0), P (1), P (2)\})$
111	110	adantl	$⊢ (φ \land F Paths (G) P) \to ((P (0) = P (\|F\|) \land \|F\| = 3) \to ran P = \{P (0), P (1), P (2)\})$
112	111	imp	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to ran P = \{P (0), P (1), P (2)\}$
113		breq2	$⊢ \|F\| = 3 \to (1 \leq \|F\| \leftrightarrow 1 \leq 3)$
114	45 113	mpbiri	$⊢ \|F\| = 3 \to 1 \leq \|F\|$
115	114	ad2antll	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to 1 \leq \|F\|$
116	2	ad2antrr	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to F Cycles (G) P$
117		cyclnumvtx	$⊢ (1 \leq \|F\| \land F Cycles (G) P) \to \|ran P\| = \|F\|$
118	115 116 117	syl2anc	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to \|ran P\| = \|F\|$
119	3	ad2antrr	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to \|F\| = 3$
120	118 119	eqtrd	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to \|ran P\| = 3$
121		cycl3grtrilem	$⊢ ((G \in UPGraph \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to (\{P (0), P (1)\} \in Edg (G) \land \{P (0), P (2)\} \in Edg (G) \land \{P (1), P (2)\} \in Edg (G))$
122	1 121	sylanl1	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to (\{P (0), P (1)\} \in Edg (G) \land \{P (0), P (2)\} \in Edg (G) \land \{P (1), P (2)\} \in Edg (G))$
123	112 120 122	3jca	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to (ran P = \{P (0), P (1), P (2)\} \land \|ran P\| = 3 \land (\{P (0), P (1)\} \in Edg (G) \land \{P (0), P (2)\} \in Edg (G) \land \{P (1), P (2)\} \in Edg (G)))$
124	12 20 28 43 54 68 123	3rspcedvdw	$⊢ ((φ \land F Paths (G) P) \land (P (0) = P (\|F\|) \land \|F\| = 3)) \to \exists x \in Vtx (G) \exists y \in Vtx (G) \exists z \in Vtx (G) (ran P = \{x, y, z\} \land \|ran P\| = 3 \land (\{x, y\} \in Edg (G) \land \{x, z\} \in Edg (G) \land \{y, z\} \in Edg (G)))$
125		eqid	$⊢ Edg (G) = Edg (G)$
126	30 125	isgrtri	Could not format ( ran P e. ( GrTriangles ` G ) <-> E. x e. ( Vtx ` G ) E. y e. ( Vtx ` G ) E. z e. ( Vtx ` G ) ( ran P = { x , y , z } /\ ( # ` ran P ) = 3 /\ ( { x , y } e. ( Edg ` G ) /\ { x , z } e. ( Edg ` G ) /\ { y , z } e. ( Edg ` G ) ) ) ) : No typesetting found for \|- ( ran P e. ( GrTriangles ` G ) <-> E. x e. ( Vtx ` G ) E. y e. ( Vtx ` G ) E. z e. ( Vtx ` G ) ( ran P = { x , y , z } /\ ( # ` ran P ) = 3 /\ ( { x , y } e. ( Edg ` G ) /\ { x , z } e. ( Edg ` G ) /\ { y , z } e. ( Edg ` G ) ) ) ) with typecode \|-
127	124 126	sylibr	Could not format ( ( ( ph /\ F ( Paths ` G ) P ) /\ ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) ) -> ran P e. ( GrTriangles ` G ) ) : No typesetting found for \|- ( ( ( ph /\ F ( Paths ` G ) P ) /\ ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) ) -> ran P e. ( GrTriangles ` G ) ) with typecode \|-
128	127	exp32	Could not format ( ( ph /\ F ( Paths ` G ) P ) -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( ( # ` F ) = 3 -> ran P e. ( GrTriangles ` G ) ) ) ) : No typesetting found for \|- ( ( ph /\ F ( Paths ` G ) P ) -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( ( # ` F ) = 3 -> ran P e. ( GrTriangles ` G ) ) ) ) with typecode \|-
129	128	com23	Could not format ( ( ph /\ F ( Paths ` G ) P ) -> ( ( # ` F ) = 3 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ran P e. ( GrTriangles ` G ) ) ) ) : No typesetting found for \|- ( ( ph /\ F ( Paths ` G ) P ) -> ( ( # ` F ) = 3 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ran P e. ( GrTriangles ` G ) ) ) ) with typecode \|-
130	129	expcom	Could not format ( F ( Paths ` G ) P -> ( ph -> ( ( # ` F ) = 3 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ran P e. ( GrTriangles ` G ) ) ) ) ) : No typesetting found for \|- ( F ( Paths ` G ) P -> ( ph -> ( ( # ` F ) = 3 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ran P e. ( GrTriangles ` G ) ) ) ) ) with typecode \|-
131	130	com24	Could not format ( F ( Paths ` G ) P -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( ( # ` F ) = 3 -> ( ph -> ran P e. ( GrTriangles ` G ) ) ) ) ) : No typesetting found for \|- ( F ( Paths ` G ) P -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( ( # ` F ) = 3 -> ( ph -> ran P e. ( GrTriangles ` G ) ) ) ) ) with typecode \|-
132	131	imp	Could not format ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 3 -> ( ph -> ran P e. ( GrTriangles ` G ) ) ) ) : No typesetting found for \|- ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 3 -> ( ph -> ran P e. ( GrTriangles ` G ) ) ) ) with typecode \|-
133	4 132	syl	Could not format ( F ( Cycles ` G ) P -> ( ( # ` F ) = 3 -> ( ph -> ran P e. ( GrTriangles ` G ) ) ) ) : No typesetting found for \|- ( F ( Cycles ` G ) P -> ( ( # ` F ) = 3 -> ( ph -> ran P e. ( GrTriangles ` G ) ) ) ) with typecode \|-
134	133	com13	Could not format ( ph -> ( ( # ` F ) = 3 -> ( F ( Cycles ` G ) P -> ran P e. ( GrTriangles ` G ) ) ) ) : No typesetting found for \|- ( ph -> ( ( # ` F ) = 3 -> ( F ( Cycles ` G ) P -> ran P e. ( GrTriangles ` G ) ) ) ) with typecode \|-
135	3 2 134	mp2d	Could not format ( ph -> ran P e. ( GrTriangles ` G ) ) : No typesetting found for \|- ( ph -> ran P e. ( GrTriangles ` G ) ) with typecode \|-

Metamath Proof Explorer

Theorem cycl3grtri

Proof