grlimgrtri - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > grlimgrtri		Structured version Visualization version GIF version

Theorem grlimgrtri 48768

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 (𝐹 “ 𝑇) of the triangle 𝑇 in the first graph. (Contributed by AV, 24-Aug-2025.)

**Hypotheses**
Ref	Expression
grlimgrtri.g	⊢ (𝜑 → 𝐺 ∈ USPGraph)
grlimgrtri.h	⊢ (𝜑 → 𝐻 ∈ USPGraph)
grlimgrtri.n	⊢ (𝜑 → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))
grlimgrtri.t	⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺))

**Assertion**
Ref	Expression
grlimgrtri	⊢ (𝜑 → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐻))

Distinct variable group: 𝑡,𝐻 Allowed substitution hints: 𝜑(𝑡) 𝑇(𝑡) 𝐹(𝑡) 𝐺(𝑡)

Proof of Theorem grlimgrtri Dummy variables 𝑎 𝑏 𝑐 𝑓 𝑔 𝑖 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		grlimgrtri.t	. . . 4 ⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺))
2		eqid 2763	. . . . 5 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
3		eqid 2763	. . . . 5 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
4	2, 3	grtriprop 48706	. . . 4 ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)∃𝑐 ∈ (Vtx‘𝐺)(𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
5	1, 4	syl 18	. . 3 ⊢ (𝜑 → ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)∃𝑐 ∈ (Vtx‘𝐺)(𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
6		grlimgrtri.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ USPGraph)
7		grlimgrtri.h	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ USPGraph)
8		grlimgrtri.n	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝐺 GraphLocIso 𝐻))
9	6, 7, 8	3jca 1146	. . . . . 6 ⊢ (𝜑 → (𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻)))
10		eqid 2763	. . . . . . 7 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
11		eqid 2763	. . . . . . 7 ⊢ (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑣)
12		eqid 2763	. . . . . . 7 ⊢ (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑣))
13		eqid 2763	. . . . . . 7 ⊢ (Edg‘𝐻) = (Edg‘𝐻)
14		sseq1 3962	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣) ↔ 𝑥 ⊆ (𝐺 ClNeighbVtx 𝑣)))
15	14	cbvrabv 3426	. . . . . . 7 ⊢ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ (𝐺 ClNeighbVtx 𝑣)}
16		sseq1 3962	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑥 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))))
17	16	cbvrabv 3426	. . . . . . 7 ⊢ {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))}
18	2, 10, 11, 12, 3, 13, 15, 17	usgrlimprop 48758	. . . . . 6 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻)) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
19		eqidd 2764	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → 𝑓 = 𝑓)
20		oveq2 7418	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑎))
21		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (𝐹‘𝑣) = (𝐹‘𝑎))
22	21	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑎)))
23	19, 20, 22	f1oeq123d 6814	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑎 → (𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎))))
24		eqidd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → 𝑔 = 𝑔)
25	20	sseq2d 3969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣) ↔ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)))
26	25	rabbidv 3423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} = {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)})
27	22	sseq2d 3969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))))
28	27	rabbidv 3423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} = {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))})
29	24, 26, 28	f1oeq123d 6814	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ↔ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}))
30	26	raleqdv 3323	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ↔ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))
31	29, 30	anbi12d 643	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ↔ (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))))
32	31	exbidv 1951	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑎 → (∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ↔ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))))
33	23, 32	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑎 → ((𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) ↔ (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
34	33	exbidv 1951	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑎 → (∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) ↔ ∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
35	34	rspcv 3577	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (Vtx‘𝐺) → (∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → ∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
36	35	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → ∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
37	36	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → ∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))))
38		tpex 7743	. . . . . . . . . . . . . . . 16 ⊢ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∈ V
39	38	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∈ V)
40		f1of1 6819	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)))
41	40	3ad2ant2 1152	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)))
42	41	3ad2ant2 1152	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)))
43	2	clnbgrvtxel 48594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 ∈ (Vtx‘𝐺) → 𝑎 ∈ (𝐺 ClNeighbVtx 𝑎))
44	43	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → 𝑎 ∈ (𝐺 ClNeighbVtx 𝑎))
45	44	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → 𝑎 ∈ (𝐺 ClNeighbVtx 𝑎))
46		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (Vtx‘𝐺))
47		simpll 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑎 ∈ (Vtx‘𝐺))
48		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → {𝑎, 𝑏} ∈ (Edg‘𝐺))
49	2, 3	predgclnbgrel 48604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 ∈ (Vtx‘𝐺) ∧ 𝑎 ∈ (Vtx‘𝐺) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
50	46, 47, 48, 49	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
51	50	2a1d 27	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))))
52	51	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎)))))
53	52	3impd 1367	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎)))
54	53	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎)))
55	54	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
56		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (Vtx‘𝐺))
57		simpll 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑎 ∈ (Vtx‘𝐺))
58		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → {𝑎, 𝑐} ∈ (Edg‘𝐺))
59	2, 3	predgclnbgrel 48604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑐 ∈ (Vtx‘𝐺) ∧ 𝑎 ∈ (Vtx‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
60	56, 57, 58, 59	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
61	60	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
62	61	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))
63	62	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))))
64	63	3impd 1367	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
65	64	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
66	65	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
67	45, 55, 66	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
68	67	ex 417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))
69	68	2a1d 27	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (𝑇 = {𝑎, 𝑏, 𝑐} → ((♯‘𝑇) = 3 → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))))
70	69	3impd 1367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))
71	70	a1d 26	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))))
72	71	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))))
73	72	3imp 1128	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
74		3simpa 1166	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3))
75	74	3ad2ant3 1153	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3))
76	73, 75	jca 520	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → ((𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3)))
77		grtrimap 48713	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → (((𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3)) → (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)))
78	42, 76, 77	sylc 66	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3))
79		tpeq1 4708	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑦, 𝑧} = {(𝑓‘𝑎), 𝑦, 𝑧})
80	79	eqeq2d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑓‘𝑎) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧}))
81		preq1 4699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑦} = {(𝑓‘𝑎), 𝑦})
82	81	eleq1d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → ({𝑥, 𝑦} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻)))
83		preq1 4699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑧} = {(𝑓‘𝑎), 𝑧})
84	83	eleq1d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → ({𝑥, 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻)))
85	82, 84	3anbi12d 1465	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑓‘𝑎) → (({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
86	80, 85	3anbi13d 1466	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑓‘𝑎) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
87		tpeq2 4709	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → {(𝑓‘𝑎), 𝑦, 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧})
88	87	eqeq2d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑓‘𝑏) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧}))
89		preq2 4700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑓‘𝑏) → {(𝑓‘𝑎), 𝑦} = {(𝑓‘𝑎), (𝑓‘𝑏)})
90	89	eleq1d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻)))
91		preq1 4699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑓‘𝑏) → {𝑦, 𝑧} = {(𝑓‘𝑏), 𝑧})
92	91	eleq1d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → ({𝑦, 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)))
93	90, 92	3anbi13d 1466	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑓‘𝑏) → (({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻))))
94	88, 93	3anbi13d 1466	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑓‘𝑏) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)))))
95		tpeq3 4710	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)})
96	95	eqeq2d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}))
97		preq2 4700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑎), 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑐)})
98	97	eleq1d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
99		preq2 4700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑏), 𝑧} = {(𝑓‘𝑏), (𝑓‘𝑐)})
100	99	eleq1d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
101	98, 100	3anbi23d 1467	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘𝑐) → (({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
102	96, 101	3anbi13d 1466	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑓‘𝑐) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))))
103	10	clnbgrisvtx 48595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
104	103	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
105	104	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
106	105	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
107	10	clnbgrisvtx 48595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
108	107	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
109	108	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
110	109	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
111	10	clnbgrisvtx 48595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
112	111	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
113	112	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
114	113	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
115		eqidd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)})
116		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = (𝑓 “ 𝑇) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
117	116	eqcoms 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
118	117	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
119		simp3 1156	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘(𝑓 “ 𝑇)) = 3)
120	118, 119	eqtrd 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3)
121	120	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3)
122		uspgruhgr 29534	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
123	6, 122	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐺 ∈ UHGraph)
124	123	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → 𝐺 ∈ UHGraph)
125		simp3 1156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))
126	124, 125	anim12i 624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
127	126	3adant2 1149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
128	127	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
129		eqid 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺 ClNeighbVtx 𝑎) = (𝐺 ClNeighbVtx 𝑎)
130		eqid 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} = {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}
131	2, 129, 3, 130	grlimgrtrilem1 48766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}))
132	128, 131	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → ({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}))
133		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐻 ClNeighbVtx (𝐹‘𝑎)) = (𝐻 ClNeighbVtx (𝐹‘𝑎))
134		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} = {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}
135	2, 129, 3, 130, 133, 13, 134	grlimgrtrilem2 48767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻))
136	135	3expia 1139	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → ({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} → {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻)))
137	2, 129, 3, 130, 133, 13, 134	grlimgrtrilem2 48767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻))
138	137	3expia 1139	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → ({𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} → {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
139	2, 129, 3, 130, 133, 13, 134	grlimgrtrilem2 48767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))
140	139	3expia 1139	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → ({𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
141	136, 138, 140	3anim123d 1471	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
142	141	anasss 471	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
143	142	ancoms 463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎))) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
144	143	3adant3 1150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
145	144	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
146	145	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → (({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
147	132, 146	mpd 16	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
148	115, 121, 147	3jca 1146	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
149	86, 94, 102, 106, 110, 114, 148	3rspcedvdw 3599	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) ∧ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)) → ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
150	78, 149	mpdan 699	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
151		eqeq1 2767	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (𝑡 = {𝑥, 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧}))
152		fveqeq2 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → ((♯‘𝑡) = 3 ↔ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3))
153	151, 152	3anbi12d 1465	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → ((𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
154	153	rexbidv 3189	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
155	154	2rexbidv 3230	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
156	39, 150, 155	spcedv 3557	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
157	156	3exp 1137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ∧ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))
158	157	3expd 1372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))))
159	158	exlimdv 1963	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))))
160	159	impcomd 416	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))))
161	160	exlimdv 1963	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))))
162	37, 161	syld 48	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → (∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))))
163	162	com13 89	. . . . . . 7 ⊢ (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → (∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖))) → ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))))
164	163	imp 411	. . . . . 6 ⊢ ((𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)∃𝑓(𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ∧ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))) → ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))
165	9, 18, 164	3syl 19	. . . . 5 ⊢ (𝜑 → ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))
166	165	anabsi5 681	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
167	166	rexlimdvvva 3223	. . 3 ⊢ (𝜑 → (∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)∃𝑐 ∈ (Vtx‘𝐺)(𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
168	5, 167	mpd 16	. 2 ⊢ (𝜑 → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
169	10, 13	isgrtri 48708	. . 3 ⊢ (𝑡 ∈ (GrTriangles‘𝐻) ↔ ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
170	169	exbii 1878	. 2 ⊢ (∃𝑡 𝑡 ∈ (GrTriangles‘𝐻) ↔ ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
171	168, 170	sylibr 237	1 ⊢ (𝜑 → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∃wex 1809 ∈ wcel 2143 ∀wral 3079 ∃wrex 3089 {crab 3416 Vcvv 3455 ⊆ wss 3905 {cpr 4591 {ctp 4593 “ cima 5664 –1-1→wf1 6533 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 3c3 12291 ♯chash 14362 Vtxcvtx 29346 Edgcedg 29397 UHGraphcuhgr 29406 USPGraphcuspgr 29498 ClNeighbVtx cclnbgr 48583 GrTrianglescgrtri 48702 GraphLocIso cgrlim 48741

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-3o 8451 df-oadd 8453 df-er 8690 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-dju 9883 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-3 12299 df-n0 12500 df-xnn0 12573 df-z 12587 df-uz 12858 df-fz 13531 df-fzo 13679 df-hash 14363 df-vtx 29348 df-iedg 29349 df-edg 29398 df-uhgr 29408 df-upgr 29432 df-uspgr 29500 df-clnbgr 48584 df-isubgr 48626 df-grim 48643 df-gric 48646 df-grtri 48703 df-grlim 48743

This theorem is referenced by: usgrexmpl12ngrlic 48804

W3C validator