grlicsym - Mathbox for Alexander van der Vekens

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

Theorem grlicsym 49055

Description: Graph local isomorphism is symmetric for hypergraphs. (Contributed by AV, 9-Jun-2025.)

**Assertion**
Ref	Expression
grlicsym	⊢ (𝐺 ∈ UHGraph → (𝐺 ≃_𝑙𝑔𝑟 𝑆 → 𝑆 ≃_𝑙𝑔𝑟 𝐺))

Proof of Theorem grlicsym Dummy variables 𝑓 𝑣 𝑔 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2761	. . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2761	. . . 4 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
3	1, 2	grilcbri 49051	. . 3 ⊢ (𝐺 ≃_𝑙𝑔𝑟 𝑆 → ∃𝑓(𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))))
4		grlicrcl 49049	. . 3 ⊢ (𝐺 ≃_𝑙𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V))
5		vex 3455	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
6		cnvexg 7925	. . . . . . . . . 10 ⊢ (𝑓 ∈ V → ^◡𝑓 ∈ V)
7	5, 6	mp1i 14	. . . . . . . . 9 ⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → ^◡𝑓 ∈ V)
8		f1ocnv 6829	. . . . . . . . . . 11 ⊢ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) → ^◡𝑓:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺))
9	8	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → ^◡𝑓:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺))
10		f1ocnvdm 7285	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆)) → (^◡𝑓‘𝑤) ∈ (Vtx‘𝐺))
11	10	3adant3 1150	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (^◡𝑓‘𝑤) ∈ (Vtx‘𝐺))
12		oveq2 7420	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = (^◡𝑓‘𝑤) → (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))
13	12	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (^◡𝑓‘𝑤) → (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) = (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))))
14		fveq2 6877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = (^◡𝑓‘𝑤) → (𝑓‘𝑣) = (𝑓‘(^◡𝑓‘𝑤)))
15	14	oveq2d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = (^◡𝑓‘𝑤) → (𝑆 ClNeighbVtx (𝑓‘𝑣)) = (𝑆 ClNeighbVtx (𝑓‘(^◡𝑓‘𝑤))))
16	15	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (^◡𝑓‘𝑤) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) = (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(^◡𝑓‘𝑤)))))
17	13, 16	breq12d 5116	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (^◡𝑓‘𝑤) → ((𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) ↔ (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(^◡𝑓‘𝑤))))))
18	17	rspcv 3573	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝑓‘𝑤) ∈ (Vtx‘𝐺) → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) → (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(^◡𝑓‘𝑤))))))
19	11, 18	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) → (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(^◡𝑓‘𝑤))))))
20		f1ocnvfv2 7277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆)) → (𝑓‘(^◡𝑓‘𝑤)) = 𝑤)
21	20	3adant3 1150	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (𝑓‘(^◡𝑓‘𝑤)) = 𝑤)
22	21	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (𝑆 ClNeighbVtx (𝑓‘(^◡𝑓‘𝑤))) = (𝑆 ClNeighbVtx 𝑤))
23	22	oveq2d 7428	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(^◡𝑓‘𝑤)))) = (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)))
24	23	breq2d 5115	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → ((𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(^◡𝑓‘𝑤)))) ↔ (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤))))
25		simp3 1156	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → 𝐺 ∈ UHGraph)
26	1	clnbgrssvtx 48873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)) ⊆ (Vtx‘𝐺)
27	1	isubgruhgr 48910	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ UHGraph ∧ (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)) ⊆ (Vtx‘𝐺)) → (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ∈ UHGraph)
28	25, 26, 27	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ∈ UHGraph)
29		gricsym 48963	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ∈ UHGraph → ((𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))))
30	28, 29	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → ((𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))))
31	24, 30	sylbid 243	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → ((𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(^◡𝑓‘𝑤)))) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))))
32	19, 31	syld 48	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))))
33	32	3exp 1137	. . . . . . . . . . . . 13 ⊢ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) → (𝑤 ∈ (Vtx‘𝑆) → (𝐺 ∈ UHGraph → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))))))
34	33	com24 96	. . . . . . . . . . . 12 ⊢ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) → (𝐺 ∈ UHGraph → (𝑤 ∈ (Vtx‘𝑆) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))))))
35	34	imp31 423	. . . . . . . . . . 11 ⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → (𝑤 ∈ (Vtx‘𝑆) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))))
36	35	ralrimiv 3154	. . . . . . . . . 10 ⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))))
37	9, 36	jca 521	. . . . . . . . 9 ⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → (^◡𝑓:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))))
38		f1oeq1 6804	. . . . . . . . . 10 ⊢ (𝑔 = ^◡𝑓 → (𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ↔ ^◡𝑓:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺)))
39		fveq1 6876	. . . . . . . . . . . . . 14 ⊢ (𝑔 = ^◡𝑓 → (𝑔‘𝑤) = (^◡𝑓‘𝑤))
40	39	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑔 = ^◡𝑓 → (𝐺 ClNeighbVtx (𝑔‘𝑤)) = (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))
41	40	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝑔 = ^◡𝑓 → (𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))) = (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))))
42	41	breq2d 5115	. . . . . . . . . . 11 ⊢ (𝑔 = ^◡𝑓 → ((𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))))
43	42	ralbidv 3186	. . . . . . . . . 10 ⊢ (𝑔 = ^◡𝑓 → (∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))) ↔ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤)))))
44	38, 43	anbi12d 644	. . . . . . . . 9 ⊢ (𝑔 = ^◡𝑓 → ((𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤)))) ↔ (^◡𝑓:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (^◡𝑓‘𝑤))))))
45	7, 37, 44	spcedv 3553	. . . . . . . 8 ⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → ∃𝑔(𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤)))))
46	45	3adant3 1150	. . . . . . 7 ⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph ∧ (𝐺 ∈ V ∧ 𝑆 ∈ V)) → ∃𝑔(𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤)))))
47	2, 1	dfgrlic2 49050	. . . . . . . . 9 ⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝑆 ≃_𝑙𝑔𝑟 𝐺 ↔ ∃𝑔(𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))))))
48	47	ancoms 464	. . . . . . . 8 ⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (𝑆 ≃_𝑙𝑔𝑟 𝐺 ↔ ∃𝑔(𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))))))
49	48	3ad2ant3 1153	. . . . . . 7 ⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph ∧ (𝐺 ∈ V ∧ 𝑆 ∈ V)) → (𝑆 ≃_𝑙𝑔𝑟 𝐺 ↔ ∃𝑔(𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃_𝑔𝑟 (𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))))))
50	46, 49	mpbird 260	. . . . . 6 ⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph ∧ (𝐺 ∈ V ∧ 𝑆 ∈ V)) → 𝑆 ≃_𝑙𝑔𝑟 𝐺)
51	50	3exp 1137	. . . . 5 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) → (𝐺 ∈ UHGraph → ((𝐺 ∈ V ∧ 𝑆 ∈ V) → 𝑆 ≃_𝑙𝑔𝑟 𝐺)))
52	51	com23 87	. . . 4 ⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) → ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (𝐺 ∈ UHGraph → 𝑆 ≃_𝑙𝑔𝑟 𝐺)))
53	52	exlimiv 1963	. . 3 ⊢ (∃𝑓(𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃_𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) → ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (𝐺 ∈ UHGraph → 𝑆 ≃_𝑙𝑔𝑟 𝐺)))
54	3, 4, 53	sylc 66	. 2 ⊢ (𝐺 ≃_𝑙𝑔𝑟 𝑆 → (𝐺 ∈ UHGraph → 𝑆 ≃_𝑙𝑔𝑟 𝐺))
55	54	com12 33	1 ⊢ (𝐺 ∈ UHGraph → (𝐺 ≃_𝑙𝑔𝑟 𝑆 → 𝑆 ≃_𝑙𝑔𝑟 𝐺))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ∀wral 3077 Vcvv 3451 ⊆ wss 3899 class class class wbr 5103 ^◡ccnv 5650 –1-1-onto→wf1o 6530 ‘cfv 6531 (class class class)co 7412 Vtxcvtx 29556 UHGraphcuhgr 29616 ClNeighbVtx cclnbgr 48860 ISubGr cisubgr 48902 ≃_𝑔𝑟 cgric 48918 ≃_𝑙𝑔𝑟 cgrlic 49019

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-ov 7415 df-oprab 7416 df-mpo 7417 df-1st 7990 df-2nd 7991 df-1o 8460 df-map 8833 df-vtx 29558 df-iedg 29559 df-uhgr 29618 df-clnbgr 48861 df-isubgr 48903 df-grim 48920 df-gric 48923 df-grlim 49020 df-grlic 49023

This theorem is used by: grlicsymb 49056 grlicer 49058 usgrexmpl12ngrlic 49081

W3C validator