Metamath Proof Explorer

Theorem isushgr

Description: The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020) (Revised by AV, 9-Oct-2020)

Ref Expression
Hypotheses isuhgr.v ⊢V=Vtx⁡G
isuhgr.e ⊢E=iEdg⁡G
Assertion isushgr ⊢G∈U→G∈USHGraph↔E:dom⁡E⟶1-1𝒫V∖∅

Proof

Step Hyp Ref Expression
1 isuhgr.v ⊢V=Vtx⁡G
2 isuhgr.e ⊢E=iEdg⁡G
3 df-ushgr ⊢USHGraph=g|[˙Vtx⁡g/v]˙[˙iEdg⁡g/e]˙e:dom⁡e⟶1-1𝒫v∖∅
4 3 eleq2i ⊢G∈USHGraph↔G∈g|[˙Vtx⁡g/v]˙[˙iEdg⁡g/e]˙e:dom⁡e⟶1-1𝒫v∖∅
5 fveq2 ⊢h=G→iEdg⁡h=iEdg⁡G
6 5 2 eqtr4di ⊢h=G→iEdg⁡h=E
7 5 dmeqd ⊢h=G→dom⁡iEdg⁡h=dom⁡iEdg⁡G
8 2 eqcomi ⊢iEdg⁡G=E
9 8 dmeqi ⊢dom⁡iEdg⁡G=dom⁡E
10 7 9 eqtrdi ⊢h=G→dom⁡iEdg⁡h=dom⁡E
11 fveq2 ⊢h=G→Vtx⁡h=Vtx⁡G
12 11 1 eqtr4di ⊢h=G→Vtx⁡h=V
13 12 pweqd ⊢h=G→𝒫Vtx⁡h=𝒫V
14 13 difeq1d ⊢h=G→𝒫Vtx⁡h∖∅=𝒫V∖∅
15 6 10 14 f1eq123d ⊢h=G→iEdg⁡h:dom⁡iEdg⁡h⟶1-1𝒫Vtx⁡h∖∅↔E:dom⁡E⟶1-1𝒫V∖∅
16 fvexd ⊢g=h→Vtx⁡g∈V
17 fveq2 ⊢g=h→Vtx⁡g=Vtx⁡h
18 fvexd ⊢g=h∧v=Vtx⁡h→iEdg⁡g∈V
19 fveq2 ⊢g=h→iEdg⁡g=iEdg⁡h
20 19 adantr ⊢g=h∧v=Vtx⁡h→iEdg⁡g=iEdg⁡h
21 simpr ⊢g=h∧v=Vtx⁡h∧e=iEdg⁡h→e=iEdg⁡h
22 21 dmeqd ⊢g=h∧v=Vtx⁡h∧e=iEdg⁡h→dom⁡e=dom⁡iEdg⁡h
23 simpr ⊢g=h∧v=Vtx⁡h→v=Vtx⁡h
24 23 pweqd ⊢g=h∧v=Vtx⁡h→𝒫v=𝒫Vtx⁡h
25 24 difeq1d ⊢g=h∧v=Vtx⁡h→𝒫v∖∅=𝒫Vtx⁡h∖∅
26 25 adantr ⊢g=h∧v=Vtx⁡h∧e=iEdg⁡h→𝒫v∖∅=𝒫Vtx⁡h∖∅
27 21 22 26 f1eq123d ⊢g=h∧v=Vtx⁡h∧e=iEdg⁡h→e:dom⁡e⟶1-1𝒫v∖∅↔iEdg⁡h:dom⁡iEdg⁡h⟶1-1𝒫Vtx⁡h∖∅
28 18 20 27 sbcied2 ⊢g=h∧v=Vtx⁡h→[˙iEdg⁡g/e]˙e:dom⁡e⟶1-1𝒫v∖∅↔iEdg⁡h:dom⁡iEdg⁡h⟶1-1𝒫Vtx⁡h∖∅
29 16 17 28 sbcied2 ⊢g=h→[˙Vtx⁡g/v]˙[˙iEdg⁡g/e]˙e:dom⁡e⟶1-1𝒫v∖∅↔iEdg⁡h:dom⁡iEdg⁡h⟶1-1𝒫Vtx⁡h∖∅
30 29 cbvabv ⊢g|[˙Vtx⁡g/v]˙[˙iEdg⁡g/e]˙e:dom⁡e⟶1-1𝒫v∖∅=h|iEdg⁡h:dom⁡iEdg⁡h⟶1-1𝒫Vtx⁡h∖∅
31 15 30 elab2g ⊢G∈U→G∈g|[˙Vtx⁡g/v]˙[˙iEdg⁡g/e]˙e:dom⁡e⟶1-1𝒫v∖∅↔E:dom⁡E⟶1-1𝒫V∖∅
32 4 31 syl5bb ⊢G∈U→G∈USHGraph↔E:dom⁡E⟶1-1𝒫V∖∅