Step | Hyp | Ref
| Expression |
1 | | nbgraf1o.n |
. . . 4
⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑈) |
2 | | nbgraf1o.i |
. . . 4
⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)} |
3 | | nbgraf1o.f |
. . . 4
⊢ 𝐹 = (𝑛 ∈ 𝑁 ↦ (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛})) |
4 | 1, 2, 3 | nbgraf1olem2 25971 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → 𝐹:𝑁⟶𝐼) |
5 | | ffn 5958 |
. . 3
⊢ (𝐹:𝑁⟶𝐼 → 𝐹 Fn 𝑁) |
6 | 4, 5 | syl 17 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → 𝐹 Fn 𝑁) |
7 | 1, 2, 3 | nbgraf1olem3 25972 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝑛 ∈ 𝑁) → (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) = (◡𝐸‘{𝑈, 𝑛})) |
8 | 7 | 3expa 1257 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) = (◡𝐸‘{𝑈, 𝑛})) |
9 | 8 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → (𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) ↔ 𝑗 = (◡𝐸‘{𝑈, 𝑛}))) |
10 | | usgraf1o 25887 |
. . . . . . . . . . . . . 14
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
11 | 10 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
12 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
13 | | nbgraeledg 25959 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 USGrph 𝐸 → (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) ↔ {𝑛, 𝑈} ∈ ran 𝐸)) |
14 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑛, 𝑈} = {𝑈, 𝑛} |
15 | 14 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑛, 𝑈} ∈ ran 𝐸 ↔ {𝑈, 𝑛} ∈ ran 𝐸) |
16 | 13, 15 | syl6bb 275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 USGrph 𝐸 → (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) ↔ {𝑈, 𝑛} ∈ ran 𝐸)) |
17 | 16 | biimpcd 238 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) → (𝑉 USGrph 𝐸 → {𝑈, 𝑛} ∈ ran 𝐸)) |
18 | 17 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) → (𝑈 ∈ 𝑉 → (𝑉 USGrph 𝐸 → {𝑈, 𝑛} ∈ ran 𝐸))) |
19 | 18, 1 | eleq2s 2706 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑁 → (𝑈 ∈ 𝑉 → (𝑉 USGrph 𝐸 → {𝑈, 𝑛} ∈ ran 𝐸))) |
20 | 19 | com13 86 |
. . . . . . . . . . . . 13
⊢ (𝑉 USGrph 𝐸 → (𝑈 ∈ 𝑉 → (𝑛 ∈ 𝑁 → {𝑈, 𝑛} ∈ ran 𝐸))) |
21 | 20 | imp31 447 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → {𝑈, 𝑛} ∈ ran 𝐸) |
22 | | f1ocnvdm 6440 |
. . . . . . . . . . . 12
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝑈, 𝑛} ∈ ran 𝐸) → (◡𝐸‘{𝑈, 𝑛}) ∈ dom 𝐸) |
23 | 12, 21, 22 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → (◡𝐸‘{𝑈, 𝑛}) ∈ dom 𝐸) |
24 | | prid1g 4239 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ {𝑈, 𝑛}) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → 𝑈 ∈ {𝑈, 𝑛}) |
26 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → 𝑈 ∈ {𝑈, 𝑛}) |
27 | 1 | eleq2i 2680 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑁 ↔ 𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈)) |
28 | | nbgracnvfv 25969 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈)) → (𝐸‘(◡𝐸‘{𝑈, 𝑛})) = {𝑈, 𝑛}) |
29 | 27, 28 | sylan2b 491 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑛 ∈ 𝑁) → (𝐸‘(◡𝐸‘{𝑈, 𝑛})) = {𝑈, 𝑛}) |
30 | 29 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → (𝐸‘(◡𝐸‘{𝑈, 𝑛})) = {𝑈, 𝑛}) |
31 | 26, 30 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → 𝑈 ∈ (𝐸‘(◡𝐸‘{𝑈, 𝑛}))) |
32 | 23, 31 | jca 553 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → ((◡𝐸‘{𝑈, 𝑛}) ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘(◡𝐸‘{𝑈, 𝑛})))) |
33 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑗 = (◡𝐸‘{𝑈, 𝑛}) → (𝑗 ∈ dom 𝐸 ↔ (◡𝐸‘{𝑈, 𝑛}) ∈ dom 𝐸)) |
34 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑗 = (◡𝐸‘{𝑈, 𝑛}) → (𝐸‘𝑗) = (𝐸‘(◡𝐸‘{𝑈, 𝑛}))) |
35 | 34 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑗 = (◡𝐸‘{𝑈, 𝑛}) → (𝑈 ∈ (𝐸‘𝑗) ↔ 𝑈 ∈ (𝐸‘(◡𝐸‘{𝑈, 𝑛})))) |
36 | 33, 35 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑗 = (◡𝐸‘{𝑈, 𝑛}) → ((𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗)) ↔ ((◡𝐸‘{𝑈, 𝑛}) ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘(◡𝐸‘{𝑈, 𝑛}))))) |
37 | 32, 36 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → (𝑗 = (◡𝐸‘{𝑈, 𝑛}) → (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗)))) |
38 | 9, 37 | sylbid 229 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑛 ∈ 𝑁) → (𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) → (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗)))) |
39 | 38 | rexlimdva 3013 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (∃𝑛 ∈ 𝑁 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) → (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗)))) |
40 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → 𝑉 USGrph 𝐸) |
41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) → 𝑉 USGrph 𝐸) |
42 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗)) → 𝑗 ∈ dom 𝐸) |
43 | 42 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) → 𝑗 ∈ dom 𝐸) |
44 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) → 𝑈 ∈ (𝐸‘𝑗)) |
45 | | usgraedg4 25916 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗)) → ∃𝑛 ∈ 𝑉 (𝐸‘𝑗) = {𝑈, 𝑛}) |
46 | 41, 43, 44, 45 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) → ∃𝑛 ∈ 𝑉 (𝐸‘𝑗) = {𝑈, 𝑛}) |
47 | | usgrafun 25878 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
48 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
𝐸 ∧ 𝑗 ∈ dom 𝐸) → (𝐸‘𝑗) ∈ ran 𝐸) |
49 | 48 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Fun
𝐸 → (𝑗 ∈ dom 𝐸 → (𝐸‘𝑗) ∈ ran 𝐸)) |
50 | 47, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 USGrph 𝐸 → (𝑗 ∈ dom 𝐸 → (𝐸‘𝑗) ∈ ran 𝐸)) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (𝑗 ∈ dom 𝐸 → (𝐸‘𝑗) ∈ ran 𝐸)) |
52 | 51 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ dom 𝐸 → ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (𝐸‘𝑗) ∈ ran 𝐸)) |
53 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗)) → ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (𝐸‘𝑗) ∈ ran 𝐸)) |
54 | 53 | impcom 445 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) → (𝐸‘𝑗) ∈ ran 𝐸) |
55 | 54 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → (𝐸‘𝑗) ∈ ran 𝐸) |
56 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑈, 𝑛} = (𝐸‘𝑗) → {𝑈, 𝑛} = (𝐸‘𝑗)) |
57 | 56 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘𝑗) = {𝑈, 𝑛} → {𝑈, 𝑛} = (𝐸‘𝑗)) |
58 | 14, 57 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘𝑗) = {𝑈, 𝑛} → {𝑛, 𝑈} = (𝐸‘𝑗)) |
59 | 58 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸‘𝑗) = {𝑈, 𝑛} → ({𝑛, 𝑈} ∈ ran 𝐸 ↔ (𝐸‘𝑗) ∈ ran 𝐸)) |
60 | 59 | ad2antll 761 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → ({𝑛, 𝑈} ∈ ran 𝐸 ↔ (𝐸‘𝑗) ∈ ran 𝐸)) |
61 | 55, 60 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → {𝑛, 𝑈} ∈ ran 𝐸) |
62 | 13 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) ↔ {𝑛, 𝑈} ∈ ran 𝐸)) |
63 | 61, 62 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → 𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈)) |
64 | 63, 27 | sylibr 223 |
. . . . . . . . . . . 12
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → 𝑛 ∈ 𝑁) |
65 | | f1ocnvfv1 6432 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ 𝑗 ∈ dom 𝐸) → (◡𝐸‘(𝐸‘𝑗)) = 𝑗) |
66 | 11, 42, 65 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) → (◡𝐸‘(𝐸‘𝑗)) = 𝑗) |
67 | 66 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → (◡𝐸‘(𝐸‘𝑗)) = 𝑗) |
68 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑈, 𝑛} = (𝐸‘𝑗) → (◡𝐸‘{𝑈, 𝑛}) = (◡𝐸‘(𝐸‘𝑗))) |
69 | 68 | eqcoms 2618 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸‘𝑗) = {𝑈, 𝑛} → (◡𝐸‘{𝑈, 𝑛}) = (◡𝐸‘(𝐸‘𝑗))) |
70 | 69 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸‘𝑗) = {𝑈, 𝑛} → ((◡𝐸‘{𝑈, 𝑛}) = 𝑗 ↔ (◡𝐸‘(𝐸‘𝑗)) = 𝑗)) |
71 | 70 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → ((◡𝐸‘{𝑈, 𝑛}) = 𝑗 ↔ (◡𝐸‘(𝐸‘𝑗)) = 𝑗)) |
72 | 67, 71 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → (◡𝐸‘{𝑈, 𝑛}) = 𝑗) |
73 | | eqcom 2617 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) ↔ (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) = 𝑗) |
74 | | simplll 794 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → 𝑉 USGrph 𝐸) |
75 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → 𝑈 ∈ 𝑉) |
76 | 7 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝑛 ∈ 𝑁) → ((℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) = 𝑗 ↔ (◡𝐸‘{𝑈, 𝑛}) = 𝑗)) |
77 | 74, 75, 64, 76 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → ((℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) = 𝑗 ↔ (◡𝐸‘{𝑈, 𝑛}) = 𝑗)) |
78 | 73, 77 | syl5bb 271 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → (𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) ↔ (◡𝐸‘{𝑈, 𝑛}) = 𝑗)) |
79 | 72, 78 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛})) |
80 | 64, 79 | jca 553 |
. . . . . . . . . . 11
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) ∧ (𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛})) → (𝑛 ∈ 𝑁 ∧ 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}))) |
81 | 80 | ex 449 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) → ((𝑛 ∈ 𝑉 ∧ (𝐸‘𝑗) = {𝑈, 𝑛}) → (𝑛 ∈ 𝑁 ∧ 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛})))) |
82 | 81 | reximdv2 2997 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) → (∃𝑛 ∈ 𝑉 (𝐸‘𝑗) = {𝑈, 𝑛} → ∃𝑛 ∈ 𝑁 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}))) |
83 | 46, 82 | mpd 15 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))) → ∃𝑛 ∈ 𝑁 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛})) |
84 | 83 | ex 449 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗)) → ∃𝑛 ∈ 𝑁 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}))) |
85 | 39, 84 | impbid 201 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (∃𝑛 ∈ 𝑁 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛}) ↔ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗)))) |
86 | 85 | abbidv 2728 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → {𝑗 ∣ ∃𝑛 ∈ 𝑁 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛})} = {𝑗 ∣ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))}) |
87 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑗 = 𝑖 → (𝑗 ∈ dom 𝐸 ↔ 𝑖 ∈ dom 𝐸)) |
88 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑗 = 𝑖 → (𝐸‘𝑗) = (𝐸‘𝑖)) |
89 | 88 | eleq2d 2673 |
. . . . . . 7
⊢ (𝑗 = 𝑖 → (𝑈 ∈ (𝐸‘𝑗) ↔ 𝑈 ∈ (𝐸‘𝑖))) |
90 | 87, 89 | anbi12d 743 |
. . . . . 6
⊢ (𝑗 = 𝑖 → ((𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗)) ↔ (𝑖 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑖)))) |
91 | 90 | cbvabv 2734 |
. . . . 5
⊢ {𝑗 ∣ (𝑗 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑗))} = {𝑖 ∣ (𝑖 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑖))} |
92 | 86, 91 | syl6eq 2660 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → {𝑗 ∣ ∃𝑛 ∈ 𝑁 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛})} = {𝑖 ∣ (𝑖 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑖))}) |
93 | | df-rab 2905 |
. . . 4
⊢ {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)} = {𝑖 ∣ (𝑖 ∈ dom 𝐸 ∧ 𝑈 ∈ (𝐸‘𝑖))} |
94 | 92, 93 | syl6eqr 2662 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → {𝑗 ∣ ∃𝑛 ∈ 𝑁 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛})} = {𝑖 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑖)}) |
95 | 3 | rnmpt 5292 |
. . 3
⊢ ran 𝐹 = {𝑗 ∣ ∃𝑛 ∈ 𝑁 𝑗 = (℩𝑖 ∈ 𝐼 (𝐸‘𝑖) = {𝑈, 𝑛})} |
96 | 94, 95, 2 | 3eqtr4g 2669 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ran 𝐹 = 𝐼) |
97 | 1, 2, 3 | nbgraf1olem4 25973 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝑥 ∈ 𝑁) → (𝐹‘𝑥) = (◡𝐸‘{𝑈, 𝑥})) |
98 | 97 | 3expa 1257 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) → (𝐹‘𝑥) = (◡𝐸‘{𝑈, 𝑥})) |
99 | 98 | adantr 480 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → (𝐹‘𝑥) = (◡𝐸‘{𝑈, 𝑥})) |
100 | | simplll 794 |
. . . . . . 7
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → 𝑉 USGrph 𝐸) |
101 | | simpllr 795 |
. . . . . . 7
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → 𝑈 ∈ 𝑉) |
102 | | simpr 476 |
. . . . . . 7
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → 𝑦 ∈ 𝑁) |
103 | 1, 2, 3 | nbgraf1olem4 25973 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝑦 ∈ 𝑁) → (𝐹‘𝑦) = (◡𝐸‘{𝑈, 𝑦})) |
104 | 100, 101,
102, 103 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → (𝐹‘𝑦) = (◡𝐸‘{𝑈, 𝑦})) |
105 | 99, 104 | eqeq12d 2625 |
. . . . 5
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (◡𝐸‘{𝑈, 𝑥}) = (◡𝐸‘{𝑈, 𝑦}))) |
106 | | usgraf1 25889 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→ran 𝐸) |
107 | 106 | ad3antrrr 762 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → 𝐸:dom 𝐸–1-1→ran 𝐸) |
108 | 1 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑁 ↔ 𝑥 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈)) |
109 | | nbgraeledg 25959 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → (𝑥 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) ↔ {𝑥, 𝑈} ∈ ran 𝐸)) |
110 | | prcom 4211 |
. . . . . . . . . . . . 13
⊢ {𝑥, 𝑈} = {𝑈, 𝑥} |
111 | 110 | eleq1i 2679 |
. . . . . . . . . . . 12
⊢ ({𝑥, 𝑈} ∈ ran 𝐸 ↔ {𝑈, 𝑥} ∈ ran 𝐸) |
112 | 109, 111 | syl6bb 275 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → (𝑥 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) ↔ {𝑈, 𝑥} ∈ ran 𝐸)) |
113 | 112 | biimpd 218 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑥 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) → {𝑈, 𝑥} ∈ ran 𝐸)) |
114 | 108, 113 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑥 ∈ 𝑁 → {𝑈, 𝑥} ∈ ran 𝐸)) |
115 | 114 | adantr 480 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (𝑥 ∈ 𝑁 → {𝑈, 𝑥} ∈ ran 𝐸)) |
116 | 115 | imp 444 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) → {𝑈, 𝑥} ∈ ran 𝐸) |
117 | 116 | adantr 480 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → {𝑈, 𝑥} ∈ ran 𝐸) |
118 | 1 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑁 ↔ 𝑦 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈)) |
119 | | nbgraeledg 25959 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → (𝑦 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) ↔ {𝑦, 𝑈} ∈ ran 𝐸)) |
120 | | prcom 4211 |
. . . . . . . . . . . . 13
⊢ {𝑦, 𝑈} = {𝑈, 𝑦} |
121 | 120 | eleq1i 2679 |
. . . . . . . . . . . 12
⊢ ({𝑦, 𝑈} ∈ ran 𝐸 ↔ {𝑈, 𝑦} ∈ ran 𝐸) |
122 | 119, 121 | syl6bb 275 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → (𝑦 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) ↔ {𝑈, 𝑦} ∈ ran 𝐸)) |
123 | 122 | biimpd 218 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑦 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑈) → {𝑈, 𝑦} ∈ ran 𝐸)) |
124 | 118, 123 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑦 ∈ 𝑁 → {𝑈, 𝑦} ∈ ran 𝐸)) |
125 | 124 | adantr 480 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (𝑦 ∈ 𝑁 → {𝑈, 𝑦} ∈ ran 𝐸)) |
126 | 125 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) → (𝑦 ∈ 𝑁 → {𝑈, 𝑦} ∈ ran 𝐸)) |
127 | 126 | imp 444 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → {𝑈, 𝑦} ∈ ran 𝐸) |
128 | | f1ocnvfvrneq 6441 |
. . . . . . 7
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ({𝑈, 𝑥} ∈ ran 𝐸 ∧ {𝑈, 𝑦} ∈ ran 𝐸)) → ((◡𝐸‘{𝑈, 𝑥}) = (◡𝐸‘{𝑈, 𝑦}) → {𝑈, 𝑥} = {𝑈, 𝑦})) |
129 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
130 | | vex 3176 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
131 | 129, 130 | preqr2 4321 |
. . . . . . 7
⊢ ({𝑈, 𝑥} = {𝑈, 𝑦} → 𝑥 = 𝑦) |
132 | 128, 131 | syl6 34 |
. . . . . 6
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ({𝑈, 𝑥} ∈ ran 𝐸 ∧ {𝑈, 𝑦} ∈ ran 𝐸)) → ((◡𝐸‘{𝑈, 𝑥}) = (◡𝐸‘{𝑈, 𝑦}) → 𝑥 = 𝑦)) |
133 | 107, 117,
127, 132 | syl12anc 1316 |
. . . . 5
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → ((◡𝐸‘{𝑈, 𝑥}) = (◡𝐸‘{𝑈, 𝑦}) → 𝑥 = 𝑦)) |
134 | 105, 133 | sylbid 229 |
. . . 4
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) ∧ 𝑦 ∈ 𝑁) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
135 | 134 | ralrimiva 2949 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) ∧ 𝑥 ∈ 𝑁) → ∀𝑦 ∈ 𝑁 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
136 | 135 | ralrimiva 2949 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
137 | | dff1o6 6431 |
. 2
⊢ (𝐹:𝑁–1-1-onto→𝐼 ↔ (𝐹 Fn 𝑁 ∧ ran 𝐹 = 𝐼 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
138 | 6, 96, 136, 137 | syl3anbrc 1239 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → 𝐹:𝑁–1-1-onto→𝐼) |