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 e. UPGraph /\ C e. E /\ { A , B } C_ C ) /\ ( A e. U /\ B e. 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 e. UPGraph /\ C e. E ) -> E. a e. V E. b e. V C = { a , b } )
4 3 3adant3 
 |-  ( ( G e. UPGraph /\ C e. E /\ { A , B } C_ C ) -> E. a e. V E. b e. V C = { a , b } )
5 ssprsseq 
 |-  ( ( A e. U /\ B e. W /\ A =/= B ) -> ( { A , B } C_ { a , b } <-> { A , B } = { a , b } ) )
6 5 biimpd 
 |-  ( ( A e. U /\ B e. W /\ A =/= B ) -> ( { A , B } C_ { a , b } -> { A , B } = { a , b } ) )
7 sseq2 
 |-  ( C = { a , b } -> ( { A , B } C_ C <-> { A , B } C_ { a , b } ) )
8 eqeq2 
 |-  ( C = { a , b } -> ( { A , B } = C <-> { A , B } = { a , b } ) )
9 7 8 imbi12d 
 |-  ( C = { a , b } -> ( ( { A , B } C_ C -> { A , B } = C ) <-> ( { A , B } C_ { a , b } -> { A , B } = { a , b } ) ) )
10 6 9 imbitrrid 
 |-  ( C = { a , b } -> ( ( A e. U /\ B e. W /\ A =/= B ) -> ( { A , B } C_ C -> { A , B } = C ) ) )
11 10 com23 
 |-  ( C = { a , b } -> ( { A , B } C_ C -> ( ( A e. U /\ B e. W /\ A =/= B ) -> { A , B } = C ) ) )
12 11 a1i 
 |-  ( ( a e. V /\ b e. V ) -> ( C = { a , b } -> ( { A , B } C_ C -> ( ( A e. U /\ B e. W /\ A =/= B ) -> { A , B } = C ) ) ) )
13 12 rexlimivv 
 |-  ( E. a e. V E. b e. V C = { a , b } -> ( { A , B } C_ C -> ( ( A e. U /\ B e. W /\ A =/= B ) -> { A , B } = C ) ) )
14 13 com12 
 |-  ( { A , B } C_ C -> ( E. a e. V E. b e. V C = { a , b } -> ( ( A e. U /\ B e. W /\ A =/= B ) -> { A , B } = C ) ) )
15 14 3ad2ant3 
 |-  ( ( G e. UPGraph /\ C e. E /\ { A , B } C_ C ) -> ( E. a e. V E. b e. V C = { a , b } -> ( ( A e. U /\ B e. W /\ A =/= B ) -> { A , B } = C ) ) )
16 4 15 mpd 
 |-  ( ( G e. UPGraph /\ C e. E /\ { A , B } C_ C ) -> ( ( A e. U /\ B e. W /\ A =/= B ) -> { A , B } = C ) )
17 16 imp 
 |-  ( ( ( G e. UPGraph /\ C e. E /\ { A , B } C_ C ) /\ ( A e. U /\ B e. W /\ A =/= B ) ) -> { A , B } = C )