Step |
Hyp |
Ref |
Expression |
1 |
|
umgrvad2edg.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
2 |
|
simpl |
⊢ ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → { 𝑁 , 𝐴 } ∈ 𝐸 ) |
3 |
|
simpr |
⊢ ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → { 𝐵 , 𝑁 } ∈ 𝐸 ) |
4 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
5 |
4 1
|
umgrpredgv |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝐴 } ∈ 𝐸 ) → ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) |
6 |
5
|
ex |
⊢ ( 𝐺 ∈ UMGraph → ( { 𝑁 , 𝐴 } ∈ 𝐸 → ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
7 |
4 1
|
umgrpredgv |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) |
8 |
7
|
ex |
⊢ ( 𝐺 ∈ UMGraph → ( { 𝐵 , 𝑁 } ∈ 𝐸 → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
9 |
6 8
|
anim12d |
⊢ ( 𝐺 ∈ UMGraph → ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ) ) |
10 |
9
|
adantr |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) → ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ) ) |
11 |
10
|
imp |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
12 |
|
simplr |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐴 ≠ 𝐵 ) |
13 |
1
|
umgredgne |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝐴 } ∈ 𝐸 ) → 𝑁 ≠ 𝐴 ) |
14 |
13
|
necomd |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝐴 } ∈ 𝐸 ) → 𝐴 ≠ 𝑁 ) |
15 |
14
|
ad2ant2r |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → 𝐴 ≠ 𝑁 ) |
16 |
12 15
|
jca |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝑁 ) ) |
17 |
16
|
olcd |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( ( 𝑁 ≠ 𝐵 ∧ 𝑁 ≠ 𝑁 ) ∨ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝑁 ) ) ) |
18 |
|
prneimg |
⊢ ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝑁 ≠ 𝐵 ∧ 𝑁 ≠ 𝑁 ) ∨ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝑁 ) ) → { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ) ) |
19 |
18
|
imp |
⊢ ( ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑁 ≠ 𝐵 ∧ 𝑁 ≠ 𝑁 ) ∨ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝑁 ) ) ) → { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ) |
20 |
|
prid1g |
⊢ ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) → 𝑁 ∈ { 𝑁 , 𝐴 } ) |
21 |
20
|
ad3antrrr |
⊢ ( ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑁 ≠ 𝐵 ∧ 𝑁 ≠ 𝑁 ) ∨ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝑁 ) ) ) → 𝑁 ∈ { 𝑁 , 𝐴 } ) |
22 |
|
prid2g |
⊢ ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) → 𝑁 ∈ { 𝐵 , 𝑁 } ) |
23 |
22
|
ad3antrrr |
⊢ ( ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑁 ≠ 𝐵 ∧ 𝑁 ≠ 𝑁 ) ∨ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝑁 ) ) ) → 𝑁 ∈ { 𝐵 , 𝑁 } ) |
24 |
19 21 23
|
3jca |
⊢ ( ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑁 ≠ 𝐵 ∧ 𝑁 ≠ 𝑁 ) ∨ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝑁 ) ) ) → ( { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ∧ 𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁 ∈ { 𝐵 , 𝑁 } ) ) |
25 |
11 17 24
|
syl2anc |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ( { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ∧ 𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁 ∈ { 𝐵 , 𝑁 } ) ) |
26 |
|
neeq1 |
⊢ ( 𝑥 = { 𝑁 , 𝐴 } → ( 𝑥 ≠ 𝑦 ↔ { 𝑁 , 𝐴 } ≠ 𝑦 ) ) |
27 |
|
eleq2 |
⊢ ( 𝑥 = { 𝑁 , 𝐴 } → ( 𝑁 ∈ 𝑥 ↔ 𝑁 ∈ { 𝑁 , 𝐴 } ) ) |
28 |
26 27
|
3anbi12d |
⊢ ( 𝑥 = { 𝑁 , 𝐴 } → ( ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) ↔ ( { 𝑁 , 𝐴 } ≠ 𝑦 ∧ 𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁 ∈ 𝑦 ) ) ) |
29 |
|
neeq2 |
⊢ ( 𝑦 = { 𝐵 , 𝑁 } → ( { 𝑁 , 𝐴 } ≠ 𝑦 ↔ { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ) ) |
30 |
|
eleq2 |
⊢ ( 𝑦 = { 𝐵 , 𝑁 } → ( 𝑁 ∈ 𝑦 ↔ 𝑁 ∈ { 𝐵 , 𝑁 } ) ) |
31 |
29 30
|
3anbi13d |
⊢ ( 𝑦 = { 𝐵 , 𝑁 } → ( ( { 𝑁 , 𝐴 } ≠ 𝑦 ∧ 𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁 ∈ 𝑦 ) ↔ ( { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ∧ 𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁 ∈ { 𝐵 , 𝑁 } ) ) ) |
32 |
28 31
|
rspc2ev |
⊢ ( ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ∧ ( { 𝑁 , 𝐴 } ≠ { 𝐵 , 𝑁 } ∧ 𝑁 ∈ { 𝑁 , 𝐴 } ∧ 𝑁 ∈ { 𝐵 , 𝑁 } ) ) → ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐸 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) ) |
33 |
2 3 25 32
|
syl2an23an |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( { 𝑁 , 𝐴 } ∈ 𝐸 ∧ { 𝐵 , 𝑁 } ∈ 𝐸 ) ) → ∃ 𝑥 ∈ 𝐸 ∃ 𝑦 ∈ 𝐸 ( 𝑥 ≠ 𝑦 ∧ 𝑁 ∈ 𝑥 ∧ 𝑁 ∈ 𝑦 ) ) |