This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrdi ⊢ ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 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 )