Metamath Proof Explorer

Theorem uspgr1e

Description: A simple pseudograph with one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 17-Apr-2021)

Ref Expression
Hypotheses uspgr1e.v ⊢ V = Vtx ⁡ G
uspgr1e.a ⊢ φ → A ∈ X
uspgr1e.b ⊢ φ → B ∈ V
uspgr1e.c ⊢ φ → C ∈ V
uspgr1e.e ⊢ φ → iEdg ⁡ G = A B C
Assertion uspgr1e ⊢ φ → G ∈ USHGraph

Proof

Step Hyp Ref Expression
1 uspgr1e.v ⊢ V = Vtx ⁡ G
2 uspgr1e.a ⊢ φ → A ∈ X
3 uspgr1e.b ⊢ φ → B ∈ V
4 uspgr1e.c ⊢ φ → C ∈ V
5 uspgr1e.e ⊢ φ → iEdg ⁡ G = A B C
6 prex ⊢ B C ∈ V
7 6 snid ⊢ B C ∈ B C
8 f1sng ⊢ A ∈ X ∧ B C ∈ B C → A B C : A ⟶ 1-1 B C
9 2 7 8 sylancl ⊢ φ → A B C : A ⟶ 1-1 B C
10 3 4 prssd ⊢ φ → B C ⊆ V
11 10 1 sseqtrdi ⊢ φ → B C ⊆ Vtx ⁡ G
12 6 elpw ⊢ B C ∈ 𝒫 Vtx ⁡ G ↔ B C ⊆ Vtx ⁡ G
13 11 12 sylibr ⊢ φ → B C ∈ 𝒫 Vtx ⁡ G
14 13 3 upgr1elem ⊢ φ → B C ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
15 f1ss ⊢ A B C : A ⟶ 1-1 B C ∧ B C ⊆ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 → A B C : A ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
16 9 14 15 syl2anc ⊢ φ → A B C : A ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
17 6 a1i ⊢ φ → B C ∈ V
18 17 3 upgr1elem ⊢ φ → B C ⊆ x ∈ V ∖ ∅ | x ≤ 2
19 f1ss ⊢ A B C : A ⟶ 1-1 B C ∧ B C ⊆ x ∈ V ∖ ∅ | x ≤ 2 → A B C : A ⟶ 1-1 x ∈ V ∖ ∅ | x ≤ 2
20 9 18 19 syl2anc ⊢ φ → A B C : A ⟶ 1-1 x ∈ V ∖ ∅ | x ≤ 2
21 f1dm ⊢ A B C : A ⟶ 1-1 x ∈ V ∖ ∅ | x ≤ 2 → dom ⁡ A B C = A
22 f1eq2 ⊢ dom ⁡ A B C = A → A B C : dom ⁡ A B C ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ↔ A B C : A ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
23 20 21 22 3syl ⊢ φ → A B C : dom ⁡ A B C ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ↔ A B C : A ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
24 16 23 mpbird ⊢ φ → A B C : dom ⁡ A B C ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
25 5 dmeqd ⊢ φ → dom ⁡ iEdg ⁡ G = dom ⁡ A B C
26 eqidd ⊢ φ → x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 = x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
27 5 25 26 f1eq123d ⊢ φ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ↔ A B C : dom ⁡ A B C ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
28 24 27 mpbird ⊢ φ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
29 1 1vgrex ⊢ B ∈ V → G ∈ V
30 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
31 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
32 30 31 isuspgr ⊢ G ∈ V → G ∈ USHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
33 3 29 32 3syl ⊢ φ → G ∈ USHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
34 28 33 mpbird ⊢ φ → G ∈ USHGraph