Metamath Proof Explorer

Theorem usgruspgrb

Description: A class is a simple graph iff it is a simple pseudograph without loops. (Contributed by AV, 18-Oct-2020)

Ref Expression
Assertion usgruspgrb ( 𝐺 ∈ USGraph ↔ ( 𝐺 ∈ USPGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ) )

Proof

Step Hyp Ref Expression
1 usgruspgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
2 edgusgr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑒 ) = 2 ) )
3 2 simprd ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( ♯ ‘ 𝑒 ) = 2 )
4 3 ralrimiva ⊢ ( 𝐺 ∈ USGraph → ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 )
5 1 4 jca ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 ∈ USPGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ) )
6 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
7 6 a1i ⊢ ( 𝐺 ∈ USPGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
8 7 raleqdv ⊢ ( 𝐺 ∈ USPGraph → ( ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ↔ ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ) )
9 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
11 9 10 uspgrf ⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
12 f1f ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
13 12 frnd ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
14 ssel2 ⊢ ( ( ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ 𝑦 ∈ ran ( iEdg ‘ 𝐺 ) ) → 𝑦 ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
15 14 expcom ⊢ ( 𝑦 ∈ ran ( iEdg ‘ 𝐺 ) → ( ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → 𝑦 ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
16 fveqeq2 ⊢ ( 𝑒 = 𝑦 → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ 𝑦 ) = 2 ) )
17 16 rspcv ⊢ ( 𝑦 ∈ ran ( iEdg ‘ 𝐺 ) → ( ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 → ( ♯ ‘ 𝑦 ) = 2 ) )
18 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
19 18 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑥 ) ≤ 2 ↔ ( ♯ ‘ 𝑦 ) ≤ 2 ) )
20 19 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ ( 𝑦 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ( ♯ ‘ 𝑦 ) ≤ 2 ) )
21 eldifi ⊢ ( 𝑦 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → 𝑦 ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
22 21 anim1i ⊢ ( ( 𝑦 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ( ♯ ‘ 𝑦 ) = 2 ) → ( 𝑦 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = 2 ) )
23 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ 𝑦 ) = 2 ) )
24 23 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( 𝑦 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑦 ) = 2 ) )
25 22 24 sylibr ⊢ ( ( 𝑦 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ( ♯ ‘ 𝑦 ) = 2 ) → 𝑦 ∈ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
26 25 ex ⊢ ( 𝑦 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → ( ( ♯ ‘ 𝑦 ) = 2 → 𝑦 ∈ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
27 26 adantr ⊢ ( ( 𝑦 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ( ♯ ‘ 𝑦 ) ≤ 2 ) → ( ( ♯ ‘ 𝑦 ) = 2 → 𝑦 ∈ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
28 20 27 sylbi ⊢ ( 𝑦 ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( ( ♯ ‘ 𝑦 ) = 2 → 𝑦 ∈ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
29 17 28 syl9 ⊢ ( 𝑦 ∈ ran ( iEdg ‘ 𝐺 ) → ( 𝑦 ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 → 𝑦 ∈ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
30 15 29 syld ⊢ ( 𝑦 ∈ ran ( iEdg ‘ 𝐺 ) → ( ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 → 𝑦 ∈ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
31 30 com13 ⊢ ( ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 → ( ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( 𝑦 ∈ ran ( iEdg ‘ 𝐺 ) → 𝑦 ∈ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
32 31 imp ⊢ ( ( ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ∧ ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) → ( 𝑦 ∈ ran ( iEdg ‘ 𝐺 ) → 𝑦 ∈ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
33 32 ssrdv ⊢ ( ( ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ∧ ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
34 33 ex ⊢ ( ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 → ( ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
35 13 34 mpan9 ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ) → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
36 f1ssr ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
37 35 36 syldan ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
38 37 ex ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
39 11 38 syl ⊢ ( 𝐺 ∈ USPGraph → ( ∀ 𝑒 ∈ ran ( iEdg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
40 8 39 sylbid ⊢ ( 𝐺 ∈ USPGraph → ( ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
41 40 imp ⊢ ( ( 𝐺 ∈ USPGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
42 9 10 isusgrs ⊢ ( 𝐺 ∈ USPGraph → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
43 42 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ) → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
44 41 43 mpbird ⊢ ( ( 𝐺 ∈ USPGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ) → 𝐺 ∈ USGraph )
45 5 44 impbii ⊢ ( 𝐺 ∈ USGraph ↔ ( 𝐺 ∈ USPGraph ∧ ∀ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( ♯ ‘ 𝑒 ) = 2 ) )