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 𝑉 = ( Vtx ‘ 𝐺 )
upgredg.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion upgrpredgv ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀𝑈𝑁𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( 𝑀𝑉𝑁𝑉 ) )

Proof

Step Hyp Ref Expression
1 upgredg.v 𝑉 = ( Vtx ‘ 𝐺 )
2 upgredg.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 upgredg ( ( 𝐺 ∈ UPGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ∃ 𝑚𝑉𝑛𝑉 { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } )
4 3 3adant2 ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀𝑈𝑁𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ∃ 𝑚𝑉𝑛𝑉 { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } )
5 preq12bg ( ( ( 𝑀𝑈𝑁𝑊 ) ∧ ( 𝑚𝑉𝑛𝑉 ) ) → ( { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } ↔ ( ( 𝑀 = 𝑚𝑁 = 𝑛 ) ∨ ( 𝑀 = 𝑛𝑁 = 𝑚 ) ) ) )
6 5 3ad2antl2 ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀𝑈𝑁𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) ∧ ( 𝑚𝑉𝑛𝑉 ) ) → ( { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } ↔ ( ( 𝑀 = 𝑚𝑁 = 𝑛 ) ∨ ( 𝑀 = 𝑛𝑁 = 𝑚 ) ) ) )
7 eleq1 ( 𝑚 = 𝑀 → ( 𝑚𝑉𝑀𝑉 ) )
8 7 eqcoms ( 𝑀 = 𝑚 → ( 𝑚𝑉𝑀𝑉 ) )
9 8 biimpd ( 𝑀 = 𝑚 → ( 𝑚𝑉𝑀𝑉 ) )
10 eleq1 ( 𝑛 = 𝑁 → ( 𝑛𝑉𝑁𝑉 ) )
11 10 eqcoms ( 𝑁 = 𝑛 → ( 𝑛𝑉𝑁𝑉 ) )
12 11 biimpd ( 𝑁 = 𝑛 → ( 𝑛𝑉𝑁𝑉 ) )
13 9 12 im2anan9 ( ( 𝑀 = 𝑚𝑁 = 𝑛 ) → ( ( 𝑚𝑉𝑛𝑉 ) → ( 𝑀𝑉𝑁𝑉 ) ) )
14 13 com12 ( ( 𝑚𝑉𝑛𝑉 ) → ( ( 𝑀 = 𝑚𝑁 = 𝑛 ) → ( 𝑀𝑉𝑁𝑉 ) ) )
15 eleq1 ( 𝑛 = 𝑀 → ( 𝑛𝑉𝑀𝑉 ) )
16 15 eqcoms ( 𝑀 = 𝑛 → ( 𝑛𝑉𝑀𝑉 ) )
17 16 biimpd ( 𝑀 = 𝑛 → ( 𝑛𝑉𝑀𝑉 ) )
18 eleq1 ( 𝑚 = 𝑁 → ( 𝑚𝑉𝑁𝑉 ) )
19 18 eqcoms ( 𝑁 = 𝑚 → ( 𝑚𝑉𝑁𝑉 ) )
20 19 biimpd ( 𝑁 = 𝑚 → ( 𝑚𝑉𝑁𝑉 ) )
21 17 20 im2anan9 ( ( 𝑀 = 𝑛𝑁 = 𝑚 ) → ( ( 𝑛𝑉𝑚𝑉 ) → ( 𝑀𝑉𝑁𝑉 ) ) )
22 21 com12 ( ( 𝑛𝑉𝑚𝑉 ) → ( ( 𝑀 = 𝑛𝑁 = 𝑚 ) → ( 𝑀𝑉𝑁𝑉 ) ) )
23 22 ancoms ( ( 𝑚𝑉𝑛𝑉 ) → ( ( 𝑀 = 𝑛𝑁 = 𝑚 ) → ( 𝑀𝑉𝑁𝑉 ) ) )
24 14 23 jaod ( ( 𝑚𝑉𝑛𝑉 ) → ( ( ( 𝑀 = 𝑚𝑁 = 𝑛 ) ∨ ( 𝑀 = 𝑛𝑁 = 𝑚 ) ) → ( 𝑀𝑉𝑁𝑉 ) ) )
25 24 adantl ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀𝑈𝑁𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) ∧ ( 𝑚𝑉𝑛𝑉 ) ) → ( ( ( 𝑀 = 𝑚𝑁 = 𝑛 ) ∨ ( 𝑀 = 𝑛𝑁 = 𝑚 ) ) → ( 𝑀𝑉𝑁𝑉 ) ) )
26 6 25 sylbid ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀𝑈𝑁𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) ∧ ( 𝑚𝑉𝑛𝑉 ) ) → ( { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } → ( 𝑀𝑉𝑁𝑉 ) ) )
27 26 rexlimdvva ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀𝑈𝑁𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( ∃ 𝑚𝑉𝑛𝑉 { 𝑀 , 𝑁 } = { 𝑚 , 𝑛 } → ( 𝑀𝑉𝑁𝑉 ) ) )
28 4 27 mpd ( ( 𝐺 ∈ UPGraph ∧ ( 𝑀𝑈𝑁𝑊 ) ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( 𝑀𝑉𝑁𝑉 ) )