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

Theorem isfusgr 29335
Description: The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.)
Hypothesis
Ref Expression
isfusgr.v 𝑉 = (Vtx‘𝐺)
Assertion
Ref Expression
isfusgr (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))

Proof of Theorem isfusgr
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6906 . . . 4 (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺))
2 isfusgr.v . . . 4 𝑉 = (Vtx‘𝐺)
31, 2eqtr4di 2795 . . 3 (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉)
43eleq1d 2826 . 2 (𝑔 = 𝐺 → ((Vtx‘𝑔) ∈ Fin ↔ 𝑉 ∈ Fin))
5 df-fusgr 29334 . 2 FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
64, 5elrab2 3695 1 (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wcel 2108  cfv 6561  Fincfn 8985  Vtxcvtx 29013  USGraphcusgr 29166  FinUSGraphcfusgr 29333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-fusgr 29334
This theorem is referenced by:  fusgrvtxfi  29336  isfusgrf1  29337  isfusgrcl  29338  fusgrusgr  29339  opfusgr  29340  fusgredgfi  29342  fusgrfis  29347  cusgrsizeindslem  29469  cusgrsizeinds  29470  sizusglecusglem2  29480  fusgrmaxsize  29482  finrusgrfusgr  29583  rusgrnumwwlks  29994  rusgrnumwwlk  29995  frrusgrord0lem  30358  frrusgrord0  30359  clwlknon2num  30387  numclwlk1lem1  30388  numclwlk1lem2  30389  friendshipgt3  30417
  Copyright terms: Public domain W3C validator