Metamath Proof Explorer

Theorem ausgrusgrb

Description: The equivalence of the definitions of a simple graph. (Contributed by Alexander van der Vekens, 28-Aug-2017) (Revised by AV, 14-Oct-2020)

Ref Expression
Hypothesis ausgr.1 ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } }
Assertion ausgrusgrb ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝑉 𝐺 𝐸 ↔ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ∈ USGraph ) )

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } }
2 1 isausgr ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝑉 𝐺 𝐸 ↔ 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
3 f1oi ⊢ ( I ↾ 𝐸 ) : 𝐸 –1-1-onto→ 𝐸
4 dff1o5 ⊢ ( ( I ↾ 𝐸 ) : 𝐸 –1-1-onto→ 𝐸 ↔ ( ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐸 ∧ ran ( I ↾ 𝐸 ) = 𝐸 ) )
5 f1ss ⊢ ( ( ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐸 ∧ 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) → ( I ↾ 𝐸 ) : 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
6 dmresi ⊢ dom ( I ↾ 𝐸 ) = 𝐸
7 6 eqcomi ⊢ 𝐸 = dom ( I ↾ 𝐸 )
8 f1eq2 ⊢ ( 𝐸 = dom ( I ↾ 𝐸 ) → ( ( I ↾ 𝐸 ) : 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
9 7 8 ax-mp ⊢ ( ( I ↾ 𝐸 ) : 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
10 5 9 sylib ⊢ ( ( ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐸 ∧ 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) → ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
11 10 ex ⊢ ( ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐸 → ( 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
12 11 a1d ⊢ ( ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐸 → ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
13 12 adantr ⊢ ( ( ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐸 ∧ ran ( I ↾ 𝐸 ) = 𝐸 ) → ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
14 4 13 sylbi ⊢ ( ( I ↾ 𝐸 ) : 𝐸 –1-1-onto→ 𝐸 → ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
15 3 14 ax-mp ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
16 df-f ⊢ ( ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( ( I ↾ 𝐸 ) Fn dom ( I ↾ 𝐸 ) ∧ ran ( I ↾ 𝐸 ) ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
17 rnresi ⊢ ran ( I ↾ 𝐸 ) = 𝐸
18 17 sseq1i ⊢ ( ran ( I ↾ 𝐸 ) ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
19 18 biimpi ⊢ ( ran ( I ↾ 𝐸 ) ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
20 19 a1d ⊢ ( ran ( I ↾ 𝐸 ) ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
21 16 20 simplbiim ⊢ ( ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
22 f1f ⊢ ( ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
23 21 22 syl11 ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
24 15 23 impbid ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
25 resiexg ⊢ ( 𝐸 ∈ 𝑌 → ( I ↾ 𝐸 ) ∈ V )
26 opiedgfv ⊢ ( ( 𝑉 ∈ 𝑋 ∧ ( I ↾ 𝐸 ) ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = ( I ↾ 𝐸 ) )
27 25 26 sylan2 ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = ( I ↾ 𝐸 ) )
28 27 dmeqd ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = dom ( I ↾ 𝐸 ) )
29 opvtxfv ⊢ ( ( 𝑉 ∈ 𝑋 ∧ ( I ↾ 𝐸 ) ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = 𝑉 )
30 25 29 sylan2 ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = 𝑉 )
31 30 pweqd ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = 𝒫 𝑉 )
32 31 rabeqdv ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
33 27 28 32 f1eq123d ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( I ↾ 𝐸 ) : dom ( I ↾ 𝐸 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
34 24 33 bitr4d ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
35 opex ⊢ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ∈ V
36 eqid ⊢ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ )
37 eqid ⊢ ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ )
38 36 37 isusgrs ⊢ ( ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ∈ V → ( ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ∈ USGraph ↔ ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
39 35 38 ax-mp ⊢ ( ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ∈ USGraph ↔ ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
40 39 bicomi ⊢ ( ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ∈ USGraph )
41 40 a1i ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ∈ USGraph ) )
42 2 34 41 3bitrd ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝑉 𝐺 𝐸 ↔ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ∈ USGraph ) )