Proof of Theorem 1to3vfriswmgr
Step | Hyp | Ref
| Expression |
1 | | df-3or 1032 |
. . 3
⊢ ((𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵} ∨ 𝑉 = {𝐴, 𝐵, 𝐶}) ↔ ((𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵}) ∨ 𝑉 = {𝐴, 𝐵, 𝐶})) |
2 | | 3vfriswmgr.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
3 | | 3vfriswmgr.e |
. . . . . 6
⊢ 𝐸 = (Edg‘𝐺) |
4 | 2, 3 | 1to2vfriswmgr 41449 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵})) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |
5 | 4 | expcom 450 |
. . . 4
⊢ ((𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵}) → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
6 | | tppreq3 4238 |
. . . . . . 7
⊢ (𝐵 = 𝐶 → {𝐴, 𝐵, 𝐶} = {𝐴, 𝐵}) |
7 | 6 | eqeq2d 2620 |
. . . . . 6
⊢ (𝐵 = 𝐶 → (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐴, 𝐵})) |
8 | | olc 398 |
. . . . . . . . . 10
⊢ (𝑉 = {𝐴, 𝐵} → (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵})) |
9 | 8 | anim1i 590 |
. . . . . . . . 9
⊢ ((𝑉 = {𝐴, 𝐵} ∧ 𝐴 ∈ 𝑋) → ((𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵}) ∧ 𝐴 ∈ 𝑋)) |
10 | 9 | ancomd 466 |
. . . . . . . 8
⊢ ((𝑉 = {𝐴, 𝐵} ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵}))) |
11 | 10, 4 | syl 17 |
. . . . . . 7
⊢ ((𝑉 = {𝐴, 𝐵} ∧ 𝐴 ∈ 𝑋) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |
12 | 11 | ex 449 |
. . . . . 6
⊢ (𝑉 = {𝐴, 𝐵} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
13 | 7, 12 | syl6bi 242 |
. . . . 5
⊢ (𝐵 = 𝐶 → (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))))) |
14 | | tpprceq3 4276 |
. . . . . . . 8
⊢ (¬
(𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) → {𝐶, 𝐴, 𝐵} = {𝐶, 𝐴}) |
15 | | tprot 4228 |
. . . . . . . . . . . . 13
⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶} |
16 | 15 | eqeq1i 2615 |
. . . . . . . . . . . 12
⊢ ({𝐶, 𝐴, 𝐵} = {𝐶, 𝐴} ↔ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴}) |
17 | 16 | biimpi 205 |
. . . . . . . . . . 11
⊢ ({𝐶, 𝐴, 𝐵} = {𝐶, 𝐴} → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴}) |
18 | | prcom 4211 |
. . . . . . . . . . 11
⊢ {𝐶, 𝐴} = {𝐴, 𝐶} |
19 | 17, 18 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ({𝐶, 𝐴, 𝐵} = {𝐶, 𝐴} → {𝐴, 𝐵, 𝐶} = {𝐴, 𝐶}) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . 9
⊢ ({𝐶, 𝐴, 𝐵} = {𝐶, 𝐴} → (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐴, 𝐶})) |
21 | | olc 398 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝐴, 𝐶} → (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐶})) |
22 | 2, 3 | 1to2vfriswmgr 41449 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐶})) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |
23 | 21, 22 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑉 = {𝐴, 𝐶}) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |
24 | 23 | expcom 450 |
. . . . . . . . 9
⊢ (𝑉 = {𝐴, 𝐶} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
25 | 20, 24 | syl6bi 242 |
. . . . . . . 8
⊢ ({𝐶, 𝐴, 𝐵} = {𝐶, 𝐴} → (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))))) |
26 | 14, 25 | syl 17 |
. . . . . . 7
⊢ (¬
(𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) → (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))))) |
27 | 26 | a1d 25 |
. . . . . 6
⊢ (¬
(𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) → (𝐵 ≠ 𝐶 → (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))))) |
28 | | tpprceq3 4276 |
. . . . . . . 8
⊢ (¬
(𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) → {𝐵, 𝐴, 𝐶} = {𝐵, 𝐴}) |
29 | | tpcoma 4229 |
. . . . . . . . . . . . 13
⊢ {𝐵, 𝐴, 𝐶} = {𝐴, 𝐵, 𝐶} |
30 | 29 | eqeq1i 2615 |
. . . . . . . . . . . 12
⊢ ({𝐵, 𝐴, 𝐶} = {𝐵, 𝐴} ↔ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴}) |
31 | 30 | biimpi 205 |
. . . . . . . . . . 11
⊢ ({𝐵, 𝐴, 𝐶} = {𝐵, 𝐴} → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴}) |
32 | | prcom 4211 |
. . . . . . . . . . 11
⊢ {𝐵, 𝐴} = {𝐴, 𝐵} |
33 | 31, 32 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ({𝐵, 𝐴, 𝐶} = {𝐵, 𝐴} → {𝐴, 𝐵, 𝐶} = {𝐴, 𝐵}) |
34 | 33 | eqeq2d 2620 |
. . . . . . . . 9
⊢ ({𝐵, 𝐴, 𝐶} = {𝐵, 𝐴} → (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐴, 𝐵})) |
35 | 8, 4 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑉 = {𝐴, 𝐵}) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |
36 | 35 | expcom 450 |
. . . . . . . . . 10
⊢ (𝑉 = {𝐴, 𝐵} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
37 | 36 | a1d 25 |
. . . . . . . . 9
⊢ (𝑉 = {𝐴, 𝐵} → (𝐵 ≠ 𝐶 → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))))) |
38 | 34, 37 | syl6bi 242 |
. . . . . . . 8
⊢ ({𝐵, 𝐴, 𝐶} = {𝐵, 𝐴} → (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐵 ≠ 𝐶 → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))))) |
39 | 28, 38 | syl 17 |
. . . . . . 7
⊢ (¬
(𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) → (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐵 ≠ 𝐶 → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))))) |
40 | 39 | com23 84 |
. . . . . 6
⊢ (¬
(𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) → (𝐵 ≠ 𝐶 → (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))))) |
41 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) → 𝐵 ∈ V) |
42 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) → 𝐶 ∈ V) |
43 | 41, 42 | anim12i 588 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) → (𝐵 ∈ V ∧ 𝐶 ∈ V)) |
44 | 43 | ad2antrr 758 |
. . . . . . . . . . 11
⊢
(((((𝐵 ∈ V
∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐵 ∈ V ∧ 𝐶 ∈ V)) |
45 | 44 | anim1i 590 |
. . . . . . . . . 10
⊢
((((((𝐵 ∈ V
∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐴 ∈ 𝑋) → ((𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝐴 ∈ 𝑋)) |
46 | 45 | ancomd 466 |
. . . . . . . . 9
⊢
((((((𝐵 ∈ V
∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑋 ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V))) |
47 | | 3anass 1035 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐴 ∈ 𝑋 ∧ (𝐵 ∈ V ∧ 𝐶 ∈ V))) |
48 | 46, 47 | sylibr 223 |
. . . . . . . 8
⊢
((((((𝐵 ∈ V
∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V)) |
49 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) → 𝐵 ≠ 𝐴) |
50 | 49 | necomd 2837 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) → 𝐴 ≠ 𝐵) |
51 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) → 𝐶 ≠ 𝐴) |
52 | 51 | necomd 2837 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ V ∧ 𝐶 ≠ 𝐴) → 𝐴 ≠ 𝐶) |
53 | 50, 52 | anim12i 588 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)) |
54 | 53 | anim1i 590 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) ∧ 𝐵 ≠ 𝐶) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶)) |
55 | | df-3an 1033 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ↔ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶)) |
56 | 54, 55 | sylibr 223 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) ∧ 𝐵 ≠ 𝐶) → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) |
57 | 56 | ad2antrr 758 |
. . . . . . . 8
⊢
((((((𝐵 ∈ V
∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐴 ∈ 𝑋) → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) |
58 | | simplr 788 |
. . . . . . . 8
⊢
((((((𝐵 ∈ V
∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐴 ∈ 𝑋) → 𝑉 = {𝐴, 𝐵, 𝐶}) |
59 | 2, 3 | 3vfriswmgr 41448 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |
60 | 48, 57, 58, 59 | syl3anc 1318 |
. . . . . . 7
⊢
((((((𝐵 ∈ V
∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ 𝐴 ∈ 𝑋) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |
61 | 60 | exp41 636 |
. . . . . 6
⊢ (((𝐵 ∈ V ∧ 𝐵 ≠ 𝐴) ∧ (𝐶 ∈ V ∧ 𝐶 ≠ 𝐴)) → (𝐵 ≠ 𝐶 → (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))))) |
62 | 27, 40, 61 | ecase 980 |
. . . . 5
⊢ (𝐵 ≠ 𝐶 → (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))))) |
63 | 13, 62 | pm2.61ine 2865 |
. . . 4
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
64 | 5, 63 | jaoi 393 |
. . 3
⊢ (((𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵}) ∨ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
65 | 1, 64 | sylbi 206 |
. 2
⊢ ((𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵} ∨ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐴 ∈ 𝑋 → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))) |
66 | 65 | impcom 445 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵} ∨ 𝑉 = {𝐴, 𝐵, 𝐶})) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) |