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∧AB⊆C∧A∈U∧B∈W∧A≠B→AB=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∈VC=ab
4 3 3adant3 ⊢G∈UPGraph∧C∈E∧AB⊆C→∃a∈V∃b∈VC=ab
5 ssprsseq ⊢A∈U∧B∈W∧A≠B→AB⊆ab↔AB=ab
6 5 biimpd ⊢A∈U∧B∈W∧A≠B→AB⊆ab→AB=ab
7 sseq2 ⊢C=ab→AB⊆C↔AB⊆ab
8 eqeq2 ⊢C=ab→AB=C↔AB=ab
9 7 8 imbi12d ⊢C=ab→AB⊆C→AB=C↔AB⊆ab→AB=ab
10 6 9 imbitrrid ⊢C=ab→A∈U∧B∈W∧A≠B→AB⊆C→AB=C
11 10 com23 ⊢C=ab→AB⊆C→A∈U∧B∈W∧A≠B→AB=C
12 11 a1i ⊢a∈V∧b∈V→C=ab→AB⊆C→A∈U∧B∈W∧A≠B→AB=C
13 12 rexlimivv ⊢∃a∈V∃b∈VC=ab→AB⊆C→A∈U∧B∈W∧A≠B→AB=C
14 13 com12 ⊢AB⊆C→∃a∈V∃b∈VC=ab→A∈U∧B∈W∧A≠B→AB=C
15 14 3ad2ant3 ⊢G∈UPGraph∧C∈E∧AB⊆C→∃a∈V∃b∈VC=ab→A∈U∧B∈W∧A≠B→AB=C
16 4 15 mpd ⊢G∈UPGraph∧C∈E∧AB⊆C→A∈U∧B∈W∧A≠B→AB=C
17 16 imp ⊢G∈UPGraph∧C∈E∧AB⊆C∧A∈U∧B∈W∧A≠B→AB=C