Metamath Proof Explorer

Theorem ausgrusgri

Description: The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 15-Oct-2020)

Ref Expression
Hypotheses ausgr.1 ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } }
ausgrusgri.1 ⊢ 𝑂 = { 𝑓 ∣ 𝑓 : dom 𝑓 –1-1→ ran 𝑓 }
Assertion ausgrusgri ( ( 𝐻 ∈ 𝑊 ∧ ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → 𝐻 ∈ USGraph )

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } }
2 ausgrusgri.1 ⊢ 𝑂 = { 𝑓 ∣ 𝑓 : dom 𝑓 –1-1→ ran 𝑓 }
3 fvex ⊢ ( Vtx ‘ 𝐻 ) ∈ V
4 fvex ⊢ ( Edg ‘ 𝐻 ) ∈ V
5 1 isausgr ⊢ ( ( ( Vtx ‘ 𝐻 ) ∈ V ∧ ( Edg ‘ 𝐻 ) ∈ V ) → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ↔ ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
6 3 4 5 mp2an ⊢ ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ↔ ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
7 edgval ⊢ ( Edg ‘ 𝐻 ) = ran ( iEdg ‘ 𝐻 )
8 7 a1i ⊢ ( 𝐻 ∈ 𝑊 → ( Edg ‘ 𝐻 ) = ran ( iEdg ‘ 𝐻 ) )
9 8 sseq1d ⊢ ( 𝐻 ∈ 𝑊 → ( ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
10 2 eleq2i ⊢ ( ( iEdg ‘ 𝐻 ) ∈ 𝑂 ↔ ( iEdg ‘ 𝐻 ) ∈ { 𝑓 ∣ 𝑓 : dom 𝑓 –1-1→ ran 𝑓 } )
11 fvex ⊢ ( iEdg ‘ 𝐻 ) ∈ V
12 id ⊢ ( 𝑓 = ( iEdg ‘ 𝐻 ) → 𝑓 = ( iEdg ‘ 𝐻 ) )
13 dmeq ⊢ ( 𝑓 = ( iEdg ‘ 𝐻 ) → dom 𝑓 = dom ( iEdg ‘ 𝐻 ) )
14 rneq ⊢ ( 𝑓 = ( iEdg ‘ 𝐻 ) → ran 𝑓 = ran ( iEdg ‘ 𝐻 ) )
15 12 13 14 f1eq123d ⊢ ( 𝑓 = ( iEdg ‘ 𝐻 ) → ( 𝑓 : dom 𝑓 –1-1→ ran 𝑓 ↔ ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ ran ( iEdg ‘ 𝐻 ) ) )
16 11 15 elab ⊢ ( ( iEdg ‘ 𝐻 ) ∈ { 𝑓 ∣ 𝑓 : dom 𝑓 –1-1→ ran 𝑓 } ↔ ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ ran ( iEdg ‘ 𝐻 ) )
17 10 16 sylbb ⊢ ( ( iEdg ‘ 𝐻 ) ∈ 𝑂 → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ ran ( iEdg ‘ 𝐻 ) )
18 17 3ad2ant3 ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ ran ( iEdg ‘ 𝐻 ) )
19 simp2 ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
20 f1ssr ⊢ ( ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ ran ( iEdg ‘ 𝐻 ) ∧ ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
21 18 19 20 syl2anc ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
22 21 3exp ⊢ ( 𝐻 ∈ 𝑊 → ( ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( ( iEdg ‘ 𝐻 ) ∈ 𝑂 → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
23 9 22 sylbid ⊢ ( 𝐻 ∈ 𝑊 → ( ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( ( iEdg ‘ 𝐻 ) ∈ 𝑂 → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
24 6 23 biimtrid ⊢ ( 𝐻 ∈ 𝑊 → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) → ( ( iEdg ‘ 𝐻 ) ∈ 𝑂 → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
25 24 3imp ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
26 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
27 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
28 26 27 isusgrs ⊢ ( 𝐻 ∈ 𝑊 → ( 𝐻 ∈ USGraph ↔ ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
29 28 3ad2ant1 ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → ( 𝐻 ∈ USGraph ↔ ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
30 25 29 mpbird ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → 𝐻 ∈ USGraph )