Metamath Proof Explorer

Theorem isupgr

Description: The property of being an undirected pseudograph. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Hypotheses isupgr.v ⊢V=Vtx⁡G
isupgr.e ⊢E=iEdg⁡G
Assertion isupgr ⊢G∈U→G∈UPGraph↔E:dom⁡E⟶x∈𝒫V∖∅|x≤2

Proof

Step Hyp Ref Expression
1 isupgr.v ⊢V=Vtx⁡G
2 isupgr.e ⊢E=iEdg⁡G
3 df-upgr ⊢UPGraph=g|[˙Vtx⁡g/v]˙[˙iEdg⁡g/e]˙e:dom⁡e⟶x∈𝒫v∖∅|x≤2
4 3 eleq2i ⊢G∈UPGraph↔G∈g|[˙Vtx⁡g/v]˙[˙iEdg⁡g/e]˙e:dom⁡e⟶x∈𝒫v∖∅|x≤2
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 14 rabeqdv ⊢h=G→x∈𝒫Vtx⁡h∖∅|x≤2=x∈𝒫V∖∅|x≤2
16 6 10 15 feq123d ⊢h=G→iEdg⁡h:dom⁡iEdg⁡h⟶x∈𝒫Vtx⁡h∖∅|x≤2↔E:dom⁡E⟶x∈𝒫V∖∅|x≤2
17 fvexd ⊢g=h→Vtx⁡g∈V
18 fveq2 ⊢g=h→Vtx⁡g=Vtx⁡h
19 fvexd ⊢g=h∧v=Vtx⁡h→iEdg⁡g∈V
20 fveq2 ⊢g=h→iEdg⁡g=iEdg⁡h
21 20 adantr ⊢g=h∧v=Vtx⁡h→iEdg⁡g=iEdg⁡h
22 simpr ⊢g=h∧v=Vtx⁡h∧e=iEdg⁡h→e=iEdg⁡h
23 22 dmeqd ⊢g=h∧v=Vtx⁡h∧e=iEdg⁡h→dom⁡e=dom⁡iEdg⁡h
24 pweq ⊢v=Vtx⁡h→𝒫v=𝒫Vtx⁡h
25 24 ad2antlr ⊢g=h∧v=Vtx⁡h∧e=iEdg⁡h→𝒫v=𝒫Vtx⁡h
26 25 difeq1d ⊢g=h∧v=Vtx⁡h∧e=iEdg⁡h→𝒫v∖∅=𝒫Vtx⁡h∖∅
27 26 rabeqdv ⊢g=h∧v=Vtx⁡h∧e=iEdg⁡h→x∈𝒫v∖∅|x≤2=x∈𝒫Vtx⁡h∖∅|x≤2
28 22 23 27 feq123d ⊢g=h∧v=Vtx⁡h∧e=iEdg⁡h→e:dom⁡e⟶x∈𝒫v∖∅|x≤2↔iEdg⁡h:dom⁡iEdg⁡h⟶x∈𝒫Vtx⁡h∖∅|x≤2
29 19 21 28 sbcied2 ⊢g=h∧v=Vtx⁡h→[˙iEdg⁡g/e]˙e:dom⁡e⟶x∈𝒫v∖∅|x≤2↔iEdg⁡h:dom⁡iEdg⁡h⟶x∈𝒫Vtx⁡h∖∅|x≤2
30 17 18 29 sbcied2 ⊢g=h→[˙Vtx⁡g/v]˙[˙iEdg⁡g/e]˙e:dom⁡e⟶x∈𝒫v∖∅|x≤2↔iEdg⁡h:dom⁡iEdg⁡h⟶x∈𝒫Vtx⁡h∖∅|x≤2
31 30 cbvabv ⊢g|[˙Vtx⁡g/v]˙[˙iEdg⁡g/e]˙e:dom⁡e⟶x∈𝒫v∖∅|x≤2=h|iEdg⁡h:dom⁡iEdg⁡h⟶x∈𝒫Vtx⁡h∖∅|x≤2
32 16 31 elab2g ⊢G∈U→G∈g|[˙Vtx⁡g/v]˙[˙iEdg⁡g/e]˙e:dom⁡e⟶x∈𝒫v∖∅|x≤2↔E:dom⁡E⟶x∈𝒫V∖∅|x≤2
33 4 32 bitrid ⊢G∈U→G∈UPGraph↔E:dom⁡E⟶x∈𝒫V∖∅|x≤2