This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgredgpr

Description: If a proper pair (of vertices) is a subset of an edge in a pseudograph, the pair is the edge. (Contributed by AV, 30-Dec-2020)

Ref Expression
Hypotheses upgredg.v ⊢ V = Vtx ⁡ G
upgredg.e ⊢ E = Edg ⁡ G
Assertion upgredgpr ⊢ G ∈ UPGraph ∧ C ∈ E ∧ A B ⊆ C ∧ A ∈ U ∧ B ∈ W ∧ A ≠ B → A B = C

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢ V = Vtx ⁡ G
2 upgredg.e ⊢ E = Edg ⁡ G
3 1 2 upgredg ⊢ G ∈ UPGraph ∧ C ∈ E → ∃ a ∈ V ∃ b ∈ V C = a b
4 3 3adant3 ⊢ G ∈ UPGraph ∧ C ∈ E ∧ A B ⊆ C → ∃ a ∈ V ∃ b ∈ V C = a b
5 ssprsseq ⊢ A ∈ U ∧ B ∈ W ∧ A ≠ B → A B ⊆ a b ↔ A B = a b
6 5 biimpd ⊢ A ∈ U ∧ B ∈ W ∧ A ≠ B → A B ⊆ a b → A B = a b
7 sseq2 ⊢ C = a b → A B ⊆ C ↔ A B ⊆ a b
8 eqeq2 ⊢ C = a b → A B = C ↔ A B = a b
9 7 8 imbi12d ⊢ C = a b → A B ⊆ C → A B = C ↔ A B ⊆ a b → A B = a b
10 6 9 imbitrrid ⊢ C = a b → A ∈ U ∧ B ∈ W ∧ A ≠ B → A B ⊆ C → A B = C
11 10 com23 ⊢ C = a b → A B ⊆ C → A ∈ U ∧ B ∈ W ∧ A ≠ B → A B = C
12 11 a1i ⊢ a ∈ V ∧ b ∈ V → C = a b → A B ⊆ C → A ∈ U ∧ B ∈ W ∧ A ≠ B → A B = C
13 12 rexlimivv ⊢ ∃ a ∈ V ∃ b ∈ V C = a b → A B ⊆ C → A ∈ U ∧ B ∈ W ∧ A ≠ B → A B = C
14 13 com12 ⊢ A B ⊆ C → ∃ a ∈ V ∃ b ∈ V C = a b → A ∈ U ∧ B ∈ W ∧ A ≠ B → A B = C
15 14 3ad2ant3 ⊢ G ∈ UPGraph ∧ C ∈ E ∧ A B ⊆ C → ∃ a ∈ V ∃ b ∈ V C = a b → A ∈ U ∧ B ∈ W ∧ A ≠ B → A B = C
16 4 15 mpd ⊢ G ∈ UPGraph ∧ C ∈ E ∧ A B ⊆ C → A ∈ U ∧ B ∈ W ∧ A ≠ B → A B = C
17 16 imp ⊢ G ∈ UPGraph ∧ C ∈ E ∧ A B ⊆ C ∧ A ∈ U ∧ B ∈ W ∧ A ≠ B → A B = C