Proof of Theorem 1to2vfriswmgr
Step | Hyp | Ref
| Expression |
1 | | 1vwmgr 28215 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑉 = {𝐴}) → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)) |
2 | 1 | a1d 25 |
. . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑉 = {𝐴}) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |
3 | 2 | expcom 417 |
. . 3
⊢ (𝑉 = {𝐴} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
4 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋) |
5 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋) → 𝐵 ∈ V) |
6 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋) → 𝐴 ≠ 𝐵) |
7 | 4, 5, 6 | 3jca 1129 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵)) |
8 | | 3vfriswmgr.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Vtx‘𝐺) |
9 | 8 | eqeq1i 2743 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝐴, 𝐵} ↔ (Vtx‘𝐺) = {𝐴, 𝐵}) |
10 | 9 | biimpi 219 |
. . . . . . . . . 10
⊢ (𝑉 = {𝐴, 𝐵} → (Vtx‘𝐺) = {𝐴, 𝐵}) |
11 | | nfrgr2v 28211 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ (Vtx‘𝐺) = {𝐴, 𝐵}) → 𝐺 ∉ FriendGraph ) |
12 | 7, 10, 11 | syl2anr 600 |
. . . . . . . . 9
⊢ ((𝑉 = {𝐴, 𝐵} ∧ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋)) → 𝐺 ∉ FriendGraph ) |
13 | | df-nel 3039 |
. . . . . . . . 9
⊢ (𝐺 ∉ FriendGraph ↔
¬ 𝐺 ∈ FriendGraph
) |
14 | 12, 13 | sylib 221 |
. . . . . . . 8
⊢ ((𝑉 = {𝐴, 𝐵} ∧ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋)) → ¬ 𝐺 ∈ FriendGraph ) |
15 | 14 | pm2.21d 121 |
. . . . . . 7
⊢ ((𝑉 = {𝐴, 𝐵} ∧ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋)) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |
16 | 15 | expcom 417 |
. . . . . 6
⊢ (((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋) → (𝑉 = {𝐴, 𝐵} → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
17 | 16 | ex 416 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) → (𝐴 ∈ 𝑋 → (𝑉 = {𝐴, 𝐵} → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))))) |
18 | 17 | com23 86 |
. . . 4
⊢ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) → (𝑉 = {𝐴, 𝐵} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))))) |
19 | | ianor 981 |
. . . . . . 7
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ↔ (¬ 𝐵 ∈ V ∨ ¬ 𝐴 ≠ 𝐵)) |
20 | | prprc2 4657 |
. . . . . . . 8
⊢ (¬
𝐵 ∈ V → {𝐴, 𝐵} = {𝐴}) |
21 | | nne 2938 |
. . . . . . . . 9
⊢ (¬
𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) |
22 | | preq2 4625 |
. . . . . . . . . . 11
⊢ (𝐵 = 𝐴 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
23 | 22 | eqcoms 2746 |
. . . . . . . . . 10
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
24 | | dfsn2 4529 |
. . . . . . . . . 10
⊢ {𝐴} = {𝐴, 𝐴} |
25 | 23, 24 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴}) |
26 | 21, 25 | sylbi 220 |
. . . . . . . 8
⊢ (¬
𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐴}) |
27 | 20, 26 | jaoi 856 |
. . . . . . 7
⊢ ((¬
𝐵 ∈ V ∨ ¬ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} = {𝐴}) |
28 | 19, 27 | sylbi 220 |
. . . . . 6
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} = {𝐴}) |
29 | 28 | eqeq2d 2749 |
. . . . 5
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) → (𝑉 = {𝐴, 𝐵} ↔ 𝑉 = {𝐴})) |
30 | 29, 3 | syl6bi 256 |
. . . 4
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) → (𝑉 = {𝐴, 𝐵} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))))) |
31 | 18, 30 | pm2.61i 185 |
. . 3
⊢ (𝑉 = {𝐴, 𝐵} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
32 | 3, 31 | jaoi 856 |
. 2
⊢ ((𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵}) → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
33 | 32 | impcom 411 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵})) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |