sizusglecusg

Description: The size of a simple graph with n vertices is at most the size of a complete simple graph with n vertices ( n may be infinite). (Contributed by Alexander van der Vekens, 13-Jan-2018) (Revised by AV, 13-Nov-2020)

	Ref	Expression
Hypotheses	fusgrmaxsize.v	$⊢ V = Vtx (G)$
	fusgrmaxsize.e	$⊢ E = Edg (G)$
	usgrsscusgra.h	$⊢ V = Vtx (H)$
	usgrsscusgra.f	$⊢ F = Edg (H)$
Assertion	sizusglecusg	$⊢ (G \in USGraph \land H \in ComplUSGraph) \to \|E\| \leq \|F\|$

Proof

Step	Hyp	Ref	Expression
1		fusgrmaxsize.v	$⊢ V = Vtx (G)$
2		fusgrmaxsize.e	$⊢ E = Edg (G)$
3		usgrsscusgra.h	$⊢ V = Vtx (H)$
4		usgrsscusgra.f	$⊢ F = Edg (H)$
5	2	fvexi	$⊢ E \in V$
6		resiexg	$⊢ E \in V \to {I ↾}_{E} \in V$
7	5 6	mp1i	$⊢ (G \in USGraph \land H \in ComplUSGraph) \to {I ↾}_{E} \in V$
8	1 2 3 4	sizusglecusglem1	$⊢ (G \in USGraph \land H \in ComplUSGraph) \to ({I ↾}_{E}) : E \underset{1-1}{⟶} F$
9		f1eq1	$⊢ f = {I ↾}_{E} \to (f : E \underset{1-1}{⟶} F \leftrightarrow ({I ↾}_{E}) : E \underset{1-1}{⟶} F)$
10	7 8 9	spcedv	$⊢ (G \in USGraph \land H \in ComplUSGraph) \to \exists f f : E \underset{1-1}{⟶} F$
11	10	adantl	$⊢ ((E \in Fin \land F \in Fin) \land (G \in USGraph \land H \in ComplUSGraph)) \to \exists f f : E \underset{1-1}{⟶} F$
12		hashdom	$⊢ (E \in Fin \land F \in Fin) \to (\|E\| \leq \|F\| \leftrightarrow E ≼ F)$
13	12	adantr	$⊢ ((E \in Fin \land F \in Fin) \land (G \in USGraph \land H \in ComplUSGraph)) \to (\|E\| \leq \|F\| \leftrightarrow E ≼ F)$
14		brdomg	$⊢ F \in Fin \to (E ≼ F \leftrightarrow \exists f f : E \underset{1-1}{⟶} F)$
15	14	adantl	$⊢ (E \in Fin \land F \in Fin) \to (E ≼ F \leftrightarrow \exists f f : E \underset{1-1}{⟶} F)$
16	15	adantr	$⊢ ((E \in Fin \land F \in Fin) \land (G \in USGraph \land H \in ComplUSGraph)) \to (E ≼ F \leftrightarrow \exists f f : E \underset{1-1}{⟶} F)$
17	13 16	bitrd	$⊢ ((E \in Fin \land F \in Fin) \land (G \in USGraph \land H \in ComplUSGraph)) \to (\|E\| \leq \|F\| \leftrightarrow \exists f f : E \underset{1-1}{⟶} F)$
18	11 17	mpbird	$⊢ ((E \in Fin \land F \in Fin) \land (G \in USGraph \land H \in ComplUSGraph)) \to \|E\| \leq \|F\|$
19	18	exp31	$⊢ E \in Fin \to (F \in Fin \to ((G \in USGraph \land H \in ComplUSGraph) \to \|E\| \leq \|F\|))$
20	1 2 3 4	sizusglecusglem2	$⊢ (G \in USGraph \land H \in ComplUSGraph \land F \in Fin) \to E \in Fin$
21	20	pm2.24d	$⊢ (G \in USGraph \land H \in ComplUSGraph \land F \in Fin) \to (\neg E \in Fin \to \|E\| \leq \|F\|)$
22	21	3expia	$⊢ (G \in USGraph \land H \in ComplUSGraph) \to (F \in Fin \to (\neg E \in Fin \to \|E\| \leq \|F\|))$
23	22	com13	$⊢ \neg E \in Fin \to (F \in Fin \to ((G \in USGraph \land H \in ComplUSGraph) \to \|E\| \leq \|F\|))$
24	19 23	pm2.61i	$⊢ F \in Fin \to ((G \in USGraph \land H \in ComplUSGraph) \to \|E\| \leq \|F\|)$
25	4	fvexi	$⊢ F \in V$
26		nfile	$⊢ (E \in V \land F \in V \land \neg F \in Fin) \to \|E\| \leq \|F\|$
27	5 25 26	mp3an12	$⊢ \neg F \in Fin \to \|E\| \leq \|F\|$
28	27	a1d	$⊢ \neg F \in Fin \to ((G \in USGraph \land H \in ComplUSGraph) \to \|E\| \leq \|F\|)$
29	24 28	pm2.61i	$⊢ (G \in USGraph \land H \in ComplUSGraph) \to \|E\| \leq \|F\|$

Metamath Proof Explorer

Theorem sizusglecusg

Proof