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 ⊢ G ∈ USGraph ↔ G ∈ USHGraph ∧ ∀ e ∈ Edg ⁡ G e = 2

Proof

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