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 47936

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 2734	. . . . 5 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
3		eqid 2734	. . . . 5 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
4	2, 3	grtriprop 47881	. . . 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 2734	. . . . . . 7 ⊢ (Vtx‘𝐻) = (Vtx‘𝐻)
11		eqid 2734	. . . . . . 7 ⊢ (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑣)
12		eqid 2734	. . . . . . 7 ⊢ (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑣))
13		eqid 2734	. . . . . . 7 ⊢ (Edg‘𝐻) = (Edg‘𝐻)
14		sseq1 3989	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣) ↔ 𝑥 ⊆ (𝐺 ClNeighbVtx 𝑣)))
15	14	cbvrabv 3430	. . . . . . 7 ⊢ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} = {𝑥 ∈ (Edg‘𝐺) ∣ 𝑥 ⊆ (𝐺 ClNeighbVtx 𝑣)}
16		sseq1 3989	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑥 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))))
17	16	cbvrabv 3430	. . . . . . 7 ⊢ {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} = {𝑥 ∈ (Edg‘𝐻) ∣ 𝑥 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))}
18	2, 10, 11, 12, 3, 13, 15, 17	usgrlimprop 47933	. . . . . 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 2735	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → 𝑓 = 𝑓)
20		oveq2 7421	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑎))
21		fveq2 6886	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (𝐹‘𝑣) = (𝐹‘𝑎))
22	21	oveq2d 7429	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑎 → (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑎)))
23	19, 20, 22	f1oeq123d 6822	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑎 → (𝑓:(𝐺 ClNeighbVtx 𝑣)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑓:(𝐺 ClNeighbVtx 𝑎)–1-1-onto→(𝐻 ClNeighbVtx (𝐹‘𝑎))))
24		eqidd 2735	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → 𝑔 = 𝑔)
25	20	sseq2d 3996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣) ↔ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)))
26	25	rabbidv 3427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)} = {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)})
27	22	sseq2d 3996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑎 → (𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣)) ↔ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))))
28	27	rabbidv 3427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑎 → {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} = {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))})
29	24, 26, 28	f1oeq123d 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑎 → (𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑣)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑣))} ↔ 𝑔:{𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}–1-1-onto→{𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}))
30	26	raleqdv 3309	. . . . . . . . . . . . . . . 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 1920	. . . . . . . . . . . . . 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 1920	. . . . . . . . . . . 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 3601	. . . . . . . . . . 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 7748	. . . . . . . . . . . . . . . 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 6827	. . . . . . . . . . . . . . . . . . 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 47789	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 47798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏 ∈ (Vtx‘𝐺) ∧ 𝑎 ∈ (Vtx‘𝐺) ∧ {𝑎, 𝑏} ∈ (Edg‘𝐺)) → 𝑏 ∈ (𝐺 ClNeighbVtx 𝑎))
50	46, 47, 48, 49	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1348	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 47798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑐 ∈ (Vtx‘𝐺) ∧ 𝑎 ∈ (Vtx‘𝐺) ∧ {𝑎, 𝑐} ∈ (Edg‘𝐺)) → 𝑐 ∈ (𝐺 ClNeighbVtx 𝑎))
60	56, 57, 58, 59	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1348	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1348	. . . . . . . . . . . . . . . . . . . . 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 47888	. . . . . . . . . . . . . . . . 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 4722	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑦, 𝑧} = {(𝑓‘𝑎), 𝑦, 𝑧})
80	79	eqeq2d 2745	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑓‘𝑎) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧}))
81		preq1 4713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑦} = {(𝑓‘𝑎), 𝑦})
82	81	eleq1d 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → ({𝑥, 𝑦} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻)))
83		preq1 4713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓‘𝑎) → {𝑥, 𝑧} = {(𝑓‘𝑎), 𝑧})
84	83	eleq1d 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑎) → ({𝑥, 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻)))
85	82, 84	3anbi12d 1438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑓‘𝑎) → (({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
86	80, 85	3anbi13d 1439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑓‘𝑎) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
87		tpeq2 4723	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → {(𝑓‘𝑎), 𝑦, 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧})
88	87	eqeq2d 2745	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑓‘𝑏) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧}))
89		preq2 4714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑓‘𝑏) → {(𝑓‘𝑎), 𝑦} = {(𝑓‘𝑎), (𝑓‘𝑏)})
90	89	eleq1d 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻)))
91		preq1 4713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑓‘𝑏) → {𝑦, 𝑧} = {(𝑓‘𝑏), 𝑧})
92	91	eleq1d 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑓‘𝑏) → ({𝑦, 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)))
93	90, 92	3anbi13d 1439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑓‘𝑏) → (({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻))))
94	88, 93	3anbi13d 1439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑓‘𝑏) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), 𝑦} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)))))
95		tpeq3 4724	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)})
96	95	eqeq2d 2745	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}))
97		preq2 4714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑎), 𝑧} = {(𝑓‘𝑎), (𝑓‘𝑐)})
98	97	eleq1d 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
99		preq2 4714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘𝑐) → {(𝑓‘𝑏), 𝑧} = {(𝑓‘𝑏), (𝑓‘𝑐)})
100	99	eleq1d 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘𝑐) → ({(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻) ↔ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))
101	98, 100	3anbi23d 1440	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘𝑐) → (({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻)) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻))))
102	96, 101	3anbi13d 1439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑓‘𝑐) → (({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), 𝑧} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑎), (𝑓‘𝑐)} ∈ (Edg‘𝐻) ∧ {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ (Edg‘𝐻)))))
103	10	clnbgrisvtx 47790	. . . . . . . . . . . . . . . . . . . 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 47790	. . . . . . . . . . . . . . . . . . . 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 47790	. . . . . . . . . . . . . . . . . . . 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 2735	. . . . . . . . . . . . . . . . . 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 6886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = (𝑓 “ 𝑇) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
117	116	eqcoms 2742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
118	117	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = (♯‘(𝑓 “ 𝑇)))
119		simp3 1138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓‘𝑎) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑏) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎)) ∧ (𝑓‘𝑐) ∈ (𝐻 ClNeighbVtx (𝐹‘𝑎))) ∧ (𝑓 “ 𝑇) = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} ∧ (♯‘(𝑓 “ 𝑇)) = 3) → (♯‘(𝑓 “ 𝑇)) = 3)
120	118, 119	eqtrd 2769	. . . . . . . . . . . . . . . . . . 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 29130	. . . . . . . . . . . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺 ClNeighbVtx 𝑎) = (𝐺 ClNeighbVtx 𝑎)
130		eqid 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)} = {𝑦 ∈ (Edg‘𝐺) ∣ 𝑦 ⊆ (𝐺 ClNeighbVtx 𝑎)}
131	2, 129, 3, 130	grlimgrtrilem1 47934	. . . . . . . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐻 ClNeighbVtx (𝐹‘𝑎)) = (𝐻 ClNeighbVtx (𝐹‘𝑎))
134		eqid 2734	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))} = {𝑦 ∈ (Edg‘𝐻) ∣ 𝑦 ⊆ (𝐻 ClNeighbVtx (𝐹‘𝑎))}
135	2, 129, 3, 130, 133, 13, 134	grlimgrtrilem2 47935	. . . . . . . . . . . . . . . . . . . . . . . . . 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 47935	. . . . . . . . . . . . . . . . . . . . . . . . . 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 47935	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1444	. . . . . . . . . . . . . . . . . . . . . . . 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 3623	. . . . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (𝑡 = {𝑥, 𝑦, 𝑧} ↔ {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧}))
152		fveqeq2 6895	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → ((♯‘𝑡) = 3 ↔ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3))
153	151, 152	3anbi12d 1438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → ((𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
154	153	rexbidv 3166	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
155	154	2rexbidv 3209	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = {(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} → (∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))) ↔ ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)({(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)} = {𝑥, 𝑦, 𝑧} ∧ (♯‘{(𝑓‘𝑎), (𝑓‘𝑏), (𝑓‘𝑐)}) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻)))))
156	39, 150, 155	spcedv 3581	. . . . . . . . . . . . . 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 1353	. . . . . . . . . . . 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 1932	. . . . . . . . . . 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 1932	. . . . . . . . 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 3201	. . 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 47883	. . 3 ⊢ (𝑡 ∈ (GrTriangles‘𝐻) ↔ ∃𝑥 ∈ (Vtx‘𝐻)∃𝑦 ∈ (Vtx‘𝐻)∃𝑧 ∈ (Vtx‘𝐻)(𝑡 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐻) ∧ {𝑥, 𝑧} ∈ (Edg‘𝐻) ∧ {𝑦, 𝑧} ∈ (Edg‘𝐻))))
170	169	exbii 1847	. 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 1539 ∃wex 1778 ∈ wcel 2107 ∀wral 3050 ∃wrex 3059 {crab 3419 Vcvv 3463 ⊆ wss 3931 {cpr 4608 {ctp 4610 “ cima 5668 –1-1→wf1 6538 –1-1-onto→wf1o 6540 ‘cfv 6541 (class class class)co 7413 3c3 12304 ♯chash 14352 Vtxcvtx 28942 Edgcedg 28993 UHGraphcuhgr 29002 USPGraphcuspgr 29094 ClNeighbVtx cclnbgr 47778 GrTrianglescgrtri 47877 GraphLocIso cgrlim 47916

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7870 df-1st 7996 df-2nd 7997 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-3o 8490 df-oadd 8492 df-er 8727 df-map 8850 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-dju 9923 df-card 9961 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-nn 12249 df-2 12311 df-3 12312 df-n0 12510 df-xnn0 12583 df-z 12597 df-uz 12861 df-fz 13530 df-fzo 13677 df-hash 14353 df-vtx 28944 df-iedg 28945 df-edg 28994 df-uhgr 29004 df-upgr 29028 df-uspgr 29096 df-clnbgr 47779 df-isubgr 47820 df-grim 47837 df-gric 47840 df-grtri 47878 df-grlim 47918

This theorem is referenced by: usgrexmpl12ngrlic 47971

W3C validator