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 e. ComplUSGraph /\ E e. Fin ) -> V e. Fin )

Proof

Step Hyp Ref Expression
1 cusgrfi.v 
 |-  V = ( Vtx ` G )
2 cusgrfi.e 
 |-  E = ( Edg ` G )
3 nfielex 
 |-  ( -. V e. Fin -> E. n n e. 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 -> ( E. v e. V ( v =/= n /\ e = { v , n } ) <-> E. v e. V ( v =/= n /\ p = { v , n } ) ) )
7 6 cbvrabv 
 |-  { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } = { p e. ~P V | E. v e. V ( v =/= n /\ p = { v , n } ) }
8 eqid 
 |-  ( p e. ( V \ { n } ) |-> { p , n } ) = ( p e. ( V \ { n } ) |-> { p , n } )
9 1 7 8 cusgrfilem3 
 |-  ( n e. V -> ( V e. Fin <-> { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin ) )
10 9 notbid 
 |-  ( n e. V -> ( -. V e. Fin <-> -. { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin ) )
11 10 biimpac 
 |-  ( ( -. V e. Fin /\ n e. V ) -> -. { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin )
12 1 7 cusgrfilem1 
 |-  ( ( G e. ComplUSGraph /\ n e. V ) -> { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } C_ ( Edg ` G ) )
13 2 eleq1i 
 |-  ( E e. Fin <-> ( Edg ` G ) e. Fin )
14 ssfi 
 |-  ( ( ( Edg ` G ) e. Fin /\ { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } C_ ( Edg ` G ) ) -> { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin )
15 14 expcom 
 |-  ( { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } C_ ( Edg ` G ) -> ( ( Edg ` G ) e. Fin -> { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin ) )
16 13 15 syl5bi 
 |-  ( { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } C_ ( Edg ` G ) -> ( E e. Fin -> { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin ) )
17 16 con3d 
 |-  ( { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } C_ ( Edg ` G ) -> ( -. { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin -> -. E e. Fin ) )
18 12 17 syl 
 |-  ( ( G e. ComplUSGraph /\ n e. V ) -> ( -. { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin -> -. E e. Fin ) )
19 18 expcom 
 |-  ( n e. V -> ( G e. ComplUSGraph -> ( -. { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin -> -. E e. Fin ) ) )
20 19 com23 
 |-  ( n e. V -> ( -. { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin -> ( G e. ComplUSGraph -> -. E e. Fin ) ) )
21 20 adantl 
 |-  ( ( -. V e. Fin /\ n e. V ) -> ( -. { e e. ~P V | E. v e. V ( v =/= n /\ e = { v , n } ) } e. Fin -> ( G e. ComplUSGraph -> -. E e. Fin ) ) )
22 11 21 mpd 
 |-  ( ( -. V e. Fin /\ n e. V ) -> ( G e. ComplUSGraph -> -. E e. Fin ) )
23 3 22 exlimddv 
 |-  ( -. V e. Fin -> ( G e. ComplUSGraph -> -. E e. Fin ) )
24 23 com12 
 |-  ( G e. ComplUSGraph -> ( -. V e. Fin -> -. E e. Fin ) )
25 24 con4d 
 |-  ( G e. ComplUSGraph -> ( E e. Fin -> V e. Fin ) )
26 25 imp 
 |-  ( ( G e. ComplUSGraph /\ E e. Fin ) -> V e. Fin )