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	syl5bi	⊢ ( { 𝑒 ∈ 𝒫 𝑉 ∣ ∃ 𝑣 ∈ 𝑉 ( 𝑣 ≠ 𝑛 ∧ 𝑒 = { 𝑣 , 𝑛 } ) } ⊆ ( 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 )