Step |
Hyp |
Ref |
Expression |
1 |
|
3vfriswmgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
3vfriswmgr.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
1vwmgr |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑉 = { 𝐴 } ) → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) |
4 |
3
|
a1d |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑉 = { 𝐴 } ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |
5 |
4
|
expcom |
⊢ ( 𝑉 = { 𝐴 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) |
6 |
|
simpr |
⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 ) |
7 |
|
simpll |
⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐵 ∈ V ) |
8 |
|
simplr |
⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ≠ 𝐵 ) |
9 |
6 7 8
|
3jca |
⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ) |
10 |
1
|
eqeq1i |
⊢ ( 𝑉 = { 𝐴 , 𝐵 } ↔ ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 } ) |
11 |
10
|
biimpi |
⊢ ( 𝑉 = { 𝐴 , 𝐵 } → ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 } ) |
12 |
|
nfrgr2v |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 } ) → 𝐺 ∉ FriendGraph ) |
13 |
9 11 12
|
syl2anr |
⊢ ( ( 𝑉 = { 𝐴 , 𝐵 } ∧ ( ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ∈ 𝑋 ) ) → 𝐺 ∉ FriendGraph ) |
14 |
|
df-nel |
⊢ ( 𝐺 ∉ FriendGraph ↔ ¬ 𝐺 ∈ FriendGraph ) |
15 |
13 14
|
sylib |
⊢ ( ( 𝑉 = { 𝐴 , 𝐵 } ∧ ( ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ∈ 𝑋 ) ) → ¬ 𝐺 ∈ FriendGraph ) |
16 |
15
|
pm2.21d |
⊢ ( ( 𝑉 = { 𝐴 , 𝐵 } ∧ ( ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |
17 |
16
|
expcom |
⊢ ( ( ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) |
18 |
17
|
ex |
⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ 𝑋 → ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) ) |
19 |
18
|
com23 |
⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) ) |
20 |
|
ianor |
⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ↔ ( ¬ 𝐵 ∈ V ∨ ¬ 𝐴 ≠ 𝐵 ) ) |
21 |
|
prprc2 |
⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } = { 𝐴 } ) |
22 |
|
nne |
⊢ ( ¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵 ) |
23 |
|
preq2 |
⊢ ( 𝐵 = 𝐴 → { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } ) |
24 |
23
|
eqcoms |
⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } ) |
25 |
|
dfsn2 |
⊢ { 𝐴 } = { 𝐴 , 𝐴 } |
26 |
24 25
|
eqtr4di |
⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 } ) |
27 |
22 26
|
sylbi |
⊢ ( ¬ 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 } ) |
28 |
21 27
|
jaoi |
⊢ ( ( ¬ 𝐵 ∈ V ∨ ¬ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = { 𝐴 } ) |
29 |
20 28
|
sylbi |
⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = { 𝐴 } ) |
30 |
29
|
eqeq2d |
⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → ( 𝑉 = { 𝐴 , 𝐵 } ↔ 𝑉 = { 𝐴 } ) ) |
31 |
30 5
|
syl6bi |
⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) ) |
32 |
19 31
|
pm2.61i |
⊢ ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) |
33 |
5 32
|
jaoi |
⊢ ( ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) |
34 |
33
|
impcom |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |