Metamath Proof Explorer

Theorem cusgrfi

Description: If the size of a complete simple graph is finite, then its order is also finite. (Contributed by Alexander van der Vekens, 13-Jan-2018) (Revised by AV, 11-Nov-2020)

Ref Expression
Hypotheses cusgrfi.v ⊢V=Vtx⁡G
cusgrfi.e ⊢E=Edg⁡G
Assertion cusgrfi ⊢G∈ComplUSGraph∧E∈Fin→V∈Fin

Proof

Step Hyp Ref Expression
1 cusgrfi.v ⊢V=Vtx⁡G
2 cusgrfi.e ⊢E=Edg⁡G
3 nfielex ⊢¬V∈Fin→∃nn∈V
4 eqeq1 ⊢e=p→e=vn↔p=vn
5 4 anbi2d ⊢e=p→v≠n∧e=vn↔v≠n∧p=vn
6 5 rexbidv ⊢e=p→∃v∈Vv≠n∧e=vn↔∃v∈Vv≠n∧p=vn
7 6 cbvrabv ⊢e∈𝒫V|∃v∈Vv≠n∧e=vn=p∈𝒫V|∃v∈Vv≠n∧p=vn
8 eqid ⊢p∈V∖n⟼pn=p∈V∖n⟼pn
9 1 7 8 cusgrfilem3 ⊢n∈V→V∈Fin↔e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin
10 9 notbid ⊢n∈V→¬V∈Fin↔¬e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin
11 10 biimpac ⊢¬V∈Fin∧n∈V→¬e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin
12 1 7 cusgrfilem1 ⊢G∈ComplUSGraph∧n∈V→e∈𝒫V|∃v∈Vv≠n∧e=vn⊆Edg⁡G
13 2 eleq1i ⊢E∈Fin↔Edg⁡G∈Fin
14 ssfi ⊢Edg⁡G∈Fin∧e∈𝒫V|∃v∈Vv≠n∧e=vn⊆Edg⁡G→e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin
15 14 expcom ⊢e∈𝒫V|∃v∈Vv≠n∧e=vn⊆Edg⁡G→Edg⁡G∈Fin→e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin
16 13 15 biimtrid ⊢e∈𝒫V|∃v∈Vv≠n∧e=vn⊆Edg⁡G→E∈Fin→e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin
17 16 con3d ⊢e∈𝒫V|∃v∈Vv≠n∧e=vn⊆Edg⁡G→¬e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin→¬E∈Fin
18 12 17 syl ⊢G∈ComplUSGraph∧n∈V→¬e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin→¬E∈Fin
19 18 expcom ⊢n∈V→G∈ComplUSGraph→¬e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin→¬E∈Fin
20 19 com23 ⊢n∈V→¬e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin→G∈ComplUSGraph→¬E∈Fin
21 20 adantl ⊢¬V∈Fin∧n∈V→¬e∈𝒫V|∃v∈Vv≠n∧e=vn∈Fin→G∈ComplUSGraph→¬E∈Fin
22 11 21 mpd ⊢¬V∈Fin∧n∈V→G∈ComplUSGraph→¬E∈Fin
23 3 22 exlimddv ⊢¬V∈Fin→G∈ComplUSGraph→¬E∈Fin
24 23 com12 ⊢G∈ComplUSGraph→¬V∈Fin→¬E∈Fin
25 24 con4d ⊢G∈ComplUSGraph→E∈Fin→V∈Fin
26 25 imp ⊢G∈ComplUSGraph∧E∈Fin→V∈Fin