Step | Hyp | Ref
| Expression |
1 | | cusisusgra 25987 |
. . 3
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | | cusgrares.f |
. . . 4
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
3 | 2 | usgrares1 25939 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑉 ∖ {𝑁}) USGrph 𝐹) |
4 | 1, 3 | sylan 487 |
. 2
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑉 ∖ {𝑁}) USGrph 𝐹) |
5 | | iscusgra0 25986 |
. . . 4
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)) |
6 | | usgraf1o 25887 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
7 | | f1ocnvdm 6440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝑛, 𝑘} ∈ ran 𝐸) → (◡𝐸‘{𝑛, 𝑘}) ∈ dom 𝐸) |
8 | 7 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → (◡𝐸‘{𝑛, 𝑘}) ∈ dom 𝐸) |
9 | | elpri 4145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ {𝑛, 𝑘} → (𝑁 = 𝑛 ∨ 𝑁 = 𝑘)) |
10 | | vsnid 4156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ 𝑛 ∈ {𝑛} |
11 | | sneq 4135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 = 𝑛 → {𝑁} = {𝑛}) |
12 | 10, 11 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 = 𝑛 → 𝑛 ∈ {𝑁}) |
13 | 12 | notnotd 137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 = 𝑛 → ¬ ¬ 𝑛 ∈ {𝑁}) |
14 | | df-nel 2783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑛 ∉ {𝑁} ↔ ¬ 𝑛 ∈ {𝑁}) |
15 | 13, 14 | sylnibr 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 = 𝑛 → ¬ 𝑛 ∉ {𝑁}) |
16 | | vsnid 4156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ 𝑘 ∈ {𝑘} |
17 | | sneq 4135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 = 𝑘 → {𝑁} = {𝑘}) |
18 | 16, 17 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 = 𝑘 → 𝑘 ∈ {𝑁}) |
19 | 18 | notnotd 137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 = 𝑘 → ¬ ¬ 𝑘 ∈ {𝑁}) |
20 | | df-nel 2783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑘 ∉ {𝑁} ↔ ¬ 𝑘 ∈ {𝑁}) |
21 | 19, 20 | sylnibr 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 = 𝑘 → ¬ 𝑘 ∉ {𝑁}) |
22 | 15, 21 | orim12i 537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 = 𝑛 ∨ 𝑁 = 𝑘) → (¬ 𝑛 ∉ {𝑁} ∨ ¬ 𝑘 ∉ {𝑁})) |
23 | 9, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ {𝑛, 𝑘} → (¬ 𝑛 ∉ {𝑁} ∨ ¬ 𝑘 ∉ {𝑁})) |
24 | | ianor 508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (¬
(𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) ↔ (¬ 𝑛 ∉ {𝑁} ∨ ¬ 𝑘 ∉ {𝑁})) |
25 | 23, 24 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ {𝑛, 𝑘} → ¬ (𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁})) |
26 | 25 | con2i 133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) → ¬ 𝑁 ∈ {𝑛, 𝑘}) |
27 | | df-nel 2783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∉ {𝑛, 𝑘} ↔ ¬ 𝑁 ∈ {𝑛, 𝑘}) |
28 | 26, 27 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) → 𝑁 ∉ {𝑛, 𝑘}) |
29 | 28 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → 𝑁 ∉ {𝑛, 𝑘}) |
30 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝑛, 𝑘} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘}) |
31 | 30 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘}) |
32 | | neleq2 2889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘} → (𝑁 ∉ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) ↔ 𝑁 ∉ {𝑛, 𝑘})) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → (𝑁 ∉ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) ↔ 𝑁 ∉ {𝑛, 𝑘})) |
34 | 29, 33 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → 𝑁 ∉ (𝐸‘(◡𝐸‘{𝑛, 𝑘}))) |
35 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = (◡𝐸‘{𝑛, 𝑘}) → (𝐸‘𝑥) = (𝐸‘(◡𝐸‘{𝑛, 𝑘}))) |
36 | | neleq2 2889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐸‘𝑥) = (𝐸‘(◡𝐸‘{𝑛, 𝑘})) → (𝑁 ∉ (𝐸‘𝑥) ↔ 𝑁 ∉ (𝐸‘(◡𝐸‘{𝑛, 𝑘})))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = (◡𝐸‘{𝑛, 𝑘}) → (𝑁 ∉ (𝐸‘𝑥) ↔ 𝑁 ∉ (𝐸‘(◡𝐸‘{𝑛, 𝑘})))) |
38 | 37 | elrab 3331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ↔ ((◡𝐸‘{𝑛, 𝑘}) ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘(◡𝐸‘{𝑛, 𝑘})))) |
39 | 8, 34, 38 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → (◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
40 | 39, 31 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘})) |
41 | 40 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → ({𝑛, 𝑘} ∈ ran 𝐸 → ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘})))) |
42 | 41 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∉ {𝑁} ∧ 𝑘 ∉ {𝑁}) → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘})))) |
43 | 42 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∉ {𝑁} → (𝑘 ∉ {𝑁} → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘}))))) |
44 | 43 | com14 94 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → (𝑘 ∉ {𝑁} → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝑛 ∉ {𝑁} → ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘}))))) |
45 | 6, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 USGrph 𝐸 → (𝑘 ∉ {𝑁} → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝑛 ∉ {𝑁} → ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘}))))) |
46 | 45 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) → (𝑘 ∉ {𝑁} → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝑛 ∉ {𝑁} → ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘}))))) |
47 | 46 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝑛 ∉ {𝑁} → ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘})))) |
48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝑛 ∉ {𝑁} → ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘})))) |
49 | 48 | imp31 447 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑉 USGrph
𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) ∧ {𝑛, 𝑘} ∈ ran 𝐸) ∧ 𝑛 ∉ {𝑁}) → ((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘})) |
50 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (◡𝐸‘{𝑛, 𝑘}) → (𝐸‘𝑦) = (𝐸‘(◡𝐸‘{𝑛, 𝑘}))) |
51 | 50 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (◡𝐸‘{𝑛, 𝑘}) → ((𝐸‘𝑦) = {𝑛, 𝑘} ↔ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘})) |
52 | 51 | rspcev 3282 |
. . . . . . . . . . . . . . . . 17
⊢ (((◡𝐸‘{𝑛, 𝑘}) ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ∧ (𝐸‘(◡𝐸‘{𝑛, 𝑘})) = {𝑛, 𝑘}) → ∃𝑦 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} (𝐸‘𝑦) = {𝑛, 𝑘}) |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑉 USGrph
𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) ∧ {𝑛, 𝑘} ∈ ran 𝐸) ∧ 𝑛 ∉ {𝑁}) → ∃𝑦 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} (𝐸‘𝑦) = {𝑛, 𝑘}) |
54 | | usgrafun 25878 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
55 | | funfn 5833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Fun
𝐸 ↔ 𝐸 Fn dom 𝐸) |
56 | 54, 55 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 USGrph 𝐸 → 𝐸 Fn dom 𝐸) |
57 | 56 | ad6antr 768 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑉 USGrph
𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) ∧ {𝑛, 𝑘} ∈ ran 𝐸) ∧ 𝑛 ∉ {𝑁}) → 𝐸 Fn dom 𝐸) |
58 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ⊆ dom 𝐸 |
59 | | fvelimab 6163 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 Fn dom 𝐸 ∧ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} ⊆ dom 𝐸) → ({𝑛, 𝑘} ∈ (𝐸 “ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ↔ ∃𝑦 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} (𝐸‘𝑦) = {𝑛, 𝑘})) |
60 | 57, 58, 59 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑉 USGrph
𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) ∧ {𝑛, 𝑘} ∈ ran 𝐸) ∧ 𝑛 ∉ {𝑁}) → ({𝑛, 𝑘} ∈ (𝐸 “ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ↔ ∃𝑦 ∈ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)} (𝐸‘𝑦) = {𝑛, 𝑘})) |
61 | 53, 60 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑉 USGrph
𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) ∧ {𝑛, 𝑘} ∈ ran 𝐸) ∧ 𝑛 ∉ {𝑁}) → {𝑛, 𝑘} ∈ (𝐸 “ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)})) |
62 | 2 | rneqi 5273 |
. . . . . . . . . . . . . . . 16
⊢ ran 𝐹 = ran (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
63 | | df-ima 5051 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 “ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) = ran (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
64 | 62, 63 | eqtr4i 2635 |
. . . . . . . . . . . . . . 15
⊢ ran 𝐹 = (𝐸 “ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
65 | 61, 64 | syl6eleqr 2699 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑉 USGrph
𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) ∧ {𝑛, 𝑘} ∈ ran 𝐸) ∧ 𝑛 ∉ {𝑁}) → {𝑛, 𝑘} ∈ ran 𝐹) |
66 | 65 | exp31 628 |
. . . . . . . . . . . . 13
⊢
(((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝑛 ∉ {𝑁} → {𝑛, 𝑘} ∈ ran 𝐹))) |
67 | 66 | ralimdva 2945 |
. . . . . . . . . . . 12
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) → (∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 → ∀𝑛 ∈ (𝑉 ∖ {𝑘})(𝑛 ∉ {𝑁} → {𝑛, 𝑘} ∈ ran 𝐹))) |
68 | 67 | imp 444 |
. . . . . . . . . . 11
⊢
(((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸) → ∀𝑛 ∈ (𝑉 ∖ {𝑘})(𝑛 ∉ {𝑁} → {𝑛, 𝑘} ∈ ran 𝐹)) |
69 | | raldifb 3712 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
(𝑉 ∖ {𝑘})(𝑛 ∉ {𝑁} → {𝑛, 𝑘} ∈ ran 𝐹) ↔ ∀𝑛 ∈ ((𝑉 ∖ {𝑘}) ∖ {𝑁}){𝑛, 𝑘} ∈ ran 𝐹) |
70 | 68, 69 | sylib 207 |
. . . . . . . . . 10
⊢
(((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸) → ∀𝑛 ∈ ((𝑉 ∖ {𝑘}) ∖ {𝑁}){𝑛, 𝑘} ∈ ran 𝐹) |
71 | | dif32 3850 |
. . . . . . . . . . 11
⊢ ((𝑉 ∖ {𝑁}) ∖ {𝑘}) = ((𝑉 ∖ {𝑘}) ∖ {𝑁}) |
72 | 71 | raleqi 3119 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹 ↔ ∀𝑛 ∈ ((𝑉 ∖ {𝑘}) ∖ {𝑁}){𝑛, 𝑘} ∈ ran 𝐹) |
73 | 70, 72 | sylibr 223 |
. . . . . . . . 9
⊢
(((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) ∧ 𝑘 ∉ {𝑁}) ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸) → ∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹) |
74 | 73 | exp31 628 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) → (𝑘 ∉ {𝑁} → (∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 → ∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹))) |
75 | 74 | com23 84 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) ∧ 𝑘 ∈ 𝑉) → (∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 → (𝑘 ∉ {𝑁} → ∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹))) |
76 | 75 | ralimdva 2945 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 → ∀𝑘 ∈ 𝑉 (𝑘 ∉ {𝑁} → ∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹))) |
77 | 76 | impancom 455 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸) → (𝑁 ∈ 𝑉 → ∀𝑘 ∈ 𝑉 (𝑘 ∉ {𝑁} → ∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹))) |
78 | | raldifb 3712 |
. . . . 5
⊢
(∀𝑘 ∈
𝑉 (𝑘 ∉ {𝑁} → ∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹) ↔ ∀𝑘 ∈ (𝑉 ∖ {𝑁})∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹) |
79 | 77, 78 | syl6ib 240 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸) → (𝑁 ∈ 𝑉 → ∀𝑘 ∈ (𝑉 ∖ {𝑁})∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹)) |
80 | 5, 79 | syl 17 |
. . 3
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑁 ∈ 𝑉 → ∀𝑘 ∈ (𝑉 ∖ {𝑁})∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹)) |
81 | 80 | imp 444 |
. 2
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ∀𝑘 ∈ (𝑉 ∖ {𝑁})∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹) |
82 | | usgrav 25867 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
83 | | difexg 4735 |
. . . . 5
⊢ (𝑉 ∈ V → (𝑉 ∖ {𝑁}) ∈ V) |
84 | | resexg 5362 |
. . . . . 6
⊢ (𝐸 ∈ V → (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ∈ V) |
85 | 2, 84 | syl5eqel 2692 |
. . . . 5
⊢ (𝐸 ∈ V → 𝐹 ∈ V) |
86 | | iscusgra 25985 |
. . . . 5
⊢ (((𝑉 ∖ {𝑁}) ∈ V ∧ 𝐹 ∈ V) → ((𝑉 ∖ {𝑁}) ComplUSGrph 𝐹 ↔ ((𝑉 ∖ {𝑁}) USGrph 𝐹 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑁})∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹))) |
87 | 83, 85, 86 | syl2an 493 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑉 ∖ {𝑁}) ComplUSGrph 𝐹 ↔ ((𝑉 ∖ {𝑁}) USGrph 𝐹 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑁})∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹))) |
88 | 1, 82, 87 | 3syl 18 |
. . 3
⊢ (𝑉 ComplUSGrph 𝐸 → ((𝑉 ∖ {𝑁}) ComplUSGrph 𝐹 ↔ ((𝑉 ∖ {𝑁}) USGrph 𝐹 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑁})∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹))) |
89 | 88 | adantr 480 |
. 2
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → ((𝑉 ∖ {𝑁}) ComplUSGrph 𝐹 ↔ ((𝑉 ∖ {𝑁}) USGrph 𝐹 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑁})∀𝑛 ∈ ((𝑉 ∖ {𝑁}) ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹))) |
90 | 4, 81, 89 | mpbir2and 959 |
1
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑉 ∖ {𝑁}) ComplUSGrph 𝐹) |