sizeusglecusg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > sizeusglecusg		Structured version Visualization version GIF version

Theorem sizeusglecusg 26014

Description: The size of an undirected simple graph with 𝑛 vertices is at most the size of a complete simple graph with 𝑛 vertices (𝑛 may be infinite). (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Proof shortened by AV, 4-May-2021.)

**Assertion**
Ref	Expression
sizeusglecusg	⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (#‘𝐸) ≤ (#‘𝐹))

Proof of Theorem sizeusglecusg Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		usgrav 25867	. . . . . . . . 9 ⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))
2	1	simprd 478	. . . . . . . 8 ⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V)
3		rnexg 6990	. . . . . . . 8 ⊢ (𝐸 ∈ V → ran 𝐸 ∈ V)
4		resiexg 6994	. . . . . . . 8 ⊢ (ran 𝐸 ∈ V → ( I ↾ ran 𝐸) ∈ V)
5	2, 3, 4	3syl 18	. . . . . . 7 ⊢ (𝑉 USGrph 𝐸 → ( I ↾ ran 𝐸) ∈ V)
6	5	adantr 480	. . . . . 6 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → ( I ↾ ran 𝐸) ∈ V)
7		sizeusglecusglem1 26012	. . . . . 6 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → ( I ↾ ran 𝐸):ran 𝐸–1-1→ran 𝐹)
8		f1eq1 6009	. . . . . 6 ⊢ (𝑓 = ( I ↾ ran 𝐸) → (𝑓:ran 𝐸–1-1→ran 𝐹 ↔ ( I ↾ ran 𝐸):ran 𝐸–1-1→ran 𝐹))
9	6, 7, 8	elabd 3321	. . . . 5 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → ∃𝑓 𝑓:ran 𝐸–1-1→ran 𝐹)
10	9	adantl 481	. . . 4 ⊢ (((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹)) → ∃𝑓 𝑓:ran 𝐸–1-1→ran 𝐹)
11		dmexg 6989	. . . . . . . 8 ⊢ (𝐸 ∈ Fin → dom 𝐸 ∈ V)
12	11	adantr 480	. . . . . . 7 ⊢ ((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) → dom 𝐸 ∈ V)
13		usgraf1 25889	. . . . . . . 8 ⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→ran 𝐸)
14	13	adantr 480	. . . . . . 7 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → 𝐸:dom 𝐸–1-1→ran 𝐸)
15		hashf1rn 13004	. . . . . . 7 ⊢ ((dom 𝐸 ∈ V ∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → (#‘𝐸) = (#‘ran 𝐸))
16	12, 14, 15	syl2an 493	. . . . . 6 ⊢ (((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹)) → (#‘𝐸) = (#‘ran 𝐸))
17		dmexg 6989	. . . . . . . 8 ⊢ (𝐹 ∈ Fin → dom 𝐹 ∈ V)
18	17	adantl 481	. . . . . . 7 ⊢ ((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) → dom 𝐹 ∈ V)
19		cusisusgra 25987	. . . . . . . . 9 ⊢ (𝑉 ComplUSGrph 𝐹 → 𝑉 USGrph 𝐹)
20		usgraf1 25889	. . . . . . . . 9 ⊢ (𝑉 USGrph 𝐹 → 𝐹:dom 𝐹–1-1→ran 𝐹)
21	19, 20	syl 17	. . . . . . . 8 ⊢ (𝑉 ComplUSGrph 𝐹 → 𝐹:dom 𝐹–1-1→ran 𝐹)
22	21	adantl 481	. . . . . . 7 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → 𝐹:dom 𝐹–1-1→ran 𝐹)
23		hashf1rn 13004	. . . . . . 7 ⊢ ((dom 𝐹 ∈ V ∧ 𝐹:dom 𝐹–1-1→ran 𝐹) → (#‘𝐹) = (#‘ran 𝐹))
24	18, 22, 23	syl2an 493	. . . . . 6 ⊢ (((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹)) → (#‘𝐹) = (#‘ran 𝐹))
25	16, 24	breq12d 4596	. . . . 5 ⊢ (((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹)) → ((#‘𝐸) ≤ (#‘𝐹) ↔ (#‘ran 𝐸) ≤ (#‘ran 𝐹)))
26		rnfi 8132	. . . . . . . 8 ⊢ (𝐸 ∈ Fin → ran 𝐸 ∈ Fin)
27		rnexg 6990	. . . . . . . 8 ⊢ (𝐹 ∈ Fin → ran 𝐹 ∈ V)
28	26, 27	anim12i 588	. . . . . . 7 ⊢ ((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) → (ran 𝐸 ∈ Fin ∧ ran 𝐹 ∈ V))
29	28	adantr 480	. . . . . 6 ⊢ (((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹)) → (ran 𝐸 ∈ Fin ∧ ran 𝐹 ∈ V))
30		hashdom 13029	. . . . . 6 ⊢ ((ran 𝐸 ∈ Fin ∧ ran 𝐹 ∈ V) → ((#‘ran 𝐸) ≤ (#‘ran 𝐹) ↔ ran 𝐸 ≼ ran 𝐹))
31	29, 30	syl 17	. . . . 5 ⊢ (((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹)) → ((#‘ran 𝐸) ≤ (#‘ran 𝐹) ↔ ran 𝐸 ≼ ran 𝐹))
32	27	adantl 481	. . . . . . 7 ⊢ ((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) → ran 𝐹 ∈ V)
33		brdomg 7851	. . . . . . 7 ⊢ (ran 𝐹 ∈ V → (ran 𝐸 ≼ ran 𝐹 ↔ ∃𝑓 𝑓:ran 𝐸–1-1→ran 𝐹))
34	32, 33	syl 17	. . . . . 6 ⊢ ((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) → (ran 𝐸 ≼ ran 𝐹 ↔ ∃𝑓 𝑓:ran 𝐸–1-1→ran 𝐹))
35	34	adantr 480	. . . . 5 ⊢ (((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹)) → (ran 𝐸 ≼ ran 𝐹 ↔ ∃𝑓 𝑓:ran 𝐸–1-1→ran 𝐹))
36	25, 31, 35	3bitrd 293	. . . 4 ⊢ (((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹)) → ((#‘𝐸) ≤ (#‘𝐹) ↔ ∃𝑓 𝑓:ran 𝐸–1-1→ran 𝐹))
37	10, 36	mpbird 246	. . 3 ⊢ (((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹)) → (#‘𝐸) ≤ (#‘𝐹))
38	37	ex 449	. 2 ⊢ ((𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (#‘𝐸) ≤ (#‘𝐹)))
39		usgrav 25867	. . . . . 6 ⊢ (𝑉 USGrph 𝐹 → (𝑉 ∈ V ∧ 𝐹 ∈ V))
40		hashinf 12984	. . . . . . . . 9 ⊢ ((𝐹 ∈ V ∧ ¬ 𝐹 ∈ Fin) → (#‘𝐹) = +∞)
41		hashxrcl 13010	. . . . . . . . . . 11 ⊢ (𝐸 ∈ Fin → (#‘𝐸) ∈ ℝ^*)
42		pnfge 11840	. . . . . . . . . . 11 ⊢ ((#‘𝐸) ∈ ℝ^* → (#‘𝐸) ≤ +∞)
43	41, 42	syl 17	. . . . . . . . . 10 ⊢ (𝐸 ∈ Fin → (#‘𝐸) ≤ +∞)
44		breq2 4587	. . . . . . . . . 10 ⊢ ((#‘𝐹) = +∞ → ((#‘𝐸) ≤ (#‘𝐹) ↔ (#‘𝐸) ≤ +∞))
45	43, 44	syl5ibr 235	. . . . . . . . 9 ⊢ ((#‘𝐹) = +∞ → (𝐸 ∈ Fin → (#‘𝐸) ≤ (#‘𝐹)))
46	40, 45	syl 17	. . . . . . . 8 ⊢ ((𝐹 ∈ V ∧ ¬ 𝐹 ∈ Fin) → (𝐸 ∈ Fin → (#‘𝐸) ≤ (#‘𝐹)))
47	46	ex 449	. . . . . . 7 ⊢ (𝐹 ∈ V → (¬ 𝐹 ∈ Fin → (𝐸 ∈ Fin → (#‘𝐸) ≤ (#‘𝐹))))
48	47	adantl 481	. . . . . 6 ⊢ ((𝑉 ∈ V ∧ 𝐹 ∈ V) → (¬ 𝐹 ∈ Fin → (𝐸 ∈ Fin → (#‘𝐸) ≤ (#‘𝐹))))
49	19, 39, 48	3syl 18	. . . . 5 ⊢ (𝑉 ComplUSGrph 𝐹 → (¬ 𝐹 ∈ Fin → (𝐸 ∈ Fin → (#‘𝐸) ≤ (#‘𝐹))))
50	49	adantl 481	. . . 4 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (¬ 𝐹 ∈ Fin → (𝐸 ∈ Fin → (#‘𝐸) ≤ (#‘𝐹))))
51	50	com13 86	. . 3 ⊢ (𝐸 ∈ Fin → (¬ 𝐹 ∈ Fin → ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (#‘𝐸) ≤ (#‘𝐹))))
52	51	imp 444	. 2 ⊢ ((𝐸 ∈ Fin ∧ ¬ 𝐹 ∈ Fin) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (#‘𝐸) ≤ (#‘𝐹)))
53		sizeusglecusglem2 26013	. . . . . 6 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹 ∧ 𝐹 ∈ Fin) → 𝐸 ∈ Fin)
54	53	pm2.24d 146	. . . . 5 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹 ∧ 𝐹 ∈ Fin) → (¬ 𝐸 ∈ Fin → (#‘𝐸) ≤ (#‘𝐹)))
55	54	3expia 1259	. . . 4 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (𝐹 ∈ Fin → (¬ 𝐸 ∈ Fin → (#‘𝐸) ≤ (#‘𝐹))))
56	55	com13 86	. . 3 ⊢ (¬ 𝐸 ∈ Fin → (𝐹 ∈ Fin → ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (#‘𝐸) ≤ (#‘𝐹))))
57	56	imp 444	. 2 ⊢ ((¬ 𝐸 ∈ Fin ∧ 𝐹 ∈ Fin) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (#‘𝐸) ≤ (#‘𝐹)))
58		hashinf 12984	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ V ∧ ¬ 𝐸 ∈ Fin) → (#‘𝐸) = +∞)
59		pnfxr 9971	. . . . . . . . . . . . . . . . . . . 20 ⊢ +∞ ∈ ℝ^*
60		xrleid 11859	. . . . . . . . . . . . . . . . . . . 20 ⊢ (+∞ ∈ ℝ^* → +∞ ≤ +∞)
61	59, 60	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ (((#‘𝐸) = +∞ ∧ (#‘𝐹) = +∞) → +∞ ≤ +∞)
62		breq12 4588	. . . . . . . . . . . . . . . . . . 19 ⊢ (((#‘𝐸) = +∞ ∧ (#‘𝐹) = +∞) → ((#‘𝐸) ≤ (#‘𝐹) ↔ +∞ ≤ +∞))
63	61, 62	mpbird 246	. . . . . . . . . . . . . . . . . 18 ⊢ (((#‘𝐸) = +∞ ∧ (#‘𝐹) = +∞) → (#‘𝐸) ≤ (#‘𝐹))
64	63	expcom 450	. . . . . . . . . . . . . . . . 17 ⊢ ((#‘𝐹) = +∞ → ((#‘𝐸) = +∞ → (#‘𝐸) ≤ (#‘𝐹)))
65	40, 64	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ V ∧ ¬ 𝐹 ∈ Fin) → ((#‘𝐸) = +∞ → (#‘𝐸) ≤ (#‘𝐹)))
66	65	ex 449	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ V → (¬ 𝐹 ∈ Fin → ((#‘𝐸) = +∞ → (#‘𝐸) ≤ (#‘𝐹))))
67	66	com13 86	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐸) = +∞ → (¬ 𝐹 ∈ Fin → (𝐹 ∈ V → (#‘𝐸) ≤ (#‘𝐹))))
68	58, 67	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ V ∧ ¬ 𝐸 ∈ Fin) → (¬ 𝐹 ∈ Fin → (𝐹 ∈ V → (#‘𝐸) ≤ (#‘𝐹))))
69	68	expcom 450	. . . . . . . . . . . 12 ⊢ (¬ 𝐸 ∈ Fin → (𝐸 ∈ V → (¬ 𝐹 ∈ Fin → (𝐹 ∈ V → (#‘𝐸) ≤ (#‘𝐹)))))
70	69	com23 84	. . . . . . . . . . 11 ⊢ (¬ 𝐸 ∈ Fin → (¬ 𝐹 ∈ Fin → (𝐸 ∈ V → (𝐹 ∈ V → (#‘𝐸) ≤ (#‘𝐹)))))
71	70	imp 444	. . . . . . . . . 10 ⊢ ((¬ 𝐸 ∈ Fin ∧ ¬ 𝐹 ∈ Fin) → (𝐸 ∈ V → (𝐹 ∈ V → (#‘𝐸) ≤ (#‘𝐹))))
72	71	com13 86	. . . . . . . . 9 ⊢ (𝐹 ∈ V → (𝐸 ∈ V → ((¬ 𝐸 ∈ Fin ∧ ¬ 𝐹 ∈ Fin) → (#‘𝐸) ≤ (#‘𝐹))))
73	72	adantl 481	. . . . . . . 8 ⊢ ((𝑉 ∈ V ∧ 𝐹 ∈ V) → (𝐸 ∈ V → ((¬ 𝐸 ∈ Fin ∧ ¬ 𝐹 ∈ Fin) → (#‘𝐸) ≤ (#‘𝐹))))
74	19, 39, 73	3syl 18	. . . . . . 7 ⊢ (𝑉 ComplUSGrph 𝐹 → (𝐸 ∈ V → ((¬ 𝐸 ∈ Fin ∧ ¬ 𝐹 ∈ Fin) → (#‘𝐸) ≤ (#‘𝐹))))
75	74	com12 32	. . . . . 6 ⊢ (𝐸 ∈ V → (𝑉 ComplUSGrph 𝐹 → ((¬ 𝐸 ∈ Fin ∧ ¬ 𝐹 ∈ Fin) → (#‘𝐸) ≤ (#‘𝐹))))
76	75	adantl 481	. . . . 5 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ComplUSGrph 𝐹 → ((¬ 𝐸 ∈ Fin ∧ ¬ 𝐹 ∈ Fin) → (#‘𝐸) ≤ (#‘𝐹))))
77	1, 76	syl 17	. . . 4 ⊢ (𝑉 USGrph 𝐸 → (𝑉 ComplUSGrph 𝐹 → ((¬ 𝐸 ∈ Fin ∧ ¬ 𝐹 ∈ Fin) → (#‘𝐸) ≤ (#‘𝐹))))
78	77	imp 444	. . 3 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → ((¬ 𝐸 ∈ Fin ∧ ¬ 𝐹 ∈ Fin) → (#‘𝐸) ≤ (#‘𝐹)))
79	78	com12 32	. 2 ⊢ ((¬ 𝐸 ∈ Fin ∧ ¬ 𝐹 ∈ Fin) → ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (#‘𝐸) ≤ (#‘𝐹)))
80	38, 52, 57, 79	4cases 987	1 ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (#‘𝐸) ≤ (#‘𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∃wex 1695 ∈ wcel 1977 Vcvv 3173 class class class wbr 4583 I cid 4948 dom cdm 5038 ran crn 5039 ↾ cres 5040 –1-1→wf1 5801 ‘cfv 5804 ≼ cdom 7839 Fincfn 7841 +∞cpnf 9950 ℝ^*cxr 9952 ≤ cle 9954 #chash 12979 USGrph cusg 25859 ComplUSGrph ccusgra 25947

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-n0 11170 df-xnn0 11241 df-z 11255 df-uz 11564 df-fz 12198 df-hash 12980 df-usgra 25862 df-cusgra 25950

This theorem is referenced by: usgramaxsize 26015

W3C validator