Theorem isfusgr 29892

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 6883	. . . 4 ⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺))
2		isfusgr.v	. . . 4 ⊢ 𝑉 = (Vtx‘𝐺)
3	1, 2	eqtr4di 2814	. . 3 ⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉)
4	3	eleq1d 2846	. 2 ⊢ (𝑔 = 𝐺 → ((Vtx‘𝑔) ∈ Fin ↔ 𝑉 ∈ Fin))
5		df-fusgr 29891	. 2 ⊢ FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin}
6	4, 5	elrab2 3649	1 ⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  Fincfn 8966  Vtxcvtx 29567  USGraphcusgr 29723  FinUSGraphcfusgr 29890

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-fusgr 29891

This theorem is used by:  fusgrvtxfi  29893  isfusgrf1  29894  isfusgrcl  29895  fusgrusgr  29896  opfusgr  29897  fusgredgfi  29899  fusgrfis  29904  cusgrsizeindslem  30025  cusgrsizeinds  30026  sizusglecusglem2  30036  fusgrmaxsize  30038  finrusgrfusgr  30139  rusgrnumwwlks  30559  rusgrnumwwlk  30560  frrusgrord0lem  30933  frrusgrord0  30934  clwlknon2num  30962  numclwlk1lem1  30963  numclwlk1lem2  30964  friendshipgt3  30992