Metamath Proof Explorer


Theorem isuhgr

Description: The predicate "is an undirected hypergraph." (Contributed by Alexander van der Vekens, 26-Dec-2017) (Revised by AV, 9-Oct-2020)

Ref Expression
Hypotheses isuhgr.v 𝑉 = ( Vtx ‘ 𝐺 )
isuhgr.e 𝐸 = ( iEdg ‘ 𝐺 )
Assertion isuhgr ( 𝐺𝑈 → ( 𝐺 ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )

Proof

Step Hyp Ref Expression
1 isuhgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 isuhgr.e 𝐸 = ( iEdg ‘ 𝐺 )
3 df-uhgr UHGraph = { 𝑔[ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) }
4 3 eleq2i ( 𝐺 ∈ UHGraph ↔ 𝐺 ∈ { 𝑔[ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) } )
5 fveq2 ( = 𝐺 → ( iEdg ‘ ) = ( iEdg ‘ 𝐺 ) )
6 5 2 eqtr4di ( = 𝐺 → ( iEdg ‘ ) = 𝐸 )
7 5 dmeqd ( = 𝐺 → dom ( iEdg ‘ ) = dom ( iEdg ‘ 𝐺 ) )
8 2 eqcomi ( iEdg ‘ 𝐺 ) = 𝐸
9 8 dmeqi dom ( iEdg ‘ 𝐺 ) = dom 𝐸
10 7 9 eqtrdi ( = 𝐺 → dom ( iEdg ‘ ) = dom 𝐸 )
11 fveq2 ( = 𝐺 → ( Vtx ‘ ) = ( Vtx ‘ 𝐺 ) )
12 11 1 eqtr4di ( = 𝐺 → ( Vtx ‘ ) = 𝑉 )
13 12 pweqd ( = 𝐺 → 𝒫 ( Vtx ‘ ) = 𝒫 𝑉 )
14 13 difeq1d ( = 𝐺 → ( 𝒫 ( Vtx ‘ ) ∖ { ∅ } ) = ( 𝒫 𝑉 ∖ { ∅ } ) )
15 6 10 14 feq123d ( = 𝐺 → ( ( iEdg ‘ ) : dom ( iEdg ‘ ) ⟶ ( 𝒫 ( Vtx ‘ ) ∖ { ∅ } ) ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
16 fvexd ( 𝑔 = → ( Vtx ‘ 𝑔 ) ∈ V )
17 fveq2 ( 𝑔 = → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ ) )
18 fvexd ( ( 𝑔 = 𝑣 = ( Vtx ‘ ) ) → ( iEdg ‘ 𝑔 ) ∈ V )
19 fveq2 ( 𝑔 = → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ ) )
20 19 adantr ( ( 𝑔 = 𝑣 = ( Vtx ‘ ) ) → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ ) )
21 simpr ( ( ( 𝑔 = 𝑣 = ( Vtx ‘ ) ) ∧ 𝑒 = ( iEdg ‘ ) ) → 𝑒 = ( iEdg ‘ ) )
22 21 dmeqd ( ( ( 𝑔 = 𝑣 = ( Vtx ‘ ) ) ∧ 𝑒 = ( iEdg ‘ ) ) → dom 𝑒 = dom ( iEdg ‘ ) )
23 simpr ( ( 𝑔 = 𝑣 = ( Vtx ‘ ) ) → 𝑣 = ( Vtx ‘ ) )
24 23 pweqd ( ( 𝑔 = 𝑣 = ( Vtx ‘ ) ) → 𝒫 𝑣 = 𝒫 ( Vtx ‘ ) )
25 24 difeq1d ( ( 𝑔 = 𝑣 = ( Vtx ‘ ) ) → ( 𝒫 𝑣 ∖ { ∅ } ) = ( 𝒫 ( Vtx ‘ ) ∖ { ∅ } ) )
26 25 adantr ( ( ( 𝑔 = 𝑣 = ( Vtx ‘ ) ) ∧ 𝑒 = ( iEdg ‘ ) ) → ( 𝒫 𝑣 ∖ { ∅ } ) = ( 𝒫 ( Vtx ‘ ) ∖ { ∅ } ) )
27 21 22 26 feq123d ( ( ( 𝑔 = 𝑣 = ( Vtx ‘ ) ) ∧ 𝑒 = ( iEdg ‘ ) ) → ( 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) ↔ ( iEdg ‘ ) : dom ( iEdg ‘ ) ⟶ ( 𝒫 ( Vtx ‘ ) ∖ { ∅ } ) ) )
28 18 20 27 sbcied2 ( ( 𝑔 = 𝑣 = ( Vtx ‘ ) ) → ( [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) ↔ ( iEdg ‘ ) : dom ( iEdg ‘ ) ⟶ ( 𝒫 ( Vtx ‘ ) ∖ { ∅ } ) ) )
29 16 17 28 sbcied2 ( 𝑔 = → ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) ↔ ( iEdg ‘ ) : dom ( iEdg ‘ ) ⟶ ( 𝒫 ( Vtx ‘ ) ∖ { ∅ } ) ) )
30 29 cbvabv { 𝑔[ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) } = { ∣ ( iEdg ‘ ) : dom ( iEdg ‘ ) ⟶ ( 𝒫 ( Vtx ‘ ) ∖ { ∅ } ) }
31 15 30 elab2g ( 𝐺𝑈 → ( 𝐺 ∈ { 𝑔[ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) } ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
32 4 31 syl5bb ( 𝐺𝑈 → ( 𝐺 ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )