Step | Hyp | Ref
| Expression |
1 | | nbgraf1o.n |
. . . . . 6
⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑈) |
2 | 1 | eleq2i 2680 |
. . . . 5
⊢ (𝑀 ∈ 𝑁 ↔ 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈)) |
3 | | usgrav 25867 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
5 | | nbgrael 25955 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) ↔ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸))) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) ↔ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸))) |
7 | 2, 6 | syl5bb 271 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (𝑀 ∈ 𝑁 ↔ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸))) |
8 | | usgrafun 25878 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
9 | | elrnrexdm 6271 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝐸 → ({𝑈, 𝑀} ∈ ran 𝐸 → ∃𝑖 ∈ dom 𝐸{𝑈, 𝑀} = (𝐸‘𝑖))) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 USGrph 𝐸 → ({𝑈, 𝑀} ∈ ran 𝐸 → ∃𝑖 ∈ dom 𝐸{𝑈, 𝑀} = (𝐸‘𝑖))) |
11 | 10 | com12 32 |
. . . . . . . . . . . . . 14
⊢ ({𝑈, 𝑀} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → ∃𝑖 ∈ dom 𝐸{𝑈, 𝑀} = (𝐸‘𝑖))) |
12 | 11 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸) → (𝑉 USGrph 𝐸 → ∃𝑖 ∈ dom 𝐸{𝑈, 𝑀} = (𝐸‘𝑖))) |
13 | 12 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → ((𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸) → ∃𝑖 ∈ dom 𝐸{𝑈, 𝑀} = (𝐸‘𝑖))) |
14 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸) → ∃𝑖 ∈ dom 𝐸{𝑈, 𝑀} = (𝐸‘𝑖))) |
15 | 14 | imp 444 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸)) → ∃𝑖 ∈ dom 𝐸{𝑈, 𝑀} = (𝐸‘𝑖)) |
16 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ ((𝐸‘𝑖) = {𝑈, 𝑀} ↔ {𝑈, 𝑀} = (𝐸‘𝑖)) |
17 | 16 | rexbii 3023 |
. . . . . . . . . 10
⊢
(∃𝑖 ∈ dom
𝐸(𝐸‘𝑖) = {𝑈, 𝑀} ↔ ∃𝑖 ∈ dom 𝐸{𝑈, 𝑀} = (𝐸‘𝑖)) |
18 | 15, 17 | sylibr 223 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸)) → ∃𝑖 ∈ dom 𝐸(𝐸‘𝑖) = {𝑈, 𝑀}) |
19 | | prid1g 4239 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ {𝑈, 𝑀}) |
20 | | eleq2 2677 |
. . . . . . . . . . . . . 14
⊢ ((𝐸‘𝑖) = {𝑈, 𝑀} → (𝑈 ∈ (𝐸‘𝑖) ↔ 𝑈 ∈ {𝑈, 𝑀})) |
21 | 19, 20 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ 𝑉 → ((𝐸‘𝑖) = {𝑈, 𝑀} → 𝑈 ∈ (𝐸‘𝑖))) |
22 | 21 | pm4.71rd 665 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ 𝑉 → ((𝐸‘𝑖) = {𝑈, 𝑀} ↔ (𝑈 ∈ (𝐸‘𝑖) ∧ (𝐸‘𝑖) = {𝑈, 𝑀}))) |
23 | 22 | bicomd 212 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ 𝑉 → ((𝑈 ∈ (𝐸‘𝑖) ∧ (𝐸‘𝑖) = {𝑈, 𝑀}) ↔ (𝐸‘𝑖) = {𝑈, 𝑀})) |
24 | 23 | rexbidv 3034 |
. . . . . . . . . 10
⊢ (𝑈 ∈ 𝑉 → (∃𝑖 ∈ dom 𝐸(𝑈 ∈ (𝐸‘𝑖) ∧ (𝐸‘𝑖) = {𝑈, 𝑀}) ↔ ∃𝑖 ∈ dom 𝐸(𝐸‘𝑖) = {𝑈, 𝑀})) |
25 | 24 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸)) → (∃𝑖 ∈ dom 𝐸(𝑈 ∈ (𝐸‘𝑖) ∧ (𝐸‘𝑖) = {𝑈, 𝑀}) ↔ ∃𝑖 ∈ dom 𝐸(𝐸‘𝑖) = {𝑈, 𝑀})) |
26 | 18, 25 | mpbird 246 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸)) → ∃𝑖 ∈ dom 𝐸(𝑈 ∈ (𝐸‘𝑖) ∧ (𝐸‘𝑖) = {𝑈, 𝑀})) |
27 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑖 → (𝐸‘𝑥) = (𝐸‘𝑖)) |
28 | 27 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑥 = 𝑖 → (𝑈 ∈ (𝐸‘𝑥) ↔ 𝑈 ∈ (𝐸‘𝑖))) |
29 | 28 | rexrab 3337 |
. . . . . . . 8
⊢
(∃𝑖 ∈
{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} (𝐸‘𝑖) = {𝑈, 𝑀} ↔ ∃𝑖 ∈ dom 𝐸(𝑈 ∈ (𝐸‘𝑖) ∧ (𝐸‘𝑖) = {𝑈, 𝑀})) |
30 | 26, 29 | sylibr 223 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸)) → ∃𝑖 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} (𝐸‘𝑖) = {𝑈, 𝑀}) |
31 | | nbgraf1o.i |
. . . . . . . . 9
⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)} |
32 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → (𝐸‘𝑖) = (𝐸‘𝑥)) |
33 | 32 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑥 → (𝑈 ∈ (𝐸‘𝑖) ↔ 𝑈 ∈ (𝐸‘𝑥))) |
34 | 33 | cbvrabv 3172 |
. . . . . . . . 9
⊢ {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)} = {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} |
35 | 31, 34 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐼 = {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} |
36 | 35 | rexeqi 3120 |
. . . . . . 7
⊢
(∃𝑖 ∈
𝐼 (𝐸‘𝑖) = {𝑈, 𝑀} ↔ ∃𝑖 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} (𝐸‘𝑖) = {𝑈, 𝑀}) |
37 | 30, 36 | sylibr 223 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸)) → ∃𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑀}) |
38 | | usgraf1o 25887 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
39 | | dff1o6 6431 |
. . . . . . . . . 10
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 ↔ (𝐸 Fn dom 𝐸 ∧ ran 𝐸 = ran 𝐸 ∧ ∀𝑖 ∈ dom 𝐸∀𝑗 ∈ dom 𝐸((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗))) |
40 | | ssrab2 3650 |
. . . . . . . . . . . . . 14
⊢ {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)} ⊆ dom 𝐸 |
41 | 31, 40 | eqsstri 3598 |
. . . . . . . . . . . . 13
⊢ 𝐼 ⊆ dom 𝐸 |
42 | | ssralv 3629 |
. . . . . . . . . . . . 13
⊢ (𝐼 ⊆ dom 𝐸 → (∀𝑖 ∈ dom 𝐸∀𝑗 ∈ dom 𝐸((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ dom 𝐸((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗))) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
dom 𝐸∀𝑗 ∈ dom 𝐸((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ dom 𝐸((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗)) |
44 | | ssralv 3629 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ⊆ dom 𝐸 → (∀𝑗 ∈ dom 𝐸((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗) → ∀𝑗 ∈ 𝐼 ((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗))) |
45 | 41, 44 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∀𝑗 ∈
dom 𝐸((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗) → ∀𝑗 ∈ 𝐼 ((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗)) |
46 | 45 | ralimi 2936 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
𝐼 ∀𝑗 ∈ dom 𝐸((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 ((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗)) |
47 | | eqtr3 2631 |
. . . . . . . . . . . . . . 15
⊢ (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → (𝐸‘𝑖) = (𝐸‘𝑗)) |
48 | 47 | imim1i 61 |
. . . . . . . . . . . . . 14
⊢ (((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗) → (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)) |
49 | 48 | ralimi 2936 |
. . . . . . . . . . . . 13
⊢
(∀𝑗 ∈
𝐼 ((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗) → ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)) |
50 | 49 | ralimi 2936 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
𝐼 ∀𝑗 ∈ 𝐼 ((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)) |
51 | 43, 46, 50 | 3syl 18 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
dom 𝐸∀𝑗 ∈ dom 𝐸((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)) |
52 | 51 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝐸 Fn dom 𝐸 ∧ ran 𝐸 = ran 𝐸 ∧ ∀𝑖 ∈ dom 𝐸∀𝑗 ∈ dom 𝐸((𝐸‘𝑖) = (𝐸‘𝑗) → 𝑖 = 𝑗)) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)) |
53 | 39, 52 | sylbi 206 |
. . . . . . . . 9
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)) |
54 | 38, 53 | syl 17 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)) |
55 | 54 | adantr 480 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)) |
56 | 55 | adantr 480 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸)) → ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)) |
57 | 37, 56 | jca 553 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸)) → (∃𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑀} ∧ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗))) |
58 | 57 | ex 449 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((𝑈 ∈ 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ {𝑈, 𝑀} ∈ ran 𝐸) → (∃𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑀} ∧ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)))) |
59 | 7, 58 | sylbid 229 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (𝑀 ∈ 𝑁 → (∃𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑀} ∧ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗)))) |
60 | 59 | imp 444 |
. 2
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑀 ∈ 𝑁) → (∃𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑀} ∧ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗))) |
61 | | fveq2 6103 |
. . . 4
⊢ (𝑖 = 𝑗 → (𝐸‘𝑖) = (𝐸‘𝑗)) |
62 | 61 | eqeq1d 2612 |
. . 3
⊢ (𝑖 = 𝑗 → ((𝐸‘𝑖) = {𝑈, 𝑀} ↔ (𝐸‘𝑗) = {𝑈, 𝑀})) |
63 | 62 | reu4 3367 |
. 2
⊢
(∃!𝑖 ∈
𝐼 (𝐸‘𝑖) = {𝑈, 𝑀} ↔ (∃𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑀} ∧ ∀𝑖 ∈ 𝐼 ∀𝑗 ∈ 𝐼 (((𝐸‘𝑖) = {𝑈, 𝑀} ∧ (𝐸‘𝑗) = {𝑈, 𝑀}) → 𝑖 = 𝑗))) |
64 | 60, 63 | sylibr 223 |
1
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑀 ∈ 𝑁) → ∃!𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑀}) |