grlimgrtri

Description: If one of two locally isomorphic graphs has a triangle, so does the other. The triangle in the other graph is not necessarily the image ( F " T ) of the triangle T in the first graph. (Contributed by AV, 24-Aug-2025)

	Ref	Expression
Hypotheses	grlimgrtri.g	$⊢ φ \to G \in USHGraph$
	grlimgrtri.h	$⊢ φ \to H \in USHGraph$
	grlimgrtri.n	$⊢ φ \to F \in (G GraphLocIso H)$
	grlimgrtri.t	No typesetting found for \|- ( ph -> T e. ( GrTriangles ` G ) ) with typecode \|-
Assertion	grlimgrtri	Could not format assertion : No typesetting found for \|- ( ph -> E. t t e. ( GrTriangles ` H ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		grlimgrtri.g	$⊢ φ \to G \in USHGraph$
2		grlimgrtri.h	$⊢ φ \to H \in USHGraph$
3		grlimgrtri.n	$⊢ φ \to F \in (G GraphLocIso H)$
4		grlimgrtri.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	$⊢ φ \to \exists a \in Vtx (G) \exists b \in Vtx (G) \exists c \in Vtx (G) (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))$
9	1 2 3	3jca	$⊢ φ \to (G \in USHGraph \land H \in USHGraph \land F \in (G GraphLocIso H))$
10		eqid	$⊢ Vtx (H) = Vtx (H)$
11		eqid	$⊢ G ClNeighbVtx v = G ClNeighbVtx v$
12		eqid	$⊢ H ClNeighbVtx F (v) = H ClNeighbVtx F (v)$
13		eqid	$⊢ Edg (H) = Edg (H)$
14		sseq1	$⊢ y = x \to (y \subseteq G ClNeighbVtx v \leftrightarrow x \subseteq G ClNeighbVtx v)$
15	14	cbvrabv	$⊢ \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} = \{x \in Edg (G) \| x \subseteq G ClNeighbVtx v\}$
16		sseq1	$⊢ y = x \to (y \subseteq H ClNeighbVtx F (v) \leftrightarrow x \subseteq H ClNeighbVtx F (v))$
17	16	cbvrabv	$⊢ \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} = \{x \in Edg (H) \| x \subseteq H ClNeighbVtx F (v)\}$
18	5 10 11 12 6 13 15 17	usgrlimprop	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in (G GraphLocIso H)) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \land \forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i))))$
19		eqidd	$⊢ v = a \to f = f$
20		oveq2	$⊢ v = a \to G ClNeighbVtx v = G ClNeighbVtx a$
21		fveq2	$⊢ v = a \to F (v) = F (a)$
22	21	oveq2d	$⊢ v = a \to H ClNeighbVtx F (v) = H ClNeighbVtx F (a)$
23	19 20 22	f1oeq123d	$⊢ v = a \to (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \leftrightarrow f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a))$
24		eqidd	$⊢ v = a \to g = g$
25	20	sseq2d	$⊢ v = a \to (y \subseteq G ClNeighbVtx v \leftrightarrow y \subseteq G ClNeighbVtx a)$
26	25	rabbidv	$⊢ v = a \to \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} = \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}$
27	22	sseq2d	$⊢ v = a \to (y \subseteq H ClNeighbVtx F (v) \leftrightarrow y \subseteq H ClNeighbVtx F (a))$
28	27	rabbidv	$⊢ v = a \to \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} = \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\}$
29	24 26 28	f1oeq123d	$⊢ v = a \to (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \leftrightarrow g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\})$
30	26	raleqdv	$⊢ v = a \to (\forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i) \leftrightarrow \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i))$
31	29 30	anbi12d	$⊢ v = a \to ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i)) \leftrightarrow (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)))$
32	31	exbidv	$⊢ v = a \to (\exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i)) \leftrightarrow \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)))$
33	23 32	anbi12d	$⊢ v = a \to ((f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i))) \leftrightarrow (f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i))))$
34	33	exbidv	$⊢ v = a \to (\exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i))) \leftrightarrow \exists f (f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i))))$
35	34	rspcv	$⊢ a \in Vtx (G) \to (\forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i))) \to \exists f (f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i))))$
36	35	3ad2ant1	$⊢ (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \to (\forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i))) \to \exists f (f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i))))$
37	36	adantl	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to (\forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i))) \to \exists f (f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i))))$
38		tpex	$⊢ \{f (a), f (b), f (c)\} \in V$
39	38	a1i	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to \{f (a), f (b), f (c)\} \in V$
40		f1of1	$⊢ f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \to f : G ClNeighbVtx a \underset{1-1}{⟶} H ClNeighbVtx F (a)$
41	40	3ad2ant2	$⊢ ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \to f : G ClNeighbVtx a \underset{1-1}{⟶} H ClNeighbVtx F (a)$
42	41	3ad2ant2	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to f : G ClNeighbVtx a \underset{1-1}{⟶} H ClNeighbVtx F (a)$
43	5	clnbgrvtxel	$⊢ a \in Vtx (G) \to a \in (G ClNeighbVtx a)$
44	43	3ad2ant1	$⊢ (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \to a \in (G ClNeighbVtx a)$
45	44	adantr	$⊢ ((a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to a \in (G ClNeighbVtx a)$
46		simplr	$⊢ ((a \in Vtx (G) \land b \in Vtx (G)) \land \{a, b\} \in Edg (G)) \to b \in Vtx (G)$
47		simpll	$⊢ ((a \in Vtx (G) \land b \in Vtx (G)) \land \{a, b\} \in Edg (G)) \to a \in Vtx (G)$
48		simpr	$⊢ ((a \in Vtx (G) \land b \in Vtx (G)) \land \{a, b\} \in Edg (G)) \to \{a, b\} \in Edg (G)$
49	5 6	predgclnbgrel	$⊢ (b \in Vtx (G) \land a \in Vtx (G) \land \{a, b\} \in Edg (G)) \to b \in (G ClNeighbVtx a)$
50	46 47 48 49	syl3anc	$⊢ ((a \in Vtx (G) \land b \in Vtx (G)) \land \{a, b\} \in Edg (G)) \to b \in (G ClNeighbVtx a)$
51	50	2a1d	$⊢ ((a \in Vtx (G) \land b \in Vtx (G)) \land \{a, b\} \in Edg (G)) \to (\{a, c\} \in Edg (G) \to (\{b, c\} \in Edg (G) \to b \in (G ClNeighbVtx a)))$
52	51	ex	$⊢ (a \in Vtx (G) \land b \in Vtx (G)) \to (\{a, b\} \in Edg (G) \to (\{a, c\} \in Edg (G) \to (\{b, c\} \in Edg (G) \to b \in (G ClNeighbVtx a))))$
53	52	3impd	$⊢ (a \in Vtx (G) \land b \in Vtx (G)) \to ((\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)) \to b \in (G ClNeighbVtx a))$
54	53	3adant3	$⊢ (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \to ((\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)) \to b \in (G ClNeighbVtx a))$
55	54	imp	$⊢ ((a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to b \in (G ClNeighbVtx a)$
56		simplr	$⊢ ((a \in Vtx (G) \land c \in Vtx (G)) \land \{a, c\} \in Edg (G)) \to c \in Vtx (G)$
57		simpll	$⊢ ((a \in Vtx (G) \land c \in Vtx (G)) \land \{a, c\} \in Edg (G)) \to a \in Vtx (G)$
58		simpr	$⊢ ((a \in Vtx (G) \land c \in Vtx (G)) \land \{a, c\} \in Edg (G)) \to \{a, c\} \in Edg (G)$
59	5 6	predgclnbgrel	$⊢ (c \in Vtx (G) \land a \in Vtx (G) \land \{a, c\} \in Edg (G)) \to c \in (G ClNeighbVtx a)$
60	56 57 58 59	syl3anc	$⊢ ((a \in Vtx (G) \land c \in Vtx (G)) \land \{a, c\} \in Edg (G)) \to c \in (G ClNeighbVtx a)$
61	60	a1d	$⊢ ((a \in Vtx (G) \land c \in Vtx (G)) \land \{a, c\} \in Edg (G)) \to (\{b, c\} \in Edg (G) \to c \in (G ClNeighbVtx a))$
62	61	ex	$⊢ (a \in Vtx (G) \land c \in Vtx (G)) \to (\{a, c\} \in Edg (G) \to (\{b, c\} \in Edg (G) \to c \in (G ClNeighbVtx a)))$
63	62	a1d	$⊢ (a \in Vtx (G) \land c \in Vtx (G)) \to (\{a, b\} \in Edg (G) \to (\{a, c\} \in Edg (G) \to (\{b, c\} \in Edg (G) \to c \in (G ClNeighbVtx a))))$
64	63	3impd	$⊢ (a \in Vtx (G) \land c \in Vtx (G)) \to ((\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)) \to c \in (G ClNeighbVtx a))$
65	64	3adant2	$⊢ (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \to ((\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)) \to c \in (G ClNeighbVtx a))$
66	65	imp	$⊢ ((a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to c \in (G ClNeighbVtx a)$
67	45 55 66	3jca	$⊢ ((a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to (a \in (G ClNeighbVtx a) \land b \in (G ClNeighbVtx a) \land c \in (G ClNeighbVtx a))$
68	67	ex	$⊢ (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \to ((\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)) \to (a \in (G ClNeighbVtx a) \land b \in (G ClNeighbVtx a) \land c \in (G ClNeighbVtx a)))$
69	68	2a1d	$⊢ (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \to (T = \{a, b, c\} \to (\|T\| = 3 \to ((\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)) \to (a \in (G ClNeighbVtx a) \land b \in (G ClNeighbVtx a) \land c \in (G ClNeighbVtx a)))))$
70	69	3impd	$⊢ (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to (a \in (G ClNeighbVtx a) \land b \in (G ClNeighbVtx a) \land c \in (G ClNeighbVtx a)))$
71	70	a1d	$⊢ (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G)) \to (((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to (a \in (G ClNeighbVtx a) \land b \in (G ClNeighbVtx a) \land c \in (G ClNeighbVtx a))))$
72	71	adantl	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to (((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to (a \in (G ClNeighbVtx a) \land b \in (G ClNeighbVtx a) \land c \in (G ClNeighbVtx a))))$
73	72	3imp	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to (a \in (G ClNeighbVtx a) \land b \in (G ClNeighbVtx a) \land c \in (G ClNeighbVtx a))$
74		3simpa	$⊢ (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to (T = \{a, b, c\} \land \|T\| = 3)$
75	74	3ad2ant3	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to (T = \{a, b, c\} \land \|T\| = 3)$
76	73 75	jca	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to ((a \in (G ClNeighbVtx a) \land b \in (G ClNeighbVtx a) \land c \in (G ClNeighbVtx a)) \land (T = \{a, b, c\} \land \|T\| = 3))$
77		grtrimap	$⊢ f : G ClNeighbVtx a \underset{1-1}{⟶} H ClNeighbVtx F (a) \to (((a \in (G ClNeighbVtx a) \land b \in (G ClNeighbVtx a) \land c \in (G ClNeighbVtx a)) \land (T = \{a, b, c\} \land \|T\| = 3)) \to ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3))$
78	42 76 77	sylc	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)$
79		tpeq1	$⊢ x = f (a) \to \{x, y, z\} = \{f (a), y, z\}$
80	79	eqeq2d	$⊢ x = f (a) \to (\{f (a), f (b), f (c)\} = \{x, y, z\} \leftrightarrow \{f (a), f (b), f (c)\} = \{f (a), y, z\})$
81		preq1	$⊢ x = f (a) \to \{x, y\} = \{f (a), y\}$
82	81	eleq1d	$⊢ x = f (a) \to (\{x, y\} \in Edg (H) \leftrightarrow \{f (a), y\} \in Edg (H))$
83		preq1	$⊢ x = f (a) \to \{x, z\} = \{f (a), z\}$
84	83	eleq1d	$⊢ x = f (a) \to (\{x, z\} \in Edg (H) \leftrightarrow \{f (a), z\} \in Edg (H))$
85	82 84	3anbi12d	$⊢ x = f (a) \to ((\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H)) \leftrightarrow (\{f (a), y\} \in Edg (H) \land \{f (a), z\} \in Edg (H) \land \{y, z\} \in Edg (H)))$
86	80 85	3anbi13d	$⊢ x = f (a) \to ((\{f (a), f (b), f (c)\} = \{x, y, z\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))) \leftrightarrow (\{f (a), f (b), f (c)\} = \{f (a), y, z\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{f (a), y\} \in Edg (H) \land \{f (a), z\} \in Edg (H) \land \{y, z\} \in Edg (H))))$
87		tpeq2	$⊢ y = f (b) \to \{f (a), y, z\} = \{f (a), f (b), z\}$
88	87	eqeq2d	$⊢ y = f (b) \to (\{f (a), f (b), f (c)\} = \{f (a), y, z\} \leftrightarrow \{f (a), f (b), f (c)\} = \{f (a), f (b), z\})$
89		preq2	$⊢ y = f (b) \to \{f (a), y\} = \{f (a), f (b)\}$
90	89	eleq1d	$⊢ y = f (b) \to (\{f (a), y\} \in Edg (H) \leftrightarrow \{f (a), f (b)\} \in Edg (H))$
91		preq1	$⊢ y = f (b) \to \{y, z\} = \{f (b), z\}$
92	91	eleq1d	$⊢ y = f (b) \to (\{y, z\} \in Edg (H) \leftrightarrow \{f (b), z\} \in Edg (H))$
93	90 92	3anbi13d	$⊢ y = f (b) \to ((\{f (a), y\} \in Edg (H) \land \{f (a), z\} \in Edg (H) \land \{y, z\} \in Edg (H)) \leftrightarrow (\{f (a), f (b)\} \in Edg (H) \land \{f (a), z\} \in Edg (H) \land \{f (b), z\} \in Edg (H)))$
94	88 93	3anbi13d	$⊢ y = f (b) \to ((\{f (a), f (b), f (c)\} = \{f (a), y, z\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{f (a), y\} \in Edg (H) \land \{f (a), z\} \in Edg (H) \land \{y, z\} \in Edg (H))) \leftrightarrow (\{f (a), f (b), f (c)\} = \{f (a), f (b), z\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{f (a), f (b)\} \in Edg (H) \land \{f (a), z\} \in Edg (H) \land \{f (b), z\} \in Edg (H))))$
95		tpeq3	$⊢ z = f (c) \to \{f (a), f (b), z\} = \{f (a), f (b), f (c)\}$
96	95	eqeq2d	$⊢ z = f (c) \to (\{f (a), f (b), f (c)\} = \{f (a), f (b), z\} \leftrightarrow \{f (a), f (b), f (c)\} = \{f (a), f (b), f (c)\})$
97		preq2	$⊢ z = f (c) \to \{f (a), z\} = \{f (a), f (c)\}$
98	97	eleq1d	$⊢ z = f (c) \to (\{f (a), z\} \in Edg (H) \leftrightarrow \{f (a), f (c)\} \in Edg (H))$
99		preq2	$⊢ z = f (c) \to \{f (b), z\} = \{f (b), f (c)\}$
100	99	eleq1d	$⊢ z = f (c) \to (\{f (b), z\} \in Edg (H) \leftrightarrow \{f (b), f (c)\} \in Edg (H))$
101	98 100	3anbi23d	$⊢ z = f (c) \to ((\{f (a), f (b)\} \in Edg (H) \land \{f (a), z\} \in Edg (H) \land \{f (b), z\} \in Edg (H)) \leftrightarrow (\{f (a), f (b)\} \in Edg (H) \land \{f (a), f (c)\} \in Edg (H) \land \{f (b), f (c)\} \in Edg (H)))$
102	96 101	3anbi13d	$⊢ z = f (c) \to ((\{f (a), f (b), f (c)\} = \{f (a), f (b), z\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{f (a), f (b)\} \in Edg (H) \land \{f (a), z\} \in Edg (H) \land \{f (b), z\} \in Edg (H))) \leftrightarrow (\{f (a), f (b), f (c)\} = \{f (a), f (b), f (c)\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{f (a), f (b)\} \in Edg (H) \land \{f (a), f (c)\} \in Edg (H) \land \{f (b), f (c)\} \in Edg (H))))$
103	10	clnbgrisvtx	$⊢ f (a) \in (H ClNeighbVtx F (a)) \to f (a) \in Vtx (H)$
104	103	3ad2ant1	$⊢ (f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \to f (a) \in Vtx (H)$
105	104	3ad2ant1	$⊢ ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3) \to f (a) \in Vtx (H)$
106	105	adantl	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to f (a) \in Vtx (H)$
107	10	clnbgrisvtx	$⊢ f (b) \in (H ClNeighbVtx F (a)) \to f (b) \in Vtx (H)$
108	107	3ad2ant2	$⊢ (f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \to f (b) \in Vtx (H)$
109	108	3ad2ant1	$⊢ ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3) \to f (b) \in Vtx (H)$
110	109	adantl	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to f (b) \in Vtx (H)$
111	10	clnbgrisvtx	$⊢ f (c) \in (H ClNeighbVtx F (a)) \to f (c) \in Vtx (H)$
112	111	3ad2ant3	$⊢ (f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \to f (c) \in Vtx (H)$
113	112	3ad2ant1	$⊢ ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3) \to f (c) \in Vtx (H)$
114	113	adantl	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to f (c) \in Vtx (H)$
115		eqidd	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to \{f (a), f (b), f (c)\} = \{f (a), f (b), f (c)\}$
116		fveq2	$⊢ \{f (a), f (b), f (c)\} = f [T] \to \|\{f (a), f (b), f (c)\}\| = \|f [T]\|$
117	116	eqcoms	$⊢ f [T] = \{f (a), f (b), f (c)\} \to \|\{f (a), f (b), f (c)\}\| = \|f [T]\|$
118	117	3ad2ant2	$⊢ ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3) \to \|\{f (a), f (b), f (c)\}\| = \|f [T]\|$
119		simp3	$⊢ ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3) \to \|f [T]\| = 3$
120	118 119	eqtrd	$⊢ ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3) \to \|\{f (a), f (b), f (c)\}\| = 3$
121	120	adantl	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to \|\{f (a), f (b), f (c)\}\| = 3$
122		uspgruhgr	$⊢ G \in USHGraph \to G \in UHGraph$
123	1 122	syl	$⊢ φ \to G \in UHGraph$
124	123	adantr	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to G \in UHGraph$
125		simp3	$⊢ (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))$
126	124 125	anim12i	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to (G \in UHGraph \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))$
127	126	3adant2	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to (G \in UHGraph \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))$
128	127	adantr	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to (G \in UHGraph \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))$
129		eqid	$⊢ G ClNeighbVtx a = G ClNeighbVtx a$
130		eqid	$⊢ \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} = \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}$
131	5 129 6 130	grlimgrtrilem1	$⊢ (G \in UHGraph \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to (\{a, b\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{a, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{b, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\})$
132	128 131	syl	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to (\{a, b\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{a, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{b, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\})$
133		eqid	$⊢ H ClNeighbVtx F (a) = H ClNeighbVtx F (a)$
134		eqid	$⊢ \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} = \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\}$
135	5 129 6 130 133 13 134	grlimgrtrilem2	$⊢ ((f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\}) \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i) \land \{a, b\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}) \to \{f (a), f (b)\} \in Edg (H)$
136	135	3expia	$⊢ ((f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\}) \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \to (\{a, b\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \to \{f (a), f (b)\} \in Edg (H))$
137	5 129 6 130 133 13 134	grlimgrtrilem2	$⊢ ((f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\}) \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i) \land \{a, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}) \to \{f (a), f (c)\} \in Edg (H)$
138	137	3expia	$⊢ ((f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\}) \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \to (\{a, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \to \{f (a), f (c)\} \in Edg (H))$
139	5 129 6 130 133 13 134	grlimgrtrilem2	$⊢ ((f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\}) \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i) \land \{b, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}) \to \{f (b), f (c)\} \in Edg (H)$
140	139	3expia	$⊢ ((f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\}) \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \to (\{b, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \to \{f (b), f (c)\} \in Edg (H))$
141	136 138 140	3anim123d	$⊢ ((f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\}) \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \to ((\{a, b\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{a, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{b, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}) \to (\{f (a), f (b)\} \in Edg (H) \land \{f (a), f (c)\} \in Edg (H) \land \{f (b), f (c)\} \in Edg (H)))$
142	141	anasss	$⊢ (f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i))) \to ((\{a, b\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{a, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{b, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}) \to (\{f (a), f (b)\} \in Edg (H) \land \{f (a), f (c)\} \in Edg (H) \land \{f (b), f (c)\} \in Edg (H)))$
143	142	ancoms	$⊢ ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a)) \to ((\{a, b\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{a, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{b, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}) \to (\{f (a), f (b)\} \in Edg (H) \land \{f (a), f (c)\} \in Edg (H) \land \{f (b), f (c)\} \in Edg (H)))$
144	143	3adant3	$⊢ ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \to ((\{a, b\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{a, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{b, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}) \to (\{f (a), f (b)\} \in Edg (H) \land \{f (a), f (c)\} \in Edg (H) \land \{f (b), f (c)\} \in Edg (H)))$
145	144	3ad2ant2	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to ((\{a, b\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{a, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{b, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}) \to (\{f (a), f (b)\} \in Edg (H) \land \{f (a), f (c)\} \in Edg (H) \land \{f (b), f (c)\} \in Edg (H)))$
146	145	adantr	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to ((\{a, b\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{a, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \land \{b, c\} \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\}) \to (\{f (a), f (b)\} \in Edg (H) \land \{f (a), f (c)\} \in Edg (H) \land \{f (b), f (c)\} \in Edg (H)))$
147	132 146	mpd	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to (\{f (a), f (b)\} \in Edg (H) \land \{f (a), f (c)\} \in Edg (H) \land \{f (b), f (c)\} \in Edg (H))$
148	115 121 147	3jca	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to (\{f (a), f (b), f (c)\} = \{f (a), f (b), f (c)\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{f (a), f (b)\} \in Edg (H) \land \{f (a), f (c)\} \in Edg (H) \land \{f (b), f (c)\} \in Edg (H)))$
149	86 94 102 106 110 114 148	3rspcedvdw	$⊢ (((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \land ((f (a) \in (H ClNeighbVtx F (a)) \land f (b) \in (H ClNeighbVtx F (a)) \land f (c) \in (H ClNeighbVtx F (a))) \land f [T] = \{f (a), f (b), f (c)\} \land \|f [T]\| = 3)) \to \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (\{f (a), f (b), f (c)\} = \{x, y, z\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H)))$
150	78 149	mpdan	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (\{f (a), f (b), f (c)\} = \{x, y, z\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H)))$
151		eqeq1	$⊢ t = \{f (a), f (b), f (c)\} \to (t = \{x, y, z\} \leftrightarrow \{f (a), f (b), f (c)\} = \{x, y, z\})$
152		fveqeq2	$⊢ t = \{f (a), f (b), f (c)\} \to (\|t\| = 3 \leftrightarrow \|\{f (a), f (b), f (c)\}\| = 3)$
153	151 152	3anbi12d	$⊢ t = \{f (a), f (b), f (c)\} \to ((t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))) \leftrightarrow (\{f (a), f (b), f (c)\} = \{x, y, z\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))))$
154	153	rexbidv	$⊢ t = \{f (a), f (b), f (c)\} \to (\exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))) \leftrightarrow \exists z \in Vtx (H) (\{f (a), f (b), f (c)\} = \{x, y, z\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))))$
155	154	2rexbidv	$⊢ t = \{f (a), f (b), f (c)\} \to (\exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))) \leftrightarrow \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (\{f (a), f (b), f (c)\} = \{x, y, z\} \land \|\{f (a), f (b), f (c)\}\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))))$
156	39 150 155	spcedv	$⊢ ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \land ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \land (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G)))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H)))$
157	156	3exp	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to (((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \land f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H)))))$
158	157	3expd	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to ((g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \to (f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H)))))))$
159	158	exlimdv	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to (\exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i)) \to (f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H)))))))$
160	159	impcomd	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to ((f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i))) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))))))$
161	160	exlimdv	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to (\exists f (f : G ClNeighbVtx a \underset{1-1 onto}{⟶} H ClNeighbVtx F (a) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (a)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx a\} f [i] = g (i))) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))))))$
162	37 161	syld	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to (\forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i))) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))))))$
163	162	com13	$⊢ F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \to (\forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i))) \to ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))))))$
164	163	imp	$⊢ (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \land \forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{y \in Edg (H) \| y \subseteq H ClNeighbVtx F (v)\} \land \forall i \in \{y \in Edg (G) \| y \subseteq G ClNeighbVtx v\} f [i] = g (i)))) \to ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H)))))$
165	9 18 164	3syl	$⊢ φ \to ((φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H)))))$
166	165	anabsi5	$⊢ (φ \land (a \in Vtx (G) \land b \in Vtx (G) \land c \in Vtx (G))) \to ((T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))))$
167	166	rexlimdvvva	$⊢ φ \to (\exists a \in Vtx (G) \exists b \in Vtx (G) \exists c \in Vtx (G) (T = \{a, b, c\} \land \|T\| = 3 \land (\{a, b\} \in Edg (G) \land \{a, c\} \in Edg (G) \land \{b, c\} \in Edg (G))) \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H))))$
168	8 167	mpd	$⊢ φ \to \exists t \exists x \in Vtx (H) \exists y \in Vtx (H) \exists z \in Vtx (H) (t = \{x, y, z\} \land \|t\| = 3 \land (\{x, y\} \in Edg (H) \land \{x, z\} \in Edg (H) \land \{y, z\} \in Edg (H)))$
169	10 13	isgrtri	Could not format ( t e. ( GrTriangles ` H ) <-> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) : No typesetting found for \|- ( t e. ( GrTriangles ` H ) <-> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) with typecode \|-
170	169	exbii	Could not format ( E. t t e. ( GrTriangles ` H ) <-> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) : No typesetting found for \|- ( E. t t e. ( GrTriangles ` H ) <-> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) with typecode \|-
171	168 170	sylibr	Could not format ( ph -> E. t t e. ( GrTriangles ` H ) ) : No typesetting found for \|- ( ph -> E. t t e. ( GrTriangles ` H ) ) with typecode \|-

Metamath Proof Explorer

Theorem grlimgrtri

Proof