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 47821

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 2733	. . . . 5 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
3		eqid 2733	. . . . 5 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
4	2, 3	grtriprop 47793	. . . 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 1126	. . . . . 6 ⊢ (𝜑 → (𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻)))
10		eqid 2733	. . . . . . 7 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
11		eqid 2733	. . . . . . 7 ⊢ (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑣)
12		eqid 2733	. . . . . . 7 ⊢ (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑣))
13		eqid 2733	. . . . . . 7 ⊢ (Edg‘𝐻) = (Edg‘𝐻)
14		sseq1 4021	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣) ↔ 𝑥 ⊆ (𝐺 ClNeighbVtx 𝑣)))
15	14	cbvrabv 3443	. . . . . . 7 ⊢ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ (𝐺 ClNeighbVtx 𝑣)}
16		sseq1 4021	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑥 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))))
17	16	cbvrabv 3443	. . . . . . 7 ⊢ {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))}
18	2, 10, 11, 12, 3, 13, 15, 17	usgrlimprop 47818	. . . . . 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 2734	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → 𝑓 = 𝑓)
20		oveq2 7433	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑎))
21		fveq2 6901	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (𝐹‘𝑣) = (𝐹‘𝑎))
22	21	oveq2d 7441	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑎)))
23	19, 20, 22	f1oeq123d 6837	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑎 → (𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎))))
24		eqidd 2734	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → 𝑔 = 𝑔)
25	20	sseq2d 4028	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣) ↔ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)))
26	25	rabbidv 3440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} = {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)})
27	22	sseq2d 4028	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))))
28	27	rabbidv 3440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} = {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))})
29	24, 26, 28	f1oeq123d 6837	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ↔ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}))
30	26	raleqdv 3322	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ↔ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)))
31	29, 30	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → ((𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ↔ (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))))
32	31	exbidv 1917	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑎 → (∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) ↔ ∃𝑔(𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖))))
33	23, 32	anbi12d 631	. . . . . . . . . . . . 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 1917	. . . . . . . . . . . 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 3618	. . . . . . . . . . 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 1131	. . . . . . . . . 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 7758	. . . . . . . . . . . . . . . 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 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) → 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1→(𝐻 ClNeighbVtx (𝐹‘𝑎)))
41	40	3ad2ant2 1132	. . . . . . . . . . . . . . . . . 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 1132	. . . . . . . . . . . . . . . . 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 47703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 ∈ (Vtx‘𝐺) → 𝑎 ∈ (𝐺 ClNeighbVtx 𝑎))
44	43	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . . . . . 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 47712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 ∈ (Vtx‘𝐺) ∧ 𝑎 ∈ (Vtx‘𝐺) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
50	46, 47, 48, 49	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎)))
54	53	3adant3 1130	. . . . . . . . . . . . . . . . . . . . . . . . . 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 47712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑐 ∈ (Vtx‘𝐺) ∧ 𝑎 ∈ (Vtx‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
60	56, 57, 58, 59	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺)) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎)))
65	64	3adant2 1129	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1126	. . . . . . . . . . . . . . . . . . . . . . . 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 1346	. . . . . . . . . . . . . . . . . . . . 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 1109	. . . . . . . . . . . . . . . . . 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 1146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3))
75	74	3ad2ant3 1133	. . . . . . . . . . . . . . . . . 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 47798	. . . . . . . . . . . . . . . . 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 4749	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑦, 𝑧} = {(𝑓‘𝑎), 𝑦, 𝑧})
80	79	eqeq2d 2744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑓‘𝑎) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧}))
81		preq1 4740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑦} = {(𝑓‘𝑎), 𝑦})
82	81	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → ({𝑥, 𝑦} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻)))
83		preq1 4740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑧} = {(𝑓‘𝑎), 𝑧})
84	83	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → ({𝑥, 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻)))
85	82, 84	3anbi12d 1435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑓‘𝑎) → (({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
86	80, 85	3anbi13d 1436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑓‘𝑎) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
87		tpeq2 4750	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → {(𝑓‘𝑎), 𝑦, 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧})
88	87	eqeq2d 2744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑓‘𝑏) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧}))
89		preq2 4741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑓‘𝑏) → {(𝑓‘𝑎), 𝑦} = {(𝑓‘𝑎), (𝑓‘𝑏)})
90	89	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻)))
91		preq1 4740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑓‘𝑏) → {𝑦, 𝑧} = {(𝑓‘𝑏), 𝑧})
92	91	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → ({𝑦, 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)))
93	90, 92	3anbi13d 1436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑓‘𝑏) → (({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻))))
94	88, 93	3anbi13d 1436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑓‘𝑏) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)))))
95		tpeq3 4751	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)})
96	95	eqeq2d 2744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}))
97		preq2 4741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑎), 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑐)})
98	97	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
99		preq2 4741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑏), 𝑧} = {(𝑓‘𝑏), (𝑓‘𝑐)})
100	99	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
101	98, 100	3anbi23d 1437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘𝑐) → (({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
102	96, 101	3anbi13d 1436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑓‘𝑐) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))))
103	10	clnbgrisvtx 47704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
104	103	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑎) ∈ (Vtx‘𝐻))
105	104	3ad2ant1 1131	. . . . . . . . . . . . . . . . . 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 47704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
108	107	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑏) ∈ (Vtx‘𝐻))
109	108	3ad2ant1 1131	. . . . . . . . . . . . . . . . . 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 47704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
112	111	3ad2ant3 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) → (𝑓‘𝑐) ∈ (Vtx‘𝐻))
113	112	3ad2ant1 1131	. . . . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . . 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 6901	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = (𝑓 “ 𝑇) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
117	116	eqcoms 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
118	117	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
119		simp3 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘(𝑓 “ 𝑇)) = 3)
120	118, 119	eqtrd 2773	. . . . . . . . . . . . . . . . . . 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 29197	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
123	6, 122	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐺 ∈ UHGraph)
124	123	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → 𝐺 ∈ UHGraph)
125		simp3 1136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))
126	124, 125	anim12i 612	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺)))) → (𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))))
127	126	3adant2 1129	. . . . . . . . . . . . . . . . . . . . 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 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺 ClNeighbVtx 𝑎) = (𝐺 ClNeighbVtx 𝑎)
130		eqid 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} = {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}
131	2, 129, 3, 130	grlimgrtrilem1 47819	. . . . . . . . . . . . . . . . . . . 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 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐻 ClNeighbVtx (𝐹‘𝑎)) = (𝐻 ClNeighbVtx (𝐹‘𝑎))
134		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} = {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}
135	2, 129, 3, 130, 133, 13, 134	grlimgrtrilem2 47820	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑎, 𝑏} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻))
136	135	3expia 1119	. . . . . . . . . . . . . . . . . . . . . . . . 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 47820	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑎, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻))
138	137	3expia 1119	. . . . . . . . . . . . . . . . . . . . . . . . 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 47820	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}) → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))
140	139	3expia 1119	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}) ∧ ∀𝑖 ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} (𝑓 “ 𝑖) = (𝑔‘𝑖)) → ({𝑏, 𝑐} ∈ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
141	136, 138, 140	3anim123d 1441	. . . . . . . . . . . . . . . . . . . . . . . 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 1130	. . . . . . . . . . . . . . . . . . . . 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 1132	. . . . . . . . . . . . . . . . . . . 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 1126	. . . . . . . . . . . . . . . . 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 3640	. . . . . . . . . . . . . . . 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 686	. . . . . . . . . . . . . . 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 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (𝑡 = {𝑥, 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧}))
152		fveqeq2 6910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → ((♯‘𝑡) = 3 ↔ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3))
153	151, 152	3anbi12d 1435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → ((𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
154	153	rexbidv 3175	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
155	154	2rexbidv 3218	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
156	39, 150, 155	spcedv 3598	. . . . . . . . . . . . . 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 1117	. . . . . . . . . . . . 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 1351	. . . . . . . . . . . 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 1929	. . . . . . . . . . 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 1929	. . . . . . . . 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 668	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Vtx‘𝐺) ∧ 𝑏 ∈ (Vtx‘𝐺) ∧ 𝑐 ∈ (Vtx‘𝐺))) → ((𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺))) → ∃𝑡∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
167	166	rexlimdvvva 3210	. . 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 47795	. . 3 ⊢ (𝑡 ∈ (GrTriangles‘𝐻) ↔ ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
170	169	exbii 1843	. 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 1085 = wceq 1535 ∃wex 1774 ∈ wcel 2104 ∀wral 3057 ∃wrex 3066 {crab 3432 Vcvv 3477 ⊆ wss 3963 {cpr 4632 {ctp 4634 “ cima 5686 –1-1→wf1 6555 –1-1-onto→wf1o 6557 ‘cfv 6558 (class class class)co 7425 3c3 12313 ♯chash 14355 Vtxcvtx 29009 Edgcedg 29060 UHGraphcuhgr 29069 USPGraphcuspgr 29161 ClNeighbVtx cclnbgr 47693 GrTrianglescgrtri 47789 GraphLocIso cgrlim 47801

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1963 ax-7 2003 ax-8 2106 ax-9 2114 ax-10 2137 ax-11 2153 ax-12 2173 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5366 ax-pr 5430 ax-un 7747 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1538 df-fal 1548 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2536 df-eu 2565 df-clab 2711 df-cleq 2725 df-clel 2812 df-nfc 2888 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-reu 3377 df-rab 3433 df-v 3479 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4915 df-int 4954 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5635 df-we 5637 df-xp 5689 df-rel 5690 df-cnv 5691 df-co 5692 df-dm 5693 df-rn 5694 df-res 5695 df-ima 5696 df-pred 6317 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6510 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7381 df-ov 7428 df-oprab 7429 df-mpo 7430 df-om 7881 df-1st 8007 df-2nd 8008 df-frecs 8299 df-wrecs 8330 df-recs 8404 df-rdg 8443 df-1o 8499 df-2o 8500 df-3o 8501 df-oadd 8503 df-er 8738 df-map 8861 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-dju 9932 df-card 9970 df-pnf 11288 df-mnf 11289 df-xr 11290 df-ltxr 11291 df-le 11292 df-sub 11485 df-neg 11486 df-nn 12258 df-2 12320 df-3 12321 df-n0 12518 df-xnn0 12591 df-z 12605 df-uz 12870 df-fz 13538 df-fzo 13682 df-hash 14356 df-vtx 29011 df-iedg 29012 df-edg 29061 df-uhgr 29071 df-upgr 29095 df-uspgr 29163 df-clnbgr 47694 df-isubgr 47734 df-grim 47749 df-gric 47752 df-grtri 47790 df-grlim 47803

This theorem is referenced by: usgrexmpl12ngrlic 47855

W3C validator