MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  umgrupgr Structured version   Visualization version   GIF version

Theorem umgrupgr 28118
Description: An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.)
Assertion
Ref Expression
umgrupgr (𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph)

Proof of Theorem umgrupgr
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqid 2732 . . . . 5 (Vtx‘𝐺) = (Vtx‘𝐺)
2 eqid 2732 . . . . 5 (iEdg‘𝐺) = (iEdg‘𝐺)
31, 2isumgr 28110 . . . 4 (𝐺 ∈ UMGraph → (𝐺 ∈ UMGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2}))
4 id 22 . . . . 5 ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2} → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2})
5 2re 12237 . . . . . . . . . . 11 2 ∈ ℝ
65leidi 11699 . . . . . . . . . 10 2 ≤ 2
76a1i 11 . . . . . . . . 9 ((♯‘𝑥) = 2 → 2 ≤ 2)
8 breq1 5114 . . . . . . . . 9 ((♯‘𝑥) = 2 → ((♯‘𝑥) ≤ 2 ↔ 2 ≤ 2))
97, 8mpbird 257 . . . . . . . 8 ((♯‘𝑥) = 2 → (♯‘𝑥) ≤ 2)
109a1i 11 . . . . . . 7 (𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) → ((♯‘𝑥) = 2 → (♯‘𝑥) ≤ 2))
1110ss2rabi 4040 . . . . . 6 {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2} ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}
1211a1i 11 . . . . 5 ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2} → {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2} ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
134, 12fssd 6692 . . . 4 ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2} → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
143, 13syl6bi 253 . . 3 (𝐺 ∈ UMGraph → (𝐺 ∈ UMGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
1514pm2.43i 52 . 2 (𝐺 ∈ UMGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
161, 2isupgr 28099 . 2 (𝐺 ∈ UMGraph → (𝐺 ∈ UPGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
1715, 16mpbird 257 1 (𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  {crab 3406  cdif 3911  wss 3914  c0 4288  𝒫 cpw 4566  {csn 4592   class class class wbr 5111  dom cdm 5639  wf 6498  cfv 6502  cle 11200  2c2 12218  chash 14241  Vtxcvtx 28011  iEdgciedg 28012  UPGraphcupgr 28095  UMGraphcumgr 28096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2703  ax-sep 5262  ax-nul 5269  ax-pow 5326  ax-pr 5390  ax-un 7678  ax-resscn 11118  ax-1cn 11119  ax-icn 11120  ax-addcl 11121  ax-addrcl 11122  ax-mulcl 11123  ax-mulrcl 11124  ax-i2m1 11129  ax-1ne0 11130  ax-rrecex 11133  ax-cnre 11134  ax-pre-lttri 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4289  df-if 4493  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4872  df-br 5112  df-opab 5174  df-mpt 5195  df-id 5537  df-xp 5645  df-rel 5646  df-cnv 5647  df-co 5648  df-dm 5649  df-rn 5650  df-res 5651  df-ima 5652  df-iota 6454  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7366  df-er 8656  df-en 8892  df-dom 8893  df-sdom 8894  df-pnf 11201  df-mnf 11202  df-xr 11203  df-ltxr 11204  df-le 11205  df-2 12226  df-upgr 28097  df-umgr 28098
This theorem is referenced by:  umgruhgr  28119  upgr0e  28126  umgrislfupgr  28138  nbumgrvtx  28358  umgrwlknloop  28661  umgrwwlks2on  28966  umgr3v3e3cycl  29192  konigsberg  29265
  Copyright terms: Public domain W3C validator