Theorem incistruhgr 25746

Description: An incident structure ⟨𝑃, 𝐿, 𝐼⟩ "where 𝑃 is a set whose elements are called points, 𝐿 is a distinct set whose elements are called lines and 𝐼 ⊆ (𝑃 × 𝐿) is the incidence relation" ( see Wikipedia "Incidence structure" (24-Oct-2020), https://en.wikipedia.org/wiki/Incidence_structure) implies an undirected hypergraph, if the incidence relation is right-total (to exclude empty edges). The points become the vertices, and the edge function is derived from the incidence relation by mapping each line ("edge") to the set of vertices incident to the line/edge. With 𝑃 = (Base‘𝑆) and by defining two new slots for lines and incidence relations (analogous to LineG and Itv) and enhancing the definition of iEdg accordingly, it would even be possible to express that a corresponding incident structure is an undirected hypergraph. By choosing the incident relation appropriately, other kinds of undirected graphs (pseudographs, multigraphs, simple graphs, etc.) could be defined. (Contributed by AV, 24-Oct-2020.)

Hypotheses

Ref	Expression
incistruhgr.v	⊢ 𝑉 = (Vtx‘𝐺)
incistruhgr.e	⊢ 𝐸 = (iEdg‘𝐺)

Assertion

Ref	Expression
incistruhgr	⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → ((𝑉 = 𝑃 ∧ 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒})) → 𝐺 ∈ UHGraph ))

Distinct variable groups:   𝑒,𝐸   𝑒,𝐺   𝑒,𝐼,𝑣   𝑒,𝐿,𝑣   𝑃,𝑒,𝑣   𝑒,𝑉,𝑣   𝑒,𝑊

Allowed substitution hints:   𝐸(𝑣)   𝐺(𝑣)   𝑊(𝑣)

Proof of Theorem incistruhgr

Step	Hyp	Ref	Expression
1		id 22	. . . . . . . . . 10 ⊢ (𝑉 = 𝑃 → 𝑉 = 𝑃)
2	1	rabeqdv 3167	. . . . . . . . 9 ⊢ (𝑉 = 𝑃 → {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} = {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒})
3	2	mpteq2dv 4673	. . . . . . . 8 ⊢ (𝑉 = 𝑃 → (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒}))
4	3	eqeq2d 2620	. . . . . . 7 ⊢ (𝑉 = 𝑃 → (𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) ↔ 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒})))
5		xpeq1 5052	. . . . . . . . 9 ⊢ (𝑉 = 𝑃 → (𝑉 × 𝐿) = (𝑃 × 𝐿))
6	5	sseq2d 3596	. . . . . . . 8 ⊢ (𝑉 = 𝑃 → (𝐼 ⊆ (𝑉 × 𝐿) ↔ 𝐼 ⊆ (𝑃 × 𝐿)))
7	6	3anbi2d 1396	. . . . . . 7 ⊢ (𝑉 = 𝑃 → ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ↔ (𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿)))
8	4, 7	anbi12d 743	. . . . . 6 ⊢ (𝑉 = 𝑃 → ((𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) ∧ (𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿)) ↔ (𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒}) ∧ (𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿))))
9		dmeq 5246	. . . . . . . . 9 ⊢ (𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) → dom 𝐸 = dom (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}))
10		incistruhgr.v	. . . . . . . . . . . . 13 ⊢ 𝑉 = (Vtx‘𝐺)
11		fvex 6113	. . . . . . . . . . . . 13 ⊢ (Vtx‘𝐺) ∈ V
12	10, 11	eqeltri 2684	. . . . . . . . . . . 12 ⊢ 𝑉 ∈ V
13	12	rabex 4740	. . . . . . . . . . 11 ⊢ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ∈ V
14		eqid 2610	. . . . . . . . . . 11 ⊢ (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒})
15	13, 14	dmmpti 5936	. . . . . . . . . 10 ⊢ dom (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) = 𝐿
16	15	a1i 11	. . . . . . . . 9 ⊢ (𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) → dom (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) = 𝐿)
17	9, 16	eqtrd 2644	. . . . . . . 8 ⊢ (𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) → dom 𝐸 = 𝐿)
18		ssrab2 3650	. . . . . . . . . . . . 13 ⊢ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ⊆ 𝑉
19	18	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒 ∈ 𝐿) → {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ⊆ 𝑉)
20	13	elpw 4114	. . . . . . . . . . . 12 ⊢ ({𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ∈ 𝒫 𝑉 ↔ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ⊆ 𝑉)
21	19, 20	sylibr 223	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒 ∈ 𝐿) → {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ∈ 𝒫 𝑉)
22		eleq2 2677	. . . . . . . . . . . . . . . 16 ⊢ (ran 𝐼 = 𝐿 → (𝑒 ∈ ran 𝐼 ↔ 𝑒 ∈ 𝐿))
23	22	3ad2ant3 1077	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → (𝑒 ∈ ran 𝐼 ↔ 𝑒 ∈ 𝐿))
24		ssrelrn 5237	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ⊆ (𝑉 × 𝐿) ∧ 𝑒 ∈ ran 𝐼) → ∃𝑣 ∈ 𝑉 𝑣𝐼𝑒)
25	24	ex 449	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ⊆ (𝑉 × 𝐿) → (𝑒 ∈ ran 𝐼 → ∃𝑣 ∈ 𝑉 𝑣𝐼𝑒))
26	25	3ad2ant2 1076	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → (𝑒 ∈ ran 𝐼 → ∃𝑣 ∈ 𝑉 𝑣𝐼𝑒))
27	23, 26	sylbird 249	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → (𝑒 ∈ 𝐿 → ∃𝑣 ∈ 𝑉 𝑣𝐼𝑒))
28	27	imp 444	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒 ∈ 𝐿) → ∃𝑣 ∈ 𝑉 𝑣𝐼𝑒)
29		df-ne 2782	. . . . . . . . . . . . . 14 ⊢ ({𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ≠ ∅ ↔ ¬ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} = ∅)
30		rabn0 3912	. . . . . . . . . . . . . 14 ⊢ ({𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ≠ ∅ ↔ ∃𝑣 ∈ 𝑉 𝑣𝐼𝑒)
31	29, 30	bitr3i 265	. . . . . . . . . . . . 13 ⊢ (¬ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} = ∅ ↔ ∃𝑣 ∈ 𝑉 𝑣𝐼𝑒)
32	28, 31	sylibr 223	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒 ∈ 𝐿) → ¬ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} = ∅)
33	13	elsn 4140	. . . . . . . . . . . 12 ⊢ ({𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ∈ {∅} ↔ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} = ∅)
34	32, 33	sylnibr 318	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒 ∈ 𝐿) → ¬ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ∈ {∅})
35	21, 34	eldifd 3551	. . . . . . . . . 10 ⊢ (((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒 ∈ 𝐿) → {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒} ∈ (𝒫 𝑉 ∖ {∅}))
36	35, 14	fmptd 6292	. . . . . . . . 9 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}):𝐿⟶(𝒫 𝑉 ∖ {∅}))
37		simpl 472	. . . . . . . . . 10 ⊢ ((𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) ∧ dom 𝐸 = 𝐿) → 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}))
38		simpr 476	. . . . . . . . . 10 ⊢ ((𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) ∧ dom 𝐸 = 𝐿) → dom 𝐸 = 𝐿)
39	37, 38	feq12d 5946	. . . . . . . . 9 ⊢ ((𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) ∧ dom 𝐸 = 𝐿) → (𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}) ↔ (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}):𝐿⟶(𝒫 𝑉 ∖ {∅})))
40	36, 39	syl5ibr 235	. . . . . . . 8 ⊢ ((𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) ∧ dom 𝐸 = 𝐿) → ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
41	17, 40	mpdan 699	. . . . . . 7 ⊢ (𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) → ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
42	41	imp 444	. . . . . 6 ⊢ ((𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑉 ∣ 𝑣𝐼𝑒}) ∧ (𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿)) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))
43	8, 42	syl6bir 243	. . . . 5 ⊢ (𝑉 = 𝑃 → ((𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒}) ∧ (𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿)) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
44	43	expdimp 452	. . . 4 ⊢ ((𝑉 = 𝑃 ∧ 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒})) → ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
45	44	impcom 445	. . 3 ⊢ (((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ (𝑉 = 𝑃 ∧ 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒}))) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))
46		incistruhgr.e	. . . . . 6 ⊢ 𝐸 = (iEdg‘𝐺)
47	10, 46	isuhgr 25726	. . . . 5 ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
48	47	3ad2ant1 1075	. . . 4 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
49	48	adantr 480	. . 3 ⊢ (((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ (𝑉 = 𝑃 ∧ 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒}))) → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
50	45, 49	mpbird 246	. 2 ⊢ (((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ (𝑉 = 𝑃 ∧ 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒}))) → 𝐺 ∈ UHGraph )
51	50	ex 449	1 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → ((𝑉 = 𝑃 ∧ 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒})) → 𝐺 ∈ UHGraph ))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  dom cdm 5038  ran crn 5039  ⟶wf 5800  ‘cfv 5804  Vtxcvtx 25673  iEdgciedg 25674   UHGraph cuhgr 25722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-uhgr 25724

This theorem is referenced by: (None)