Theorem isfusgr 29697

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.

Step	Hyp	Ref	Expression
1		fveq2 6885	. . . 4 ⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺))
2		isfusgr.v	. . . 4 ⊢ 𝑉 = (Vtx‘𝐺)
3	1, 2	eqtr4di 2818	. . 3 ⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉)
4	3	eleq1d 2850	. 2 ⊢ (𝑔 = 𝐺 → ((Vtx‘𝑔) ∈ Fin ↔ 𝑉 ∈ Fin))
5		df-fusgr 29696	. 2 ⊢ FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
6	4, 5	elrab2 3656	1 ⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ‘cfv 6540  Fincfn 8945  Vtxcvtx 29375  USGraphcusgr 29528  FinUSGraphcfusgr 29695

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-fusgr 29696

This theorem is used by:  fusgrvtxfi  29698  isfusgrf1  29699  isfusgrcl  29700  fusgrusgr  29701  opfusgr  29702  fusgredgfi  29704  fusgrfis  29709  cusgrsizeindslem  29830  cusgrsizeinds  29831  sizusglecusglem2  29841  fusgrmaxsize  29843  finrusgrfusgr  29944  rusgrnumwwlks  30355  rusgrnumwwlk  30356  frrusgrord0lem  30719  frrusgrord0  30720  clwlknon2num  30748  numclwlk1lem1  30749  numclwlk1lem2  30750  friendshipgt3  30778