Step | Hyp | Ref
| Expression |
1 | | usgraf1 25889 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→ran 𝐸) |
2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → 𝐸:dom 𝐸–1-1→ran 𝐸) |
3 | | ssrab2 3650 |
. . . . 5
⊢ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ⊆ dom 𝐸 |
4 | | f1ssres 6021 |
. . . . 5
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ⊆ dom 𝐸) → (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}):{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}–1-1→ran 𝐸) |
5 | 2, 3, 4 | sylancl 693 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}):{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}–1-1→ran 𝐸) |
6 | | usgrafis.f |
. . . . . 6
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)})) |
8 | 6 | dmeqi 5247 |
. . . . . 6
⊢ dom 𝐹 = dom (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
9 | 3 | a1i 11 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ⊆ dom 𝐸) |
10 | | ssdmres 5340 |
. . . . . . 7
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ⊆ dom 𝐸 ↔ dom (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
11 | 9, 10 | sylib 207 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → dom (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
12 | 8, 11 | syl5eq 2656 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → dom 𝐹 = {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
13 | | eqidd 2611 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ran 𝐸 = ran 𝐸) |
14 | 7, 12, 13 | f1eq123d 6044 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝐹:dom 𝐹–1-1→ran 𝐸 ↔ (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}):{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}–1-1→ran 𝐸)) |
15 | 5, 14 | mpbird 246 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → 𝐹:dom 𝐹–1-1→ran 𝐸) |
16 | 6 | rneqi 5273 |
. . . . 5
⊢ ran 𝐹 = ran (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
17 | | df-ima 5051 |
. . . . 5
⊢ (𝐸 “ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) = ran (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
18 | 16, 17 | eqtr4i 2635 |
. . . 4
⊢ ran 𝐹 = (𝐸 “ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
19 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝑁 = 𝑁) |
20 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐸‘𝑥) = (𝐸‘𝑦)) |
21 | 19, 20 | neleq12d 2887 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑁 ∉ (𝐸‘𝑥) ↔ 𝑁 ∉ (𝐸‘𝑦))) |
22 | 21 | elrab 3331 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ↔ (𝑦 ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘𝑦))) |
23 | | usgraf0 25877 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}) |
24 | | f1f 6014 |
. . . . . . . . . . . . . . 15
⊢ (𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} → 𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}) |
25 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ∧ 𝑦 ∈ dom 𝐸) → (𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}) |
26 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = (𝐸‘𝑦) → (#‘𝑒) = (#‘(𝐸‘𝑦))) |
27 | 26 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝐸‘𝑦) → ((#‘𝑒) = 2 ↔ (#‘(𝐸‘𝑦)) = 2)) |
28 | 27 | elrab 3331 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ↔ ((𝐸‘𝑦) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑦)) = 2)) |
29 | | df-nel 2783 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∉ (𝐸‘𝑦) ↔ ¬ 𝑁 ∈ (𝐸‘𝑦)) |
30 | 29 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∉ (𝐸‘𝑦) → ¬ 𝑁 ∈ (𝐸‘𝑦)) |
31 | 30 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐸‘𝑦) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑦)) = 2) ∧ 𝑁 ∉ (𝐸‘𝑦)) ∧ 𝑁 ∈ 𝑉) → ¬ 𝑁 ∈ (𝐸‘𝑦)) |
32 | | disjsn 4192 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐸‘𝑦) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (𝐸‘𝑦)) |
33 | 31, 32 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐸‘𝑦) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑦)) = 2) ∧ 𝑁 ∉ (𝐸‘𝑦)) ∧ 𝑁 ∈ 𝑉) → ((𝐸‘𝑦) ∩ {𝑁}) = ∅) |
34 | | elpwi 4117 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐸‘𝑦) ∈ 𝒫 𝑉 → (𝐸‘𝑦) ⊆ 𝑉) |
35 | 34 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐸‘𝑦) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑦)) = 2) ∧ 𝑁 ∉ (𝐸‘𝑦)) ∧ 𝑁 ∈ 𝑉) → (𝐸‘𝑦) ⊆ 𝑉) |
36 | | reldisj 3972 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸‘𝑦) ⊆ 𝑉 → (((𝐸‘𝑦) ∩ {𝑁}) = ∅ ↔ (𝐸‘𝑦) ⊆ (𝑉 ∖ {𝑁}))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐸‘𝑦) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑦)) = 2) ∧ 𝑁 ∉ (𝐸‘𝑦)) ∧ 𝑁 ∈ 𝑉) → (((𝐸‘𝑦) ∩ {𝑁}) = ∅ ↔ (𝐸‘𝑦) ⊆ (𝑉 ∖ {𝑁}))) |
38 | 33, 37 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐸‘𝑦) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑦)) = 2) ∧ 𝑁 ∉ (𝐸‘𝑦)) ∧ 𝑁 ∈ 𝑉) → (𝐸‘𝑦) ⊆ (𝑉 ∖ {𝑁})) |
39 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐸‘𝑦) ∈ V |
40 | 39 | elpw 4114 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ↔ (𝐸‘𝑦) ⊆ (𝑉 ∖ {𝑁})) |
41 | 38, 40 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐸‘𝑦) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑦)) = 2) ∧ 𝑁 ∉ (𝐸‘𝑦)) ∧ 𝑁 ∈ 𝑉) → (𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁})) |
42 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐸‘𝑦) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑦)) = 2) ∧ 𝑁 ∉ (𝐸‘𝑦)) ∧ 𝑁 ∈ 𝑉) → (#‘(𝐸‘𝑦)) = 2) |
43 | 41, 42 | jca 553 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐸‘𝑦) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑦)) = 2) ∧ 𝑁 ∉ (𝐸‘𝑦)) ∧ 𝑁 ∈ 𝑉) → ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (#‘(𝐸‘𝑦)) = 2)) |
44 | 43 | exp31 628 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐸‘𝑦) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑦)) = 2) → (𝑁 ∉ (𝐸‘𝑦) → (𝑁 ∈ 𝑉 → ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (#‘(𝐸‘𝑦)) = 2)))) |
45 | 28, 44 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} → (𝑁 ∉ (𝐸‘𝑦) → (𝑁 ∈ 𝑉 → ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (#‘(𝐸‘𝑦)) = 2)))) |
46 | 25, 45 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ∧ 𝑦 ∈ dom 𝐸) → (𝑁 ∉ (𝐸‘𝑦) → (𝑁 ∈ 𝑉 → ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (#‘(𝐸‘𝑦)) = 2)))) |
47 | 46 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} → (𝑦 ∈ dom 𝐸 → (𝑁 ∉ (𝐸‘𝑦) → (𝑁 ∈ 𝑉 → ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (#‘(𝐸‘𝑦)) = 2))))) |
48 | 24, 47 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} → (𝑦 ∈ dom 𝐸 → (𝑁 ∉ (𝐸‘𝑦) → (𝑁 ∈ 𝑉 → ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (#‘(𝐸‘𝑦)) = 2))))) |
49 | 48 | impd 446 |
. . . . . . . . . . . . 13
⊢ (𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} → ((𝑦 ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘𝑦)) → (𝑁 ∈ 𝑉 → ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (#‘(𝐸‘𝑦)) = 2)))) |
50 | 49 | com23 84 |
. . . . . . . . . . . 12
⊢ (𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} → (𝑁 ∈ 𝑉 → ((𝑦 ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘𝑦)) → ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (#‘(𝐸‘𝑦)) = 2)))) |
51 | 50 | imp31 447 |
. . . . . . . . . . 11
⊢ (((𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘𝑦))) → ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (#‘(𝐸‘𝑦)) = 2)) |
52 | 27 | elrab 3331 |
. . . . . . . . . . 11
⊢ ((𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2} ↔ ((𝐸‘𝑦) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (#‘(𝐸‘𝑦)) = 2)) |
53 | 51, 52 | sylibr 223 |
. . . . . . . . . 10
⊢ (((𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ∧ 𝑁 ∈ 𝑉) ∧ (𝑦 ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘𝑦))) → (𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2}) |
54 | 53 | exp31 628 |
. . . . . . . . 9
⊢ (𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} → (𝑁 ∈ 𝑉 → ((𝑦 ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘𝑦)) → (𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2}))) |
55 | 23, 54 | syl 17 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → (𝑁 ∈ 𝑉 → ((𝑦 ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘𝑦)) → (𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2}))) |
56 | 55 | imp 444 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝑦 ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘𝑦)) → (𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2})) |
57 | 22, 56 | syl5bi 231 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} → (𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2})) |
58 | 57 | ralrimiv 2948 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ∀𝑦 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} (𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2}) |
59 | | usgrafun 25878 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
60 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ⊆ dom 𝐸) |
61 | 59, 60 | jca 553 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → (Fun 𝐸 ∧ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ⊆ dom 𝐸)) |
62 | 61 | adantr 480 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (Fun 𝐸 ∧ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ⊆ dom 𝐸)) |
63 | | funimass4 6157 |
. . . . . 6
⊢ ((Fun
𝐸 ∧ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ⊆ dom 𝐸) → ((𝐸 “ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ⊆ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2} ↔ ∀𝑦 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} (𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2})) |
64 | 62, 63 | syl 17 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝐸 “ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ⊆ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2} ↔ ∀𝑦 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} (𝐸‘𝑦) ∈ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2})) |
65 | 58, 64 | mpbird 246 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝐸 “ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ⊆ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2}) |
66 | 18, 65 | syl5eqss 3612 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ran 𝐹 ⊆ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2}) |
67 | | f1ssr 6020 |
. . 3
⊢ ((𝐹:dom 𝐹–1-1→ran 𝐸 ∧ ran 𝐹 ⊆ {𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2}) → 𝐹:dom 𝐹–1-1→{𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2}) |
68 | 15, 66, 67 | syl2anc 691 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → 𝐹:dom 𝐹–1-1→{𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2}) |
69 | | usgrav 25867 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
70 | | difexg 4735 |
. . . . 5
⊢ (𝑉 ∈ V → (𝑉 ∖ {𝑁}) ∈ V) |
71 | | resexg 5362 |
. . . . . 6
⊢ (𝐸 ∈ V → (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ∈ V) |
72 | 6, 71 | syl5eqel 2692 |
. . . . 5
⊢ (𝐸 ∈ V → 𝐹 ∈ V) |
73 | | isusgra0 25876 |
. . . . 5
⊢ (((𝑉 ∖ {𝑁}) ∈ V ∧ 𝐹 ∈ V) → ((𝑉 ∖ {𝑁}) USGrph 𝐹 ↔ 𝐹:dom 𝐹–1-1→{𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2})) |
74 | 70, 72, 73 | syl2an 493 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑉 ∖ {𝑁}) USGrph 𝐹 ↔ 𝐹:dom 𝐹–1-1→{𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2})) |
75 | 69, 74 | syl 17 |
. . 3
⊢ (𝑉 USGrph 𝐸 → ((𝑉 ∖ {𝑁}) USGrph 𝐹 ↔ 𝐹:dom 𝐹–1-1→{𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2})) |
76 | 75 | adantr 480 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝑉 ∖ {𝑁}) USGrph 𝐹 ↔ 𝐹:dom 𝐹–1-1→{𝑒 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑒) = 2})) |
77 | 68, 76 | mpbird 246 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑉 ∖ {𝑁}) USGrph 𝐹) |