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 𝑉 = ( Vtx ‘ 𝐺 )
upgredg.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion upgredgpr ( ( ( 𝐺 ∈ UPGraph ∧ 𝐶𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) ∧ ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) ) → { 𝐴 , 𝐵 } = 𝐶 )

Proof

Step Hyp Ref Expression
1 upgredg.v 𝑉 = ( Vtx ‘ 𝐺 )
2 upgredg.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 upgredg ( ( 𝐺 ∈ UPGraph ∧ 𝐶𝐸 ) → ∃ 𝑎𝑉𝑏𝑉 𝐶 = { 𝑎 , 𝑏 } )
4 3 3adant3 ( ( 𝐺 ∈ UPGraph ∧ 𝐶𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ∃ 𝑎𝑉𝑏𝑉 𝐶 = { 𝑎 , 𝑏 } )
5 ssprsseq ( ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } ↔ { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
6 5 biimpd ( ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
7 sseq2 ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 ↔ { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } ) )
8 eqeq2 ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } = 𝐶 ↔ { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
9 7 8 imbi12d ( 𝐶 = { 𝑎 , 𝑏 } → ( ( { 𝐴 , 𝐵 } ⊆ 𝐶 → { 𝐴 , 𝐵 } = 𝐶 ) ↔ ( { 𝐴 , 𝐵 } ⊆ { 𝑎 , 𝑏 } → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
10 6 9 syl5ibr ( 𝐶 = { 𝑎 , 𝑏 } → ( ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → { 𝐴 , 𝐵 } = 𝐶 ) ) )
11 10 com23 ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) )
12 11 a1i ( ( 𝑎𝑉𝑏𝑉 ) → ( 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) ) )
13 12 rexlimivv ( ∃ 𝑎𝑉𝑏𝑉 𝐶 = { 𝑎 , 𝑏 } → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) )
14 13 com12 ( { 𝐴 , 𝐵 } ⊆ 𝐶 → ( ∃ 𝑎𝑉𝑏𝑉 𝐶 = { 𝑎 , 𝑏 } → ( ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) )
15 14 3ad2ant3 ( ( 𝐺 ∈ UPGraph ∧ 𝐶𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ( ∃ 𝑎𝑉𝑏𝑉 𝐶 = { 𝑎 , 𝑏 } → ( ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) ) )
16 4 15 mpd ( ( 𝐺 ∈ UPGraph ∧ 𝐶𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ( ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 ) )
17 16 imp ( ( ( 𝐺 ∈ UPGraph ∧ 𝐶𝐸 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) ∧ ( 𝐴𝑈𝐵𝑊𝐴𝐵 ) ) → { 𝐴 , 𝐵 } = 𝐶 )