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∈UPGraph∧M∈U∧N∈W∧MN∈E→M∈V∧N∈V

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢V=Vtx⁡G
2 upgredg.e ⊢E=Edg⁡G
3 1 2 upgredg ⊢G∈UPGraph∧MN∈E→∃m∈V∃n∈VMN=mn
4 3 3adant2 ⊢G∈UPGraph∧M∈U∧N∈W∧MN∈E→∃m∈V∃n∈VMN=mn
5 preq12bg ⊢M∈U∧N∈W∧m∈V∧n∈V→MN=mn↔M=m∧N=n∨M=n∧N=m
6 5 3ad2antl2 ⊢G∈UPGraph∧M∈U∧N∈W∧MN∈E∧m∈V∧n∈V→MN=mn↔M=m∧N=n∨M=n∧N=m
7 eleq1 ⊢m=M→m∈V↔M∈V
8 7 eqcoms ⊢M=m→m∈V↔M∈V
9 8 biimpd ⊢M=m→m∈V→M∈V
10 eleq1 ⊢n=N→n∈V↔N∈V
11 10 eqcoms ⊢N=n→n∈V↔N∈V
12 11 biimpd ⊢N=n→n∈V→N∈V
13 9 12 im2anan9 ⊢M=m∧N=n→m∈V∧n∈V→M∈V∧N∈V
14 13 com12 ⊢m∈V∧n∈V→M=m∧N=n→M∈V∧N∈V
15 eleq1 ⊢n=M→n∈V↔M∈V
16 15 eqcoms ⊢M=n→n∈V↔M∈V
17 16 biimpd ⊢M=n→n∈V→M∈V
18 eleq1 ⊢m=N→m∈V↔N∈V
19 18 eqcoms ⊢N=m→m∈V↔N∈V
20 19 biimpd ⊢N=m→m∈V→N∈V
21 17 20 im2anan9 ⊢M=n∧N=m→n∈V∧m∈V→M∈V∧N∈V
22 21 com12 ⊢n∈V∧m∈V→M=n∧N=m→M∈V∧N∈V
23 22 ancoms ⊢m∈V∧n∈V→M=n∧N=m→M∈V∧N∈V
24 14 23 jaod ⊢m∈V∧n∈V→M=m∧N=n∨M=n∧N=m→M∈V∧N∈V
25 24 adantl ⊢G∈UPGraph∧M∈U∧N∈W∧MN∈E∧m∈V∧n∈V→M=m∧N=n∨M=n∧N=m→M∈V∧N∈V
26 6 25 sylbid ⊢G∈UPGraph∧M∈U∧N∈W∧MN∈E∧m∈V∧n∈V→MN=mn→M∈V∧N∈V
27 26 rexlimdvva ⊢G∈UPGraph∧M∈U∧N∈W∧MN∈E→∃m∈V∃n∈VMN=mn→M∈V∧N∈V
28 4 27 mpd ⊢G∈UPGraph∧M∈U∧N∈W∧MN∈E→M∈V∧N∈V