Theorem incistruhgr

Description: Anincidence structure <. P , L , I >. "where P is a set whose elements are calledpoints, L is a distinct set whose elements are calledlines and I C_ ( P X. L ) is theincidence 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 P = ( BaseS ) 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 incidence structureis 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)

	Ref	Expression
Hypotheses	incistruhgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	incistruhgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	incistruhgr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → ( ( 𝑉 = 𝑃 ∧ 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } ) ) → 𝐺 ∈ UHGraph ) )

Proof

Step	Hyp	Ref	Expression
1		incistruhgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		incistruhgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		rabeq	⊢ ( 𝑉 = 𝑃 → { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } = { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } )
4	3	mpteq2dv	⊢ ( 𝑉 = 𝑃 → ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } ) )
5	4	eqeq2d	⊢ ( 𝑉 = 𝑃 → ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) ↔ 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } ) ) )
6		xpeq1	⊢ ( 𝑉 = 𝑃 → ( 𝑉 × 𝐿 ) = ( 𝑃 × 𝐿 ) )
7	6	sseq2d	⊢ ( 𝑉 = 𝑃 → ( 𝐼 ⊆ ( 𝑉 × 𝐿 ) ↔ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ) )
8	7	3anbi2d	⊢ ( 𝑉 = 𝑃 → ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ↔ ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ) )
9	5 8	anbi12d	⊢ ( 𝑉 = 𝑃 → ( ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) ∧ ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ) ↔ ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } ) ∧ ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ) ) )
10		dmeq	⊢ ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) → dom 𝐸 = dom ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) )
11	1	fvexi	⊢ 𝑉 ∈ V
12	11	rabex	⊢ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ∈ V
13		eqid	⊢ ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } )
14	12 13	dmmpti	⊢ dom ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) = 𝐿
15	10 14	eqtrdi	⊢ ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) → dom 𝐸 = 𝐿 )
16		ssrab2	⊢ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ⊆ 𝑉
17	16	a1i	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ∧ 𝑒 ∈ 𝐿 ) → { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ⊆ 𝑉 )
18	12	elpw	⊢ ( { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ∈ 𝒫 𝑉 ↔ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ⊆ 𝑉 )
19	17 18	sylibr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ∧ 𝑒 ∈ 𝐿 ) → { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ∈ 𝒫 𝑉 )
20		eleq2	⊢ ( ran 𝐼 = 𝐿 → ( 𝑒 ∈ ran 𝐼 ↔ 𝑒 ∈ 𝐿 ) )
21	20	3ad2ant3	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → ( 𝑒 ∈ ran 𝐼 ↔ 𝑒 ∈ 𝐿 ) )
22		ssrelrn	⊢ ( ( 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ 𝑒 ∈ ran 𝐼 ) → ∃ 𝑣 ∈ 𝑉 𝑣 𝐼 𝑒 )
23	22	ex	⊢ ( 𝐼 ⊆ ( 𝑉 × 𝐿 ) → ( 𝑒 ∈ ran 𝐼 → ∃ 𝑣 ∈ 𝑉 𝑣 𝐼 𝑒 ) )
24	23	3ad2ant2	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → ( 𝑒 ∈ ran 𝐼 → ∃ 𝑣 ∈ 𝑉 𝑣 𝐼 𝑒 ) )
25	21 24	sylbird	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → ( 𝑒 ∈ 𝐿 → ∃ 𝑣 ∈ 𝑉 𝑣 𝐼 𝑒 ) )
26	25	imp	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ∧ 𝑒 ∈ 𝐿 ) → ∃ 𝑣 ∈ 𝑉 𝑣 𝐼 𝑒 )
27		df-ne	⊢ ( { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ≠ ∅ ↔ ¬ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } = ∅ )
28		rabn0	⊢ ( { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ≠ ∅ ↔ ∃ 𝑣 ∈ 𝑉 𝑣 𝐼 𝑒 )
29	27 28	bitr3i	⊢ ( ¬ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } = ∅ ↔ ∃ 𝑣 ∈ 𝑉 𝑣 𝐼 𝑒 )
30	26 29	sylibr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ∧ 𝑒 ∈ 𝐿 ) → ¬ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } = ∅ )
31	12	elsn	⊢ ( { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ∈ { ∅ } ↔ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } = ∅ )
32	30 31	sylnibr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ∧ 𝑒 ∈ 𝐿 ) → ¬ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ∈ { ∅ } )
33	19 32	eldifd	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ∧ 𝑒 ∈ 𝐿 ) → { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ∈ ( 𝒫 𝑉 ∖ { ∅ } ) )
34	33	fmpttd	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) : 𝐿 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
35		simpl	⊢ ( ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) ∧ dom 𝐸 = 𝐿 ) → 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) )
36		simpr	⊢ ( ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) ∧ dom 𝐸 = 𝐿 ) → dom 𝐸 = 𝐿 )
37	35 36	feq12d	⊢ ( ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) ∧ dom 𝐸 = 𝐿 ) → ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) : 𝐿 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
38	34 37	syl5ibr	⊢ ( ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) ∧ dom 𝐸 = 𝐿 ) → ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
39	15 38	mpdan	⊢ ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) → ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
40	39	imp	⊢ ( ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑉 ∣ 𝑣 𝐼 𝑒 } ) ∧ ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑉 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ) → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
41	9 40	syl6bir	⊢ ( 𝑉 = 𝑃 → ( ( 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } ) ∧ ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ) → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
42	41	expdimp	⊢ ( ( 𝑉 = 𝑃 ∧ 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } ) ) → ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
43	42	impcom	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ∧ ( 𝑉 = 𝑃 ∧ 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } ) ) ) → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
44	1 2	isuhgr	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
45	44	3ad2ant1	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → ( 𝐺 ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
46	45	adantr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ∧ ( 𝑉 = 𝑃 ∧ 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } ) ) ) → ( 𝐺 ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
47	43 46	mpbird	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) ∧ ( 𝑉 = 𝑃 ∧ 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } ) ) ) → 𝐺 ∈ UHGraph )
48	47	ex	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → ( ( 𝑉 = 𝑃 ∧ 𝐸 = ( 𝑒 ∈ 𝐿 ↦ { 𝑣 ∈ 𝑃 ∣ 𝑣 𝐼 𝑒 } ) ) → 𝐺 ∈ UHGraph ) )