Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . 6
⊢ (𝑣 = 𝑡 → ((𝑉 VDeg 𝐸)‘𝑣) = ((𝑉 VDeg 𝐸)‘𝑡)) |
2 | 1 | eqeq1d 2612 |
. . . . 5
⊢ (𝑣 = 𝑡 → (((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ↔ ((𝑉 VDeg 𝐸)‘𝑡) = 𝐾)) |
3 | 2 | cbvrabv 3172 |
. . . 4
⊢ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾} = {𝑡 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑡) = 𝐾} |
4 | | eqid 2610 |
. . . 4
⊢ (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) |
5 | 3, 4 | frgrawopreg 26576 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → (((#‘{𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = 1 ∨ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾} = ∅) ∨ ((#‘(𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾})) = 1 ∨ (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = ∅))) |
6 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑟 → ((𝑉 VDeg 𝐸)‘𝑣) = ((𝑉 VDeg 𝐸)‘𝑟)) |
7 | 6 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑣 = 𝑟 → (((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ↔ ((𝑉 VDeg 𝐸)‘𝑟) = 𝐾)) |
8 | 7 | cbvrabv 3172 |
. . . . . . . 8
⊢ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾} = {𝑟 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑟) = 𝐾} |
9 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑣 → ((𝑉 VDeg 𝐸)‘𝑠) = ((𝑉 VDeg 𝐸)‘𝑣)) |
10 | 9 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑣 → (((𝑉 VDeg 𝐸)‘𝑠) = 𝐾 ↔ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾)) |
11 | 10 | cbvrabv 3172 |
. . . . . . . . 9
⊢ {𝑠 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑠) = 𝐾} = {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾} |
12 | 11 | difeq2i 3687 |
. . . . . . . 8
⊢ (𝑉 ∖ {𝑠 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑠) = 𝐾}) = (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) |
13 | 8, 12 | frgrawopreg1 26577 |
. . . . . . 7
⊢ ((𝑉 FriendGrph 𝐸 ∧ (#‘{𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = 1) → ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸) |
14 | 13 | 3mix3d 1231 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ (#‘{𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = 1) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸)) |
15 | 14 | expcom 450 |
. . . . 5
⊢
((#‘{𝑣 ∈
𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = 1 → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
16 | | rabeq0 3911 |
. . . . . 6
⊢ ({𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾} = ∅ ↔ ∀𝑣 ∈ 𝑉 ¬ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) |
17 | | df-ne 2782 |
. . . . . . . . . 10
⊢ (((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ↔ ¬ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) |
18 | 17 | biimpri 217 |
. . . . . . . . 9
⊢ (¬
((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾) |
19 | 18 | ralimi 2936 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝑉 ¬ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾) |
20 | 19 | 3mix2d 1230 |
. . . . . . 7
⊢
(∀𝑣 ∈
𝑉 ¬ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸)) |
21 | 20 | a1d 25 |
. . . . . 6
⊢
(∀𝑣 ∈
𝑉 ¬ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
22 | 16, 21 | sylbi 206 |
. . . . 5
⊢ ({𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾} = ∅ → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
23 | 15, 22 | jaoi 393 |
. . . 4
⊢
(((#‘{𝑣 ∈
𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = 1 ∨ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾} = ∅) → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
24 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → ((𝑉 VDeg 𝐸)‘𝑟) = ((𝑉 VDeg 𝐸)‘𝑠)) |
25 | 24 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑟 = 𝑠 → (((𝑉 VDeg 𝐸)‘𝑟) = 𝐾 ↔ ((𝑉 VDeg 𝐸)‘𝑠) = 𝐾)) |
26 | 25 | cbvrabv 3172 |
. . . . . . . 8
⊢ {𝑟 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑟) = 𝐾} = {𝑠 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑠) = 𝐾} |
27 | 8 | difeq2i 3687 |
. . . . . . . 8
⊢ (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = (𝑉 ∖ {𝑟 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑟) = 𝐾}) |
28 | 26, 27 | frgrawopreg2 26578 |
. . . . . . 7
⊢ ((𝑉 FriendGrph 𝐸 ∧ (#‘(𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾})) = 1) → ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸) |
29 | 28 | 3mix3d 1231 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ (#‘(𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾})) = 1) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸)) |
30 | 29 | expcom 450 |
. . . . 5
⊢
((#‘(𝑉 ∖
{𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾})) = 1 → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
31 | | difrab0eq 3990 |
. . . . . 6
⊢ ((𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = ∅ ↔ 𝑉 = {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) |
32 | | rabid2 3096 |
. . . . . . 7
⊢ (𝑉 = {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾} ↔ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) |
33 | | 3mix1 1223 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸)) |
34 | 33 | a1d 25 |
. . . . . . 7
⊢
(∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
35 | 32, 34 | sylbi 206 |
. . . . . 6
⊢ (𝑉 = {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾} → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
36 | 31, 35 | sylbi 206 |
. . . . 5
⊢ ((𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = ∅ → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
37 | 30, 36 | jaoi 393 |
. . . 4
⊢
(((#‘(𝑉
∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾})) = 1 ∨ (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = ∅) → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
38 | 23, 37 | jaoi 393 |
. . 3
⊢
((((#‘{𝑣
∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = 1 ∨ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾} = ∅) ∨ ((#‘(𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾})) = 1 ∨ (𝑉 ∖ {𝑣 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾}) = ∅)) → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
39 | 5, 38 | mpcom 37 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸)) |
40 | | biidd 251 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾)) |
41 | | biidd 251 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ↔ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾)) |
42 | | sneq 4135 |
. . . . . . 7
⊢ (𝑣 = 𝑡 → {𝑣} = {𝑡}) |
43 | 42 | difeq2d 3690 |
. . . . . 6
⊢ (𝑣 = 𝑡 → (𝑉 ∖ {𝑣}) = (𝑉 ∖ {𝑡})) |
44 | | preq1 4212 |
. . . . . . 7
⊢ (𝑣 = 𝑡 → {𝑣, 𝑤} = {𝑡, 𝑤}) |
45 | 44 | eleq1d 2672 |
. . . . . 6
⊢ (𝑣 = 𝑡 → ({𝑣, 𝑤} ∈ ran 𝐸 ↔ {𝑡, 𝑤} ∈ ran 𝐸)) |
46 | 43, 45 | raleqbidv 3129 |
. . . . 5
⊢ (𝑣 = 𝑡 → (∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸)) |
47 | 46 | cbvrexv 3148 |
. . . 4
⊢
(∃𝑣 ∈
𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸) |
48 | 47 | a1i 11 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → (∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸)) |
49 | 40, 41, 48 | 3orbi123d 1390 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → ((∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸) ↔ (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑡 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑡}){𝑡, 𝑤} ∈ ran 𝐸))) |
50 | 39, 49 | mpbird 246 |
1
⊢ (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) |