Step |
Hyp |
Ref |
Expression |
1 |
|
cplgr0v.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
cplgr2v.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
simpl |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) → 𝐺 ∈ UHGraph ) |
4 |
|
fveq2 |
⊢ ( 𝑉 = { 𝐴 , 𝐵 } → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ { 𝐴 , 𝐵 } ) ) |
5 |
4
|
adantl |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ { 𝐴 , 𝐵 } ) ) |
6 |
|
elex |
⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ V ) |
7 |
|
elex |
⊢ ( 𝐵 ∈ 𝑌 → 𝐵 ∈ V ) |
8 |
|
id |
⊢ ( 𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵 ) |
9 |
|
hashprb |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) |
10 |
9
|
biimpi |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) |
11 |
6 7 8 10
|
syl3an |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) |
12 |
5 11
|
sylan9eqr |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( ♯ ‘ 𝑉 ) = 2 ) |
13 |
1 2
|
cplgr2v |
⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ( 𝐺 ∈ ComplGraph ↔ 𝑉 ∈ 𝐸 ) ) |
14 |
3 12 13
|
syl2an2 |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝐺 ∈ ComplGraph ↔ 𝑉 ∈ 𝐸 ) ) |
15 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → 𝑉 = { 𝐴 , 𝐵 } ) |
16 |
15
|
eleq1d |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝑉 ∈ 𝐸 ↔ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) |
17 |
14 16
|
bitrd |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝐺 ∈ ComplGraph ↔ { 𝐴 , 𝐵 } ∈ 𝐸 ) ) |