Step | Hyp | Ref
| Expression |
1 | | frgrregorufr0.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | frgrregorufr0.d |
. . . 4
⊢ 𝐷 = (VtxDeg‘𝐺) |
3 | | fveq2 6103 |
. . . . . 6
⊢ (𝑣 = 𝑡 → (𝐷‘𝑣) = (𝐷‘𝑡)) |
4 | 3 | eqeq1d 2612 |
. . . . 5
⊢ (𝑣 = 𝑡 → ((𝐷‘𝑣) = 𝐾 ↔ (𝐷‘𝑡) = 𝐾)) |
5 | 4 | cbvrabv 3172 |
. . . 4
⊢ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾} = {𝑡 ∈ 𝑉 ∣ (𝐷‘𝑡) = 𝐾} |
6 | | eqid 2610 |
. . . 4
⊢ (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) |
7 | | frgrregorufr0.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
8 | 1, 2, 5, 6, 7 | frgrwopreg 41486 |
. . 3
⊢ (𝐺 ∈ FriendGraph →
(((#‘{𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = 1 ∨ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾} = ∅) ∨ ((#‘(𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾})) = 1 ∨ (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = ∅))) |
9 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑟 → (𝐷‘𝑣) = (𝐷‘𝑟)) |
10 | 9 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑣 = 𝑟 → ((𝐷‘𝑣) = 𝐾 ↔ (𝐷‘𝑟) = 𝐾)) |
11 | 10 | cbvrabv 3172 |
. . . . . . . 8
⊢ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾} = {𝑟 ∈ 𝑉 ∣ (𝐷‘𝑟) = 𝐾} |
12 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑣 → (𝐷‘𝑠) = (𝐷‘𝑣)) |
13 | 12 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑣 → ((𝐷‘𝑠) = 𝐾 ↔ (𝐷‘𝑣) = 𝐾)) |
14 | 13 | cbvrabv 3172 |
. . . . . . . . 9
⊢ {𝑠 ∈ 𝑉 ∣ (𝐷‘𝑠) = 𝐾} = {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾} |
15 | 14 | difeq2i 3687 |
. . . . . . . 8
⊢ (𝑉 ∖ {𝑠 ∈ 𝑉 ∣ (𝐷‘𝑠) = 𝐾}) = (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) |
16 | 1, 2, 11, 15, 7 | frgrwopreg1 41487 |
. . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧
(#‘{𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = 1) → ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸) |
17 | 16 | 3mix3d 1231 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧
(#‘{𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = 1) → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸)) |
18 | 17 | expcom 450 |
. . . . 5
⊢
((#‘{𝑣 ∈
𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = 1 → (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
19 | | rabeq0 3911 |
. . . . . 6
⊢ ({𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾} = ∅ ↔ ∀𝑣 ∈ 𝑉 ¬ (𝐷‘𝑣) = 𝐾) |
20 | | neqne 2790 |
. . . . . . . . 9
⊢ (¬
(𝐷‘𝑣) = 𝐾 → (𝐷‘𝑣) ≠ 𝐾) |
21 | 20 | ralimi 2936 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝑉 ¬ (𝐷‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾) |
22 | 21 | 3mix2d 1230 |
. . . . . . 7
⊢
(∀𝑣 ∈
𝑉 ¬ (𝐷‘𝑣) = 𝐾 → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸)) |
23 | 22 | a1d 25 |
. . . . . 6
⊢
(∀𝑣 ∈
𝑉 ¬ (𝐷‘𝑣) = 𝐾 → (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
24 | 19, 23 | sylbi 206 |
. . . . 5
⊢ ({𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾} = ∅ → (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
25 | 18, 24 | jaoi 393 |
. . . 4
⊢
(((#‘{𝑣 ∈
𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = 1 ∨ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾} = ∅) → (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
26 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → (𝐷‘𝑟) = (𝐷‘𝑠)) |
27 | 26 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑟 = 𝑠 → ((𝐷‘𝑟) = 𝐾 ↔ (𝐷‘𝑠) = 𝐾)) |
28 | 27 | cbvrabv 3172 |
. . . . . . . 8
⊢ {𝑟 ∈ 𝑉 ∣ (𝐷‘𝑟) = 𝐾} = {𝑠 ∈ 𝑉 ∣ (𝐷‘𝑠) = 𝐾} |
29 | 11 | difeq2i 3687 |
. . . . . . . 8
⊢ (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = (𝑉 ∖ {𝑟 ∈ 𝑉 ∣ (𝐷‘𝑟) = 𝐾}) |
30 | 1, 2, 28, 29, 7 | frgrwopreg2 41488 |
. . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧
(#‘(𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾})) = 1) → ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸) |
31 | 30 | 3mix3d 1231 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧
(#‘(𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾})) = 1) → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸)) |
32 | 31 | expcom 450 |
. . . . 5
⊢
((#‘(𝑉 ∖
{𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾})) = 1 → (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
33 | | difrab0eq 3990 |
. . . . . 6
⊢ ((𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = ∅ ↔ 𝑉 = {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) |
34 | | rabid2 3096 |
. . . . . . 7
⊢ (𝑉 = {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾} ↔ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾) |
35 | | 3mix1 1223 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝑉 (𝐷‘𝑣) = 𝐾 → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸)) |
36 | 35 | a1d 25 |
. . . . . . 7
⊢
(∀𝑣 ∈
𝑉 (𝐷‘𝑣) = 𝐾 → (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
37 | 34, 36 | sylbi 206 |
. . . . . 6
⊢ (𝑉 = {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾} → (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
38 | 33, 37 | sylbi 206 |
. . . . 5
⊢ ((𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = ∅ → (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
39 | 32, 38 | jaoi 393 |
. . . 4
⊢
(((#‘(𝑉
∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾})) = 1 ∨ (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = ∅) → (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
40 | 25, 39 | jaoi 393 |
. . 3
⊢
((((#‘{𝑣
∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = 1 ∨ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾} = ∅) ∨ ((#‘(𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾})) = 1 ∨ (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ (𝐷‘𝑣) = 𝐾}) = ∅)) → (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
41 | 8, 40 | mpcom 37 |
. 2
⊢ (𝐺 ∈ FriendGraph →
(∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸)) |
42 | | biidd 251 |
. . 3
⊢ (𝐺 ∈ FriendGraph →
(∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)) |
43 | | biidd 251 |
. . 3
⊢ (𝐺 ∈ FriendGraph →
(∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ↔ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾)) |
44 | | sneq 4135 |
. . . . . . 7
⊢ (𝑣 = 𝑡 → {𝑣} = {𝑡}) |
45 | 44 | difeq2d 3690 |
. . . . . 6
⊢ (𝑣 = 𝑡 → (𝑉 ∖ {𝑣}) = (𝑉 ∖ {𝑡})) |
46 | | preq1 4212 |
. . . . . . 7
⊢ (𝑣 = 𝑡 → {𝑣, 𝑤} = {𝑡, 𝑤}) |
47 | 46 | eleq1d 2672 |
. . . . . 6
⊢ (𝑣 = 𝑡 → ({𝑣, 𝑤} ∈ 𝐸 ↔ {𝑡, 𝑤} ∈ 𝐸)) |
48 | 45, 47 | raleqbidv 3129 |
. . . . 5
⊢ (𝑣 = 𝑡 → (∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸 ↔ ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸)) |
49 | 48 | cbvrexv 3148 |
. . . 4
⊢
(∃𝑣 ∈
𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸) |
50 | 49 | a1i 11 |
. . 3
⊢ (𝐺 ∈ FriendGraph →
(∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸 ↔ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸)) |
51 | 42, 43, 50 | 3orbi123d 1390 |
. 2
⊢ (𝐺 ∈ FriendGraph →
((∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸) ↔ (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ 𝐸))) |
52 | 41, 51 | mpbird 246 |
1
⊢ (𝐺 ∈ FriendGraph →
(∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸)) |