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	$⊢ G \in FinUSGraph \to Edg (G) \in Fin$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2	1	isfusgr	$⊢ G \in FinUSGraph \leftrightarrow (G \in USGraph \land Vtx (G) \in Fin)$
3		usgrop	$⊢ G \in USGraph \to ⟨Vtx (G), iEdg (G)⟩ \in USGraph$
4		fvex	$⊢ iEdg (G) \in V$
5		mptresid	$⊢ {I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}} = (q \in \{p \in Edg (⟨v, e⟩) \| n \notin p\} ⟼ q)$
6		fvex	$⊢ Edg (⟨v, e⟩) \in V$
7	6	mptrabex	$⊢ (q \in \{p \in Edg (⟨v, e⟩) \| n \notin p\} ⟼ q) \in V$
8	5 7	eqeltri	$⊢ {I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}} \in V$
9		eleq1	$⊢ e = iEdg (G) \to (e \in Fin \leftrightarrow iEdg (G) \in Fin)$
10	9	adantl	$⊢ (v = Vtx (G) \land e = iEdg (G)) \to (e \in Fin \leftrightarrow iEdg (G) \in Fin)$
11		eleq1	$⊢ e = f \to (e \in Fin \leftrightarrow f \in Fin)$
12	11	adantl	$⊢ (v = w \land e = f) \to (e \in Fin \leftrightarrow f \in Fin)$
13		vex	$⊢ v \in V$
14		vex	$⊢ e \in V$
15	13 14	opvtxfvi	$⊢ Vtx (⟨v, e⟩) = v$
16	15	eqcomi	$⊢ v = Vtx (⟨v, e⟩)$
17		eqid	$⊢ Edg (⟨v, e⟩) = Edg (⟨v, e⟩)$
18		eqid	$⊢ \{p \in Edg (⟨v, e⟩) \| n \notin p\} = \{p \in Edg (⟨v, e⟩) \| n \notin p\}$
19		eqid	$⊢ ⟨v ∖ \{n\}, {I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}}⟩ = ⟨v ∖ \{n\}, {I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}}⟩$
20	16 17 18 19	usgrres1	$⊢ (⟨v, e⟩ \in USGraph \land n \in v) \to ⟨v ∖ \{n\}, {I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}}⟩ \in USGraph$
21		eleq1	$⊢ f = {I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}} \to (f \in Fin \leftrightarrow {I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}} \in Fin)$
22	21	adantl	$⊢ (w = v ∖ \{n\} \land f = {I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}}) \to (f \in Fin \leftrightarrow {I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}} \in Fin)$
23	13 14	pm3.2i	$⊢ (v \in V \land e \in V)$
24		fusgrfisbase	$⊢ ((v \in V \land e \in V) \land ⟨v, e⟩ \in USGraph \land \|v\| = 0) \to e \in Fin$
25	23 24	mp3an1	$⊢ (⟨v, e⟩ \in USGraph \land \|v\| = 0) \to e \in Fin$
26		simpl	$⊢ ((v \in V \land e \in V) \land (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v))) \to (v \in V \land e \in V)$
27		simprr1	$⊢ ((v \in V \land e \in V) \land (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v))) \to ⟨v, e⟩ \in USGraph$
28		eleq1	$⊢ \|v\| = y + 1 \to (\|v\| \in ℕ_{0} \leftrightarrow y + 1 \in ℕ_{0})$
29		hashclb	$⊢ v \in V \to (v \in Fin \leftrightarrow \|v\| \in ℕ_{0})$
30	29	biimprd	$⊢ v \in V \to (\|v\| \in ℕ_{0} \to v \in Fin)$
31	30	adantr	$⊢ (v \in V \land e \in V) \to (\|v\| \in ℕ_{0} \to v \in Fin)$
32	31	com12	$⊢ \|v\| \in ℕ_{0} \to ((v \in V \land e \in V) \to v \in Fin)$
33	28 32	biimtrrdi	$⊢ \|v\| = y + 1 \to (y + 1 \in ℕ_{0} \to ((v \in V \land e \in V) \to v \in Fin))$
34	33	3ad2ant2	$⊢ (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v) \to (y + 1 \in ℕ_{0} \to ((v \in V \land e \in V) \to v \in Fin))$
35	34	impcom	$⊢ (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v)) \to ((v \in V \land e \in V) \to v \in Fin)$
36	35	impcom	$⊢ ((v \in V \land e \in V) \land (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v))) \to v \in Fin$
37		opfusgr	$⊢ (v \in V \land e \in V) \to (⟨v, e⟩ \in FinUSGraph \leftrightarrow (⟨v, e⟩ \in USGraph \land v \in Fin))$
38	37	adantr	$⊢ ((v \in V \land e \in V) \land (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v))) \to (⟨v, e⟩ \in FinUSGraph \leftrightarrow (⟨v, e⟩ \in USGraph \land v \in Fin))$
39	27 36 38	mpbir2and	$⊢ ((v \in V \land e \in V) \land (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v))) \to ⟨v, e⟩ \in FinUSGraph$
40		simprr3	$⊢ ((v \in V \land e \in V) \land (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v))) \to n \in v$
41	26 39 40	3jca	$⊢ ((v \in V \land e \in V) \land (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v))) \to ((v \in V \land e \in V) \land ⟨v, e⟩ \in FinUSGraph \land n \in v)$
42	23 41	mpan	$⊢ (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v)) \to ((v \in V \land e \in V) \land ⟨v, e⟩ \in FinUSGraph \land n \in v)$
43		fusgrfisstep	$⊢ ((v \in V \land e \in V) \land ⟨v, e⟩ \in FinUSGraph \land n \in v) \to ({I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}} \in Fin \to e \in Fin)$
44	42 43	syl	$⊢ (y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v)) \to ({I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}} \in Fin \to e \in Fin)$
45	44	imp	$⊢ ((y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in USGraph \land \|v\| = y + 1 \land n \in v)) \land {I ↾}_{\{p \in Edg (⟨v, e⟩) \| n \notin p\}} \in Fin) \to e \in Fin$
46	4 8 10 12 20 22 25 45	opfi1ind	$⊢ (⟨Vtx (G), iEdg (G)⟩ \in USGraph \land Vtx (G) \in Fin) \to iEdg (G) \in Fin$
47	3 46	sylan	$⊢ (G \in USGraph \land Vtx (G) \in Fin) \to iEdg (G) \in Fin$
48		eqid	$⊢ iEdg (G) = iEdg (G)$
49		eqid	$⊢ Edg (G) = Edg (G)$
50	48 49	usgredgffibi	$⊢ G \in USGraph \to (Edg (G) \in Fin \leftrightarrow iEdg (G) \in Fin)$
51	50	adantr	$⊢ (G \in USGraph \land Vtx (G) \in Fin) \to (Edg (G) \in Fin \leftrightarrow iEdg (G) \in Fin)$
52	47 51	mpbird	$⊢ (G \in USGraph \land Vtx (G) \in Fin) \to Edg (G) \in Fin$
53	2 52	sylbi	$⊢ G \in FinUSGraph \to Edg (G) \in Fin$

Metamath Proof Explorer

Theorem fusgrfis

Proof