Metamath Proof Explorer


Theorem fusgrfis

Description: A finite simple graph is of finite size, i.e. has a finite number of edges. (Contributed by Alexander van der Vekens, 6-Jan-2018) (Revised by AV, 8-Nov-2020)

Ref Expression
Assertion fusgrfis ( 𝐺 ∈ FinUSGraph → ( Edg ‘ 𝐺 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 isfusgr ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) )
3 usgrop ( 𝐺 ∈ USGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ USGraph )
4 fvex ( iEdg ‘ 𝐺 ) ∈ V
5 mptresid ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) = ( 𝑞 ∈ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ↦ 𝑞 )
6 fvex ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∈ V
7 6 mptrabex ( 𝑞 ∈ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ↦ 𝑞 ) ∈ V
8 5 7 eqeltri ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) ∈ V
9 eleq1 ( 𝑒 = ( iEdg ‘ 𝐺 ) → ( 𝑒 ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) )
10 9 adantl ( ( 𝑣 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( 𝑒 ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) )
11 eleq1 ( 𝑒 = 𝑓 → ( 𝑒 ∈ Fin ↔ 𝑓 ∈ Fin ) )
12 11 adantl ( ( 𝑣 = 𝑤𝑒 = 𝑓 ) → ( 𝑒 ∈ Fin ↔ 𝑓 ∈ Fin ) )
13 vex 𝑣 ∈ V
14 vex 𝑒 ∈ V
15 13 14 opvtxfvi ( Vtx ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = 𝑣
16 15 eqcomi 𝑣 = ( Vtx ‘ ⟨ 𝑣 , 𝑒 ⟩ )
17 eqid ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) = ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ )
18 eqid { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } = { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 }
19 eqid ⟨ ( 𝑣 ∖ { 𝑛 } ) , ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) ⟩ = ⟨ ( 𝑣 ∖ { 𝑛 } ) , ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) ⟩
20 16 17 18 19 usgrres1 ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ 𝑛𝑣 ) → ⟨ ( 𝑣 ∖ { 𝑛 } ) , ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) ⟩ ∈ USGraph )
21 eleq1 ( 𝑓 = ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) → ( 𝑓 ∈ Fin ↔ ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) ∈ Fin ) )
22 21 adantl ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) ) → ( 𝑓 ∈ Fin ↔ ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) ∈ Fin ) )
23 13 14 pm3.2i ( 𝑣 ∈ V ∧ 𝑒 ∈ V )
24 fusgrfisbase ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝑒 ∈ Fin )
25 23 24 mp3an1 ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝑒 ∈ Fin )
26 simpl ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) ) → ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) )
27 simprr1 ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) ) → ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph )
28 eleq1 ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( ( ♯ ‘ 𝑣 ) ∈ ℕ0 ↔ ( 𝑦 + 1 ) ∈ ℕ0 ) )
29 hashclb ( 𝑣 ∈ V → ( 𝑣 ∈ Fin ↔ ( ♯ ‘ 𝑣 ) ∈ ℕ0 ) )
30 29 biimprd ( 𝑣 ∈ V → ( ( ♯ ‘ 𝑣 ) ∈ ℕ0𝑣 ∈ Fin ) )
31 30 adantr ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → ( ( ♯ ‘ 𝑣 ) ∈ ℕ0𝑣 ∈ Fin ) )
32 31 com12 ( ( ♯ ‘ 𝑣 ) ∈ ℕ0 → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → 𝑣 ∈ Fin ) )
33 28 32 syl6bir ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( ( 𝑦 + 1 ) ∈ ℕ0 → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → 𝑣 ∈ Fin ) ) )
34 33 3ad2ant2 ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) → ( ( 𝑦 + 1 ) ∈ ℕ0 → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → 𝑣 ∈ Fin ) ) )
35 34 impcom ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → 𝑣 ∈ Fin ) )
36 35 impcom ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) ) → 𝑣 ∈ Fin )
37 opfusgr ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → ( ⟨ 𝑣 , 𝑒 ⟩ ∈ FinUSGraph ↔ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ 𝑣 ∈ Fin ) ) )
38 37 adantr ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) ) → ( ⟨ 𝑣 , 𝑒 ⟩ ∈ FinUSGraph ↔ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ 𝑣 ∈ Fin ) ) )
39 27 36 38 mpbir2and ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) ) → ⟨ 𝑣 , 𝑒 ⟩ ∈ FinUSGraph )
40 simprr3 ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) ) → 𝑛𝑣 )
41 26 39 40 3jca ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) ) → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ⟨ 𝑣 , 𝑒 ⟩ ∈ FinUSGraph ∧ 𝑛𝑣 ) )
42 23 41 mpan ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ⟨ 𝑣 , 𝑒 ⟩ ∈ FinUSGraph ∧ 𝑛𝑣 ) )
43 fusgrfisstep ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ⟨ 𝑣 , 𝑒 ⟩ ∈ FinUSGraph ∧ 𝑛𝑣 ) → ( ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) ∈ Fin → 𝑒 ∈ Fin ) )
44 42 43 syl ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) → ( ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) ∈ Fin → 𝑒 ∈ Fin ) )
45 44 imp ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛𝑣 ) ) ∧ ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑣 , 𝑒 ⟩ ) ∣ 𝑛𝑝 } ) ∈ Fin ) → 𝑒 ∈ Fin )
46 4 8 10 12 20 22 25 45 opfi1ind ( ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) → ( iEdg ‘ 𝐺 ) ∈ Fin )
47 3 46 sylan ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) → ( iEdg ‘ 𝐺 ) ∈ Fin )
48 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
49 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
50 48 49 usgredgffibi ( 𝐺 ∈ USGraph → ( ( Edg ‘ 𝐺 ) ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) )
51 50 adantr ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) → ( ( Edg ‘ 𝐺 ) ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) )
52 47 51 mpbird ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) → ( Edg ‘ 𝐺 ) ∈ Fin )
53 2 52 sylbi ( 𝐺 ∈ FinUSGraph → ( Edg ‘ 𝐺 ) ∈ Fin )