Step |
Hyp |
Ref |
Expression |
1 |
|
fusgrmaxsize.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
fusgrmaxsize.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
1
|
isfusgr |
⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ) |
4 |
|
cusgrexg |
⊢ ( 𝑉 ∈ Fin → ∃ 𝑒 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph ) |
5 |
4
|
adantl |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) → ∃ 𝑒 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph ) |
6 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
7 |
|
vex |
⊢ 𝑒 ∈ V |
8 |
6 7
|
opvtxfvi |
⊢ ( Vtx ‘ 〈 𝑉 , 𝑒 〉 ) = 𝑉 |
9 |
8
|
eqcomi |
⊢ 𝑉 = ( Vtx ‘ 〈 𝑉 , 𝑒 〉 ) |
10 |
|
eqid |
⊢ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) = ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) |
11 |
1 2 9 10
|
sizusglecusg |
⊢ ( ( 𝐺 ∈ USGraph ∧ 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) ) |
12 |
11
|
adantlr |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ∧ 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) ) |
13 |
9 10
|
cusgrsize |
⊢ ( ( 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ) |
14 |
|
breq2 |
⊢ ( ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) = ( ( ♯ ‘ 𝑉 ) C 2 ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) ↔ ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) |
15 |
14
|
biimpd |
⊢ ( ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) = ( ( ♯ ‘ 𝑉 ) C 2 ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) |
16 |
13 15
|
syl |
⊢ ( ( 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) |
17 |
16
|
expcom |
⊢ ( 𝑉 ∈ Fin → ( 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) |
18 |
17
|
adantl |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) → ( 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) ) |
19 |
18
|
imp |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ∧ 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ 〈 𝑉 , 𝑒 〉 ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) |
20 |
12 19
|
mpd |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ∧ 〈 𝑉 , 𝑒 〉 ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) |
21 |
5 20
|
exlimddv |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) |
22 |
3 21
|
sylbi |
⊢ ( 𝐺 ∈ FinUSGraph → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) |