Metamath Proof Explorer

Theorem upgrpredgv

Description: An edge of a pseudograph always connects two vertices if the edge contains two sets. The two vertices/sets need not necessarily be different (loops are allowed). (Contributed by AV, 18-Nov-2021)

Ref Expression
Hypotheses upgredg.v 
|- V = ( Vtx ` G )
upgredg.e 
|- E = ( Edg ` G )
Assertion upgrpredgv 
|- ( ( G e. UPGraph /\ ( M e. U /\ N e. W ) /\ { M , N } e. E ) -> ( M e. V /\ N e. V ) )

Proof

Step Hyp Ref Expression
1 upgredg.v 
 |-  V = ( Vtx ` G )
2 upgredg.e 
 |-  E = ( Edg ` G )
3 1 2 upgredg 
 |-  ( ( G e. UPGraph /\ { M , N } e. E ) -> E. m e. V E. n e. V { M , N } = { m , n } )
4 3 3adant2 
 |-  ( ( G e. UPGraph /\ ( M e. U /\ N e. W ) /\ { M , N } e. E ) -> E. m e. V E. n e. V { M , N } = { m , n } )
5 preq12bg 
 |-  ( ( ( M e. U /\ N e. W ) /\ ( m e. V /\ n e. V ) ) -> ( { M , N } = { m , n } <-> ( ( M = m /\ N = n ) \/ ( M = n /\ N = m ) ) ) )
6 5 3ad2antl2 
 |-  ( ( ( G e. UPGraph /\ ( M e. U /\ N e. W ) /\ { M , N } e. E ) /\ ( m e. V /\ n e. V ) ) -> ( { M , N } = { m , n } <-> ( ( M = m /\ N = n ) \/ ( M = n /\ N = m ) ) ) )
7 eleq1 
 |-  ( m = M -> ( m e. V <-> M e. V ) )
8 7 eqcoms 
 |-  ( M = m -> ( m e. V <-> M e. V ) )
9 8 biimpd 
 |-  ( M = m -> ( m e. V -> M e. V ) )
10 eleq1 
 |-  ( n = N -> ( n e. V <-> N e. V ) )
11 10 eqcoms 
 |-  ( N = n -> ( n e. V <-> N e. V ) )
12 11 biimpd 
 |-  ( N = n -> ( n e. V -> N e. V ) )
13 9 12 im2anan9 
 |-  ( ( M = m /\ N = n ) -> ( ( m e. V /\ n e. V ) -> ( M e. V /\ N e. V ) ) )
14 13 com12 
 |-  ( ( m e. V /\ n e. V ) -> ( ( M = m /\ N = n ) -> ( M e. V /\ N e. V ) ) )
15 eleq1 
 |-  ( n = M -> ( n e. V <-> M e. V ) )
16 15 eqcoms 
 |-  ( M = n -> ( n e. V <-> M e. V ) )
17 16 biimpd 
 |-  ( M = n -> ( n e. V -> M e. V ) )
18 eleq1 
 |-  ( m = N -> ( m e. V <-> N e. V ) )
19 18 eqcoms 
 |-  ( N = m -> ( m e. V <-> N e. V ) )
20 19 biimpd 
 |-  ( N = m -> ( m e. V -> N e. V ) )
21 17 20 im2anan9 
 |-  ( ( M = n /\ N = m ) -> ( ( n e. V /\ m e. V ) -> ( M e. V /\ N e. V ) ) )
22 21 com12 
 |-  ( ( n e. V /\ m e. V ) -> ( ( M = n /\ N = m ) -> ( M e. V /\ N e. V ) ) )
23 22 ancoms 
 |-  ( ( m e. V /\ n e. V ) -> ( ( M = n /\ N = m ) -> ( M e. V /\ N e. V ) ) )
24 14 23 jaod 
 |-  ( ( m e. V /\ n e. V ) -> ( ( ( M = m /\ N = n ) \/ ( M = n /\ N = m ) ) -> ( M e. V /\ N e. V ) ) )
25 24 adantl 
 |-  ( ( ( G e. UPGraph /\ ( M e. U /\ N e. W ) /\ { M , N } e. E ) /\ ( m e. V /\ n e. V ) ) -> ( ( ( M = m /\ N = n ) \/ ( M = n /\ N = m ) ) -> ( M e. V /\ N e. V ) ) )
26 6 25 sylbid 
 |-  ( ( ( G e. UPGraph /\ ( M e. U /\ N e. W ) /\ { M , N } e. E ) /\ ( m e. V /\ n e. V ) ) -> ( { M , N } = { m , n } -> ( M e. V /\ N e. V ) ) )
27 26 rexlimdvva 
 |-  ( ( G e. UPGraph /\ ( M e. U /\ N e. W ) /\ { M , N } e. E ) -> ( E. m e. V E. n e. V { M , N } = { m , n } -> ( M e. V /\ N e. V ) ) )
28 4 27 mpd 
 |-  ( ( G e. UPGraph /\ ( M e. U /\ N e. W ) /\ { M , N } e. E ) -> ( M e. V /\ N e. V ) )