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

Theorem isupgr 29116
Description: The property of being an undirected pseudograph. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.)
Hypotheses
Ref Expression
isupgr.v 𝑉 = (Vtx‘𝐺)
isupgr.e 𝐸 = (iEdg‘𝐺)
Assertion
Ref Expression
isupgr (𝐺𝑈 → (𝐺 ∈ UPGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
Distinct variable groups:   𝑥,𝐺   𝑥,𝑉
Allowed substitution hints:   𝑈(𝑥)   𝐸(𝑥)

Proof of Theorem isupgr
Dummy variables 𝑒 𝑔 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-upgr 29114 . . 3 UPGraph = {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}}
21eleq2i 2831 . 2 (𝐺 ∈ UPGraph ↔ 𝐺 ∈ {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}})
3 fveq2 6907 . . . . 5 ( = 𝐺 → (iEdg‘) = (iEdg‘𝐺))
4 isupgr.e . . . . 5 𝐸 = (iEdg‘𝐺)
53, 4eqtr4di 2793 . . . 4 ( = 𝐺 → (iEdg‘) = 𝐸)
63dmeqd 5919 . . . . 5 ( = 𝐺 → dom (iEdg‘) = dom (iEdg‘𝐺))
74eqcomi 2744 . . . . . 6 (iEdg‘𝐺) = 𝐸
87dmeqi 5918 . . . . 5 dom (iEdg‘𝐺) = dom 𝐸
96, 8eqtrdi 2791 . . . 4 ( = 𝐺 → dom (iEdg‘) = dom 𝐸)
10 fveq2 6907 . . . . . . . 8 ( = 𝐺 → (Vtx‘) = (Vtx‘𝐺))
11 isupgr.v . . . . . . . 8 𝑉 = (Vtx‘𝐺)
1210, 11eqtr4di 2793 . . . . . . 7 ( = 𝐺 → (Vtx‘) = 𝑉)
1312pweqd 4622 . . . . . 6 ( = 𝐺 → 𝒫 (Vtx‘) = 𝒫 𝑉)
1413difeq1d 4135 . . . . 5 ( = 𝐺 → (𝒫 (Vtx‘) ∖ {∅}) = (𝒫 𝑉 ∖ {∅}))
1514rabeqdv 3449 . . . 4 ( = 𝐺 → {𝑥 ∈ (𝒫 (Vtx‘) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
165, 9, 15feq123d 6726 . . 3 ( = 𝐺 → ((iEdg‘):dom (iEdg‘)⟶{𝑥 ∈ (𝒫 (Vtx‘) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
17 fvexd 6922 . . . . 5 (𝑔 = → (Vtx‘𝑔) ∈ V)
18 fveq2 6907 . . . . 5 (𝑔 = → (Vtx‘𝑔) = (Vtx‘))
19 fvexd 6922 . . . . . 6 ((𝑔 = 𝑣 = (Vtx‘)) → (iEdg‘𝑔) ∈ V)
20 fveq2 6907 . . . . . . 7 (𝑔 = → (iEdg‘𝑔) = (iEdg‘))
2120adantr 480 . . . . . 6 ((𝑔 = 𝑣 = (Vtx‘)) → (iEdg‘𝑔) = (iEdg‘))
22 simpr 484 . . . . . . 7 (((𝑔 = 𝑣 = (Vtx‘)) ∧ 𝑒 = (iEdg‘)) → 𝑒 = (iEdg‘))
2322dmeqd 5919 . . . . . . 7 (((𝑔 = 𝑣 = (Vtx‘)) ∧ 𝑒 = (iEdg‘)) → dom 𝑒 = dom (iEdg‘))
24 pweq 4619 . . . . . . . . . 10 (𝑣 = (Vtx‘) → 𝒫 𝑣 = 𝒫 (Vtx‘))
2524ad2antlr 727 . . . . . . . . 9 (((𝑔 = 𝑣 = (Vtx‘)) ∧ 𝑒 = (iEdg‘)) → 𝒫 𝑣 = 𝒫 (Vtx‘))
2625difeq1d 4135 . . . . . . . 8 (((𝑔 = 𝑣 = (Vtx‘)) ∧ 𝑒 = (iEdg‘)) → (𝒫 𝑣 ∖ {∅}) = (𝒫 (Vtx‘) ∖ {∅}))
2726rabeqdv 3449 . . . . . . 7 (((𝑔 = 𝑣 = (Vtx‘)) ∧ 𝑒 = (iEdg‘)) → {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} = {𝑥 ∈ (𝒫 (Vtx‘) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
2822, 23, 27feq123d 6726 . . . . . 6 (((𝑔 = 𝑣 = (Vtx‘)) ∧ 𝑒 = (iEdg‘)) → (𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ↔ (iEdg‘):dom (iEdg‘)⟶{𝑥 ∈ (𝒫 (Vtx‘) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
2919, 21, 28sbcied2 3839 . . . . 5 ((𝑔 = 𝑣 = (Vtx‘)) → ([(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ↔ (iEdg‘):dom (iEdg‘)⟶{𝑥 ∈ (𝒫 (Vtx‘) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
3017, 18, 29sbcied2 3839 . . . 4 (𝑔 = → ([(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ↔ (iEdg‘):dom (iEdg‘)⟶{𝑥 ∈ (𝒫 (Vtx‘) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
3130cbvabv 2810 . . 3 {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}} = { ∣ (iEdg‘):dom (iEdg‘)⟶{𝑥 ∈ (𝒫 (Vtx‘) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}}
3216, 31elab2g 3683 . 2 (𝐺𝑈 → (𝐺 ∈ {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}} ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
332, 32bitrid 283 1 (𝐺𝑈 → (𝐺 ∈ UPGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  {cab 2712  {crab 3433  Vcvv 3478  [wsbc 3791  cdif 3960  c0 4339  𝒫 cpw 4605  {csn 4631   class class class wbr 5148  dom cdm 5689  wf 6559  cfv 6563  cle 11294  2c2 12319  chash 14366  Vtxcvtx 29028  iEdgciedg 29029  UPGraphcupgr 29112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-upgr 29114
This theorem is referenced by:  wrdupgr  29117  upgrf  29118  upgrop  29126  umgrupgr  29135  upgr1e  29145  upgrun  29150  uspgrupgr  29210  subupgr  29319  upgrres  29338  upgrres1  29345
  Copyright terms: Public domain W3C validator