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 )