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 → ∃ n n ∈ V
4 eqeq1 ⊢ e = p → e = v n ↔ p = v n
5 4 anbi2d ⊢ e = p → v ≠ n ∧ e = v n ↔ v ≠ n ∧ p = v n
6 5 rexbidv ⊢ e = p → ∃ v ∈ V v ≠ n ∧ e = v n ↔ ∃ v ∈ V v ≠ n ∧ p = v n
7 6 cbvrabv ⊢ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n = p ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ p = v n
8 eqid ⊢ p ∈ V ∖ n ⟼ p n = p ∈ V ∖ n ⟼ p n
9 1 7 8 cusgrfilem3 ⊢ n ∈ V → V ∈ Fin ↔ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ Fin
10 9 notbid ⊢ n ∈ V → ¬ V ∈ Fin ↔ ¬ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ Fin
11 10 biimpac ⊢ ¬ V ∈ Fin ∧ n ∈ V → ¬ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ Fin
12 1 7 cusgrfilem1 ⊢ G ∈ ComplUSGraph ∧ n ∈ V → e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ⊆ Edg ⁡ G
13 2 eleq1i ⊢ E ∈ Fin ↔ Edg ⁡ G ∈ Fin
14 ssfi ⊢ Edg ⁡ G ∈ Fin ∧ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ⊆ Edg ⁡ G → e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ Fin
15 14 expcom ⊢ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ⊆ Edg ⁡ G → Edg ⁡ G ∈ Fin → e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ Fin
16 13 15 syl5bi ⊢ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ⊆ Edg ⁡ G → E ∈ Fin → e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ Fin
17 16 con3d ⊢ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ⊆ Edg ⁡ G → ¬ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ Fin → ¬ E ∈ Fin
18 12 17 syl ⊢ G ∈ ComplUSGraph ∧ n ∈ V → ¬ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ Fin → ¬ E ∈ Fin
19 18 expcom ⊢ n ∈ V → G ∈ ComplUSGraph → ¬ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ Fin → ¬ E ∈ Fin
20 19 com23 ⊢ n ∈ V → ¬ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ Fin → G ∈ ComplUSGraph → ¬ E ∈ Fin
21 20 adantl ⊢ ¬ V ∈ Fin ∧ n ∈ V → ¬ e ∈ 𝒫 V | ∃ v ∈ V v ≠ n ∧ e = v n ∈ 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