grtriprop

	Ref	Expression
Hypotheses	grtri.v	$⊢ V = Vtx (G)$
	grtri.e	$⊢ E = Edg (G)$
Assertion	grtriprop	Could not format assertion : 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 \|-

Proof

Step	Hyp	Ref	Expression
1		grtri.v	$⊢ V = Vtx (G)$
2		grtri.e	$⊢ E = Edg (G)$
3		elfvex	Could not format ( T e. ( GrTriangles ` G ) -> G e. _V ) : No typesetting found for \|- ( T e. ( GrTriangles ` G ) -> G e. _V ) with typecode \|-
4	1 2	grtri	Could not format ( G e. _V -> ( GrTriangles ` G ) = { t e. ~P V \| E. f ( 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 \|- ( G e. _V -> ( GrTriangles ` G ) = { t e. ~P V \| E. f ( 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 \|-
5	3 4	syl	Could not format ( T e. ( GrTriangles ` G ) -> ( GrTriangles ` G ) = { t e. ~P V \| E. f ( 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 ) -> ( GrTriangles ` G ) = { t e. ~P V \| E. f ( 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 \|-
6	5	eleq2d	Could not format ( T e. ( GrTriangles ` G ) -> ( T e. ( GrTriangles ` G ) <-> T e. { t e. ~P V \| E. f ( 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 ) -> ( T e. ( GrTriangles ` G ) <-> T e. { t e. ~P V \| E. f ( 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 \|-
7		f1oeq3	$⊢ t = T \to (f : (0 ..^3) \underset{1-1 onto}{⟶} t \leftrightarrow f : (0 ..^3) \underset{1-1 onto}{⟶} T)$
8	7	anbi1d	$⊢ t = T \to ((f : (0 ..^3) \underset{1-1 onto}{⟶} t \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \leftrightarrow (f : (0 ..^3) \underset{1-1 onto}{⟶} T \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)))$
9	8	exbidv	$⊢ t = T \to (\exists f (f : (0 ..^3) \underset{1-1 onto}{⟶} t \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \leftrightarrow \exists f (f : (0 ..^3) \underset{1-1 onto}{⟶} T \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)))$
10	9	elrab	$⊢ T \in \{t \in 𝒫 V \| \exists f (f : (0 ..^3) \underset{1-1 onto}{⟶} t \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E))\} \leftrightarrow (T \in 𝒫 V \land \exists f (f : (0 ..^3) \underset{1-1 onto}{⟶} T \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)))$
11	6 10	bitrdi	Could not format ( T e. ( GrTriangles ` G ) -> ( T e. ( GrTriangles ` G ) <-> ( T e. ~P V /\ E. f ( 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 ) -> ( T e. ( GrTriangles ` G ) <-> ( T e. ~P V /\ E. f ( 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 \|-
12		ovexd	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to (0 ..^3) \in V$
13		simpr	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to f : (0 ..^3) \underset{1-1 onto}{⟶} T$
14	12 13	hasheqf1od	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to \|(0 ..^3)\| = \|T\|$
15		eqcom	$⊢ \|(0 ..^3)\| = \|T\| \leftrightarrow \|T\| = \|(0 ..^3)\|$
16		3nn0	$⊢ 3 \in ℕ_{0}$
17		hashfzo0	$⊢ 3 \in ℕ_{0} \to \|(0 ..^3)\| = 3$
18	16 17	mp1i	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to \|(0 ..^3)\| = 3$
19	18	eqeq2d	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to (\|T\| = \|(0 ..^3)\| \leftrightarrow \|T\| = 3)$
20	15 19	bitrid	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to (\|(0 ..^3)\| = \|T\| \leftrightarrow \|T\| = 3)$
21		hash3tpb	$⊢ T \in 𝒫 V \to (\|T\| = 3 \leftrightarrow \exists x \in T \exists y \in T \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}))$
22	21	adantr	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to (\|T\| = 3 \leftrightarrow \exists x \in T \exists y \in T \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}))$
23	22	biimpa	$⊢ ((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \to \exists x \in T \exists y \in T \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\})$
24		elpwi	$⊢ T \in 𝒫 V \to T \subseteq V$
25		ss2rexv	$⊢ T \subseteq V \to (\exists x \in T \exists y \in T \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists x \in V \exists y \in V \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}))$
26		ssrexv	$⊢ T \subseteq V \to (\exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}))$
27	26	reximdv	$⊢ T \subseteq V \to (\exists y \in V \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists y \in V \exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}))$
28	27	reximdv	$⊢ T \subseteq V \to (\exists x \in V \exists y \in V \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists x \in V \exists y \in V \exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}))$
29	25 28	syld	$⊢ T \subseteq V \to (\exists x \in T \exists y \in T \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists x \in V \exists y \in V \exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}))$
30	24 29	syl	$⊢ T \in 𝒫 V \to (\exists x \in T \exists y \in T \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists x \in V \exists y \in V \exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}))$
31	30	adantr	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to (\exists x \in T \exists y \in T \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists x \in V \exists y \in V \exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}))$
32	31	adantr	$⊢ ((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \to (\exists x \in T \exists y \in T \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists x \in V \exists y \in V \exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}))$
33		simprr	$⊢ ((((((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \land (x \in V \land y \in V)) \land z \in V) \land ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\})) \to T = \{x, y, z\}$
34		simp-5r	$⊢ ((((((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \land (x \in V \land y \in V)) \land z \in V) \land ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\})) \to \|T\| = 3$
35		f1oeq3	$⊢ T = \{x, y, z\} \to (f : (0 ..^3) \underset{1-1 onto}{⟶} T \leftrightarrow f : (0 ..^3) \underset{1-1 onto}{⟶} \{x, y, z\})$
36		grtriproplem	$⊢ (f : (0 ..^3) \underset{1-1 onto}{⟶} \{x, y, z\} \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
37	36	2a1d	$⊢ (f : (0 ..^3) \underset{1-1 onto}{⟶} \{x, y, z\} \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \to ((x \in V \land y \in V) \to (z \in V \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)))$
38	37	ex	$⊢ f : (0 ..^3) \underset{1-1 onto}{⟶} \{x, y, z\} \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to ((x \in V \land y \in V) \to (z \in V \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))))$
39	38	a1d	$⊢ f : (0 ..^3) \underset{1-1 onto}{⟶} \{x, y, z\} \to (\|T\| = 3 \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to ((x \in V \land y \in V) \to (z \in V \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)))))$
40	35 39	biimtrdi	$⊢ T = \{x, y, z\} \to (f : (0 ..^3) \underset{1-1 onto}{⟶} T \to (\|T\| = 3 \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to ((x \in V \land y \in V) \to (z \in V \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))))))$
41	40	adantld	$⊢ T = \{x, y, z\} \to ((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to (\|T\| = 3 \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to ((x \in V \land y \in V) \to (z \in V \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))))))$
42	41	imp4c	$⊢ T = \{x, y, z\} \to ((((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \to ((x \in V \land y \in V) \to (z \in V \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))))$
43	42	imp4c	$⊢ T = \{x, y, z\} \to ((((((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \land (x \in V \land y \in V)) \land z \in V) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
44	43	adantl	$⊢ ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to ((((((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \land (x \in V \land y \in V)) \land z \in V) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
45	44	impcom	$⊢ ((((((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \land (x \in V \land y \in V)) \land z \in V) \land ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\})) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
46	33 34 45	3jca	$⊢ ((((((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \land (x \in V \land y \in V)) \land z \in V) \land ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\})) \to (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
47	46	ex	$⊢ (((((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \land (x \in V \land y \in V)) \land z \in V) \to (((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)))$
48	47	reximdva	$⊢ ((((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \land (x \in V \land y \in V)) \to (\exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)))$
49	48	reximdvva	$⊢ (((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \to (\exists x \in V \exists y \in V \exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)))$
50	49	ex	$⊢ ((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\exists x \in V \exists y \in V \exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))))$
51	50	com23	$⊢ ((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \to (\exists x \in V \exists y \in V \exists z \in V ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))))$
52	32 51	syld	$⊢ ((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \to (\exists x \in T \exists y \in T \exists z \in T ((x \neq y \land x \neq z \land y \neq z) \land T = \{x, y, z\}) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))))$
53	23 52	mpd	$⊢ ((T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \land \|T\| = 3) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)))$
54	53	ex	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to (\|T\| = 3 \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))))$
55	20 54	sylbid	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to (\|(0 ..^3)\| = \|T\| \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))))$
56	14 55	mpd	$⊢ (T \in 𝒫 V \land f : (0 ..^3) \underset{1-1 onto}{⟶} T) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)))$
57	56	expimpd	$⊢ T \in 𝒫 V \to ((f : (0 ..^3) \underset{1-1 onto}{⟶} T \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)))$
58	57	exlimdv	$⊢ T \in 𝒫 V \to (\exists f (f : (0 ..^3) \underset{1-1 onto}{⟶} T \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)))$
59	58	imp	$⊢ (T \in 𝒫 V \land \exists f (f : (0 ..^3) \underset{1-1 onto}{⟶} T \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E))) \to \exists x \in V \exists y \in V \exists z \in V (T = \{x, y, z\} \land \|T\| = 3 \land (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
60	11 59	biimtrdi	Could not format ( T e. ( GrTriangles ` G ) -> ( 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 ) -> ( 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 \|-
61	60	pm2.43i	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 \|-

Metamath Proof Explorer

Theorem grtriprop

Proof