Metamath Proof Explorer

Theorem upgr1e

Description: A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 16-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 17-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 upgr1e.v ⊢ V = Vtx ⁡ G
2 upgr1e.a ⊢ φ → A ∈ X
3 upgr1e.b ⊢ φ → B ∈ V
4 upgr1e.c ⊢ φ → C ∈ V
5 upgr1e.e ⊢ φ → iEdg ⁡ G = A B C
6 prex ⊢ B C ∈ V
7 6 snid ⊢ B C ∈ B C
8 7 a1i ⊢ φ → B C ∈ B C
9 2 8 fsnd ⊢ φ → A B C : A ⟶ 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 9 14 fssd ⊢ φ → A B C : A ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
16 15 ffdmd ⊢ φ → A B C : dom ⁡ A B C ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
17 5 dmeqd ⊢ φ → dom ⁡ iEdg ⁡ G = dom ⁡ A B C
18 5 17 feq12d ⊢ φ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ↔ A B C : dom ⁡ A B C ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
19 16 18 mpbird ⊢ φ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
20 1 1vgrex ⊢ B ∈ V → G ∈ V
21 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
22 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
23 21 22 isupgr ⊢ G ∈ V → G ∈ UPGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
24 3 20 23 3syl ⊢ φ → G ∈ UPGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
25 19 24 mpbird ⊢ φ → G ∈ UPGraph