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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
cusgrfi.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion cusgrfi ( ( 𝐺 ∈ ComplUSGraph ∧ 𝐸 ∈ Fin ) → 𝑉 ∈ Fin )

Proof

Step Hyp Ref Expression
1 cusgrfi.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgrfi.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 nfielex ⊢ ( ¬ 𝑉 ∈ Fin → ∃ 𝑛 𝑛 ∈ 𝑉 )
4 eqeq1 ⊢ ( 𝑒 = 𝑝 → ( 𝑒 = { 𝑣 , 𝑛 } ↔ 𝑝 = { 𝑣 , 𝑛 } ) )
5 4 anbi2d ⊢ ( 𝑒 = 𝑝 → ( ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) ↔ ( 𝑣 ≠ 𝑛 ∧ 𝑝 = { 𝑣 , 𝑛 } ) ) )
6 5 rexbidv ⊢ ( 𝑒 = 𝑝 → ( ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) ↔ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑝 = { 𝑣 , 𝑛 } ) ) )
7 6 cbvrabv ⊢ { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑝 = { 𝑣 , 𝑛 } ) }
8 eqid ⊢ ( 𝑝 ∈ ( 𝑉 ∖ { 𝑛 } ) ↦ { 𝑝 , 𝑛 } ) = ( 𝑝 ∈ ( 𝑉 ∖ { 𝑛 } ) ↦ { 𝑝 , 𝑛 } )
9 1 7 8 cusgrfilem3 ⊢ ( 𝑛 ∈ 𝑉 → ( 𝑉 ∈ Fin ↔ { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin ) )
10 9 notbid ⊢ ( 𝑛 ∈ 𝑉 → ( ¬ 𝑉 ∈ Fin ↔ ¬ { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin ) )
11 10 biimpac ⊢ ( ( ¬ 𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉 ) → ¬ { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin )
12 1 7 cusgrfilem1 ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑛 ∈ 𝑉 ) → { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ⊆ ( Edg ‘ 𝐺 ) )
13 2 eleq1i ⊢ ( 𝐸 ∈ Fin ↔ ( Edg ‘ 𝐺 ) ∈ Fin )
14 ssfi ⊢ ( ( ( Edg ‘ 𝐺 ) ∈ Fin ∧ { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ⊆ ( Edg ‘ 𝐺 ) ) → { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin )
15 14 expcom ⊢ ( { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ⊆ ( Edg ‘ 𝐺 ) → ( ( Edg ‘ 𝐺 ) ∈ Fin → { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin ) )
16 13 15 biimtrid ⊢ ( { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ⊆ ( Edg ‘ 𝐺 ) → ( 𝐸 ∈ Fin → { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin ) )
17 16 con3d ⊢ ( { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ⊆ ( Edg ‘ 𝐺 ) → ( ¬ { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin → ¬ 𝐸 ∈ Fin ) )
18 12 17 syl ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑛 ∈ 𝑉 ) → ( ¬ { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin → ¬ 𝐸 ∈ Fin ) )
19 18 expcom ⊢ ( 𝑛 ∈ 𝑉 → ( 𝐺 ∈ ComplUSGraph → ( ¬ { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin → ¬ 𝐸 ∈ Fin ) ) )
20 19 com23 ⊢ ( 𝑛 ∈ 𝑉 → ( ¬ { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin → ( 𝐺 ∈ ComplUSGraph → ¬ 𝐸 ∈ Fin ) ) )
21 20 adantl ⊢ ( ( ¬ 𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉 ) → ( ¬ { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ∈ Fin → ( 𝐺 ∈ ComplUSGraph → ¬ 𝐸 ∈ Fin ) ) )
22 11 21 mpd ⊢ ( ( ¬ 𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉 ) → ( 𝐺 ∈ ComplUSGraph → ¬ 𝐸 ∈ Fin ) )
23 3 22 exlimddv ⊢ ( ¬ 𝑉 ∈ Fin → ( 𝐺 ∈ ComplUSGraph → ¬ 𝐸 ∈ Fin ) )
24 23 com12 ⊢ ( 𝐺 ∈ ComplUSGraph → ( ¬ 𝑉 ∈ Fin → ¬ 𝐸 ∈ Fin ) )
25 24 con4d ⊢ ( 𝐺 ∈ ComplUSGraph → ( 𝐸 ∈ Fin → 𝑉 ∈ Fin ) )
26 25 imp ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝐸 ∈ Fin ) → 𝑉 ∈ Fin )