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 47968

Description: Local isomorphisms between simple pseudographs map triangles onto triangles. (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 2729	. . . . 5 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
3		eqid 2729	. . . . 5 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
4	2, 3	grtriprop 47913	. . . 4 ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → ∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)∃𝑐 ∈ (Vtx‘𝐺)(𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
5	1, 4	syl 17	. . 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 1128	. . . . . 6 ⊢ (𝜑 → (𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻)))
10		eqid 2729	. . . . . . 7 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
11		eqid 2729	. . . . . . 7 ⊢ (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑣)
12		eqid 2729	. . . . . . 7 ⊢ (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑣))
13		eqid 2729	. . . . . . 7 ⊢ (Edg‘𝐻) = (Edg‘𝐻)
14		sseq1 3969	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣) ↔ 𝑥 ⊆ (𝐺 ClNeighbVtx 𝑣)))
15	14	cbvrabv 3413	. . . . . . 7 ⊢ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ (𝐺 ClNeighbVtx 𝑣)}
16		sseq1 3969	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑥 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))))
17	16	cbvrabv 3413	. . . . . . 7 ⊢ {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))}
18	2, 10, 11, 12, 3, 13, 15, 17	usgrlimprop 47965	. . . . . 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 2730	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → 𝑓 = 𝑓)
20		oveq2 7377	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑎))
21		fveq2 6840	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (𝐹‘𝑣) = (𝐹‘𝑎))
22	21	oveq2d 7385	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑎)))
23	19, 20, 22	f1oeq123d 6776	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑎 → (𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎))))
24		eqidd 2730	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → 𝑔 = 𝑔)
25	20	sseq2d 3976	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣) ↔ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)))
26	25	rabbidv 3410	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} = {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)})
27	22	sseq2d 3976	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))))
28	27	rabbidv 3410	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} = {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))})
29	24, 26, 28	f1oeq123d 6776	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ↔ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}))
30	26	raleqdv 3296	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ↔ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))
31	29, 30	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ↔ (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))))
32	31	exbidv 1921	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑎 → (∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ↔ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))))
33	23, 32	anbi12d 632	. . . . . . . . . . . . 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 1921	. . . . . . . . . . . 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 3581	. . . . . . . . . . 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 1133	. . . . . . . . . 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 481	. . . . . . . . 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 7702	. . . . . . . . . . . . . . . 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 6781	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)))
41	40	3ad2ant2 1134	. . . . . . . . . . . . . . . . . 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 1134	. . . . . . . . . . . . . . . . 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 47803	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 ∈ (Vtx‘𝐺) → 𝑎 ∈ (𝐺 ClNeighbVtx 𝑎))
44	43	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → 𝑎 ∈ (𝐺 ClNeighbVtx 𝑎))
45	44	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → 𝑎 ∈ (𝐺 ClNeighbVtx 𝑎))
46		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (Vtx‘𝐺))
47		simpll 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑎 ∈ (Vtx‘𝐺))
48		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → {𝑎, 𝑏} ∈ (Edg‘𝐺))
49	2, 3	predgclnbgrel 47812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 ∈ (Vtx‘𝐺) ∧ 𝑎 ∈ (Vtx‘𝐺) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
50	46, 47, 48, 49	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
51	50	2a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))))
52	51	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎)))))
53	52	3impd 1349	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎)))
54	53	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎)))
55	54	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
56		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (Vtx‘𝐺))
57		simpll 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑎 ∈ (Vtx‘𝐺))
58		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → {𝑎, 𝑐} ∈ (Edg‘𝐺))
59	2, 3	predgclnbgrel 47812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑐 ∈ (Vtx‘𝐺) ∧ 𝑎 ∈ (Vtx‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
60	56, 57, 58, 59	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
61	60	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
62	61	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))
63	62	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) → ({𝑎, 𝑐} ∈ (Edg‘𝐺) → ({𝑏, 𝑐} ∈ (Edg‘𝐺) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))))
64	63	3impd 1349	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
65	64	3adant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
66	65	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
67	45, 55, 66	3jca 1128	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
68	67	ex 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))
69	68	2a1d 26	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (𝑇 = {𝑎, 𝑏, 𝑐} → ((♯‘𝑇) = 3 → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))))
70	69	3impd 1349	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))))
71	70	a1d 25	. . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . 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 1110	. . . . . . . . . . . . . . . . . 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 1148	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3))
75	74	3ad2ant3 1135	. . . . . . . . . . . . . . . . . 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 511	. . . . . . . . . . . . . . . . 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 47920	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → (((𝑎 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎) ∧ 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3)) → (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3)))
78	42, 76, 77	sylc 65	. . . . . . . . . . . . . . . 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 4702	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑦, 𝑧} = {(𝑓‘𝑎), 𝑦, 𝑧})
80	79	eqeq2d 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑓‘𝑎) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧}))
81		preq1 4693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑦} = {(𝑓‘𝑎), 𝑦})
82	81	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → ({𝑥, 𝑦} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻)))
83		preq1 4693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑧} = {(𝑓‘𝑎), 𝑧})
84	83	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → ({𝑥, 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻)))
85	82, 84	3anbi12d 1439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑓‘𝑎) → (({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
86	80, 85	3anbi13d 1440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑓‘𝑎) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
87		tpeq2 4703	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → {(𝑓‘𝑎), 𝑦, 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧})
88	87	eqeq2d 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑓‘𝑏) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧}))
89		preq2 4694	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑓‘𝑏) → {(𝑓‘𝑎), 𝑦} = {(𝑓‘𝑎), (𝑓‘𝑏)})
90	89	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻)))
91		preq1 4693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑓‘𝑏) → {𝑦, 𝑧} = {(𝑓‘𝑏), 𝑧})
92	91	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → ({𝑦, 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)))
93	90, 92	3anbi13d 1440	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑓‘𝑏) → (({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻))))
94	88, 93	3anbi13d 1440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑓‘𝑏) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)))))
95		tpeq3 4704	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)})
96	95	eqeq2d 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}))
97		preq2 4694	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑎), 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑐)})
98	97	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
99		preq2 4694	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑏), 𝑧} = {(𝑓‘𝑏), (𝑓‘𝑐)})
100	99	eleq1d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
101	98, 100	3anbi23d 1441	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘𝑐) → (({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
102	96, 101	3anbi13d 1440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑓‘𝑐) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))))
103	10	clnbgrisvtx 47804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
104	103	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
105	104	3ad2ant1 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
106	105	adantl 481	. . . . . . . . . . . . . . . . 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 47804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
108	107	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
109	108	3ad2ant1 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
110	109	adantl 481	. . . . . . . . . . . . . . . . 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 47804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
112	111	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
113	112	3ad2ant1 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
114	113	adantl 481	. . . . . . . . . . . . . . . . 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 2730	. . . . . . . . . . . . . . . . . 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 6840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = (𝑓 “ 𝑇) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
117	116	eqcoms 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
118	117	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
119		simp3 1138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘(𝑓 “ 𝑇)) = 3)
120	118, 119	eqtrd 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3)
121	120	adantl 481	. . . . . . . . . . . . . . . . . 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 29087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
123	6, 122	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐺 ∈ UHGraph)
124	123	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → 𝐺 ∈ UHGraph)
125		simp3 1138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))
126	124, 125	anim12i 613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
127	126	3adant2 1131	. . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺 ClNeighbVtx 𝑎) = (𝐺 ClNeighbVtx 𝑎)
130		eqid 2729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} = {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}
131	2, 129, 3, 130	grlimgrtrilem1 47966	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ({𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}))
132	128, 131	syl 17	. . . . . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐻 ClNeighbVtx (𝐹‘𝑎)) = (𝐻 ClNeighbVtx (𝐹‘𝑎))
134		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} = {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}
135	2, 129, 3, 130, 133, 13, 134	grlimgrtrilem2 47967	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻))
136	135	3expia 1121	. . . . . . . . . . . . . . . . . . . . . . . . 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 47967	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻))
138	137	3expia 1121	. . . . . . . . . . . . . . . . . . . . . . . . 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 47967	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))
140	139	3expia 1121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → ({𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
141	136, 138, 140	3anim123d 1445	. . . . . . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . . . . . . . . . . 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 1132	. . . . . . . . . . . . . . . . . . . . 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 1134	. . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . 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 15	. . . . . . . . . . . . . . . . . 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 1128	. . . . . . . . . . . . . . . . 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 3603	. . . . . . . . . . . . . . . 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 687	. . . . . . . . . . . . . . 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 2733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (𝑡 = {𝑥, 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧}))
152		fveqeq2 6849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → ((♯‘𝑡) = 3 ↔ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3))
153	151, 152	3anbi12d 1439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → ((𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
154	153	rexbidv 3157	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
155	154	2rexbidv 3200	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
156	39, 150, 155	spcedv 3561	. . . . . . . . . . . . . 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 1119	. . . . . . . . . . . . 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 1354	. . . . . . . . . . . 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 1933	. . . . . . . . . . 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 411	. . . . . . . . . 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 1933	. . . . . . . . 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 47	. . . . . . . 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 88	. . . . . . 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 406	. . . . . 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 18	. . . . 5 ⊢ (𝜑 → ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))))
166	165	anabsi5 669	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
167	166	rexlimdvvva 3193	. . 3 ⊢ (𝜑 → (∃𝑎 ∈ (Vtx‘𝐺)∃𝑏 ∈ (Vtx‘𝐺)∃𝑐 ∈ (Vtx‘𝐺)(𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
168	5, 167	mpd 15	. 2 ⊢ (𝜑 → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
169	10, 13	isgrtri 47915	. . 3 ⊢ (𝑡 ∈ (GrTriangles‘𝐻) ↔ ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
170	169	exbii 1848	. 2 ⊢ (∃𝑡 𝑡 ∈ (GrTriangles‘𝐻) ↔ ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
171	168, 170	sylibr 234	1 ⊢ (𝜑 → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 {crab 3402 Vcvv 3444 ⊆ wss 3911 {cpr 4587 {ctp 4589 “ cima 5634 –1-1→wf1 6496 –1-1-onto→wf1o 6498 ‘cfv 6499 (class class class)co 7369 3c3 12218 ♯chash 14271 Vtxcvtx 28899 Edgcedg 28950 UHGraphcuhgr 28959 USPGraphcuspgr 29051 ClNeighbVtx cclnbgr 47792 GrTrianglescgrtri 47909 GraphLocIso cgrlim 47948

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-3o 8413 df-oadd 8415 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-dju 9830 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-xnn0 12492 df-z 12506 df-uz 12770 df-fz 13445 df-fzo 13592 df-hash 14272 df-vtx 28901 df-iedg 28902 df-edg 28951 df-uhgr 28961 df-upgr 28985 df-uspgr 29053 df-clnbgr 47793 df-isubgr 47834 df-grim 47851 df-gric 47854 df-grtri 47910 df-grlim 47950

This theorem is referenced by: usgrexmpl12ngrlic 48003

W3C validator