Step | Hyp | Ref
| Expression |
1 | | cusisusgra 25987 |
. . 3
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | | usgrav 25867 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
4 | | simp-4l 802 |
. . . . . . . 8
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑉 USGrph 𝐸) ∧ 𝑘 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
5 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) ∧ 𝑘 ∈ 𝑉) → 𝑘 ∈ 𝑉) |
6 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑉 ∖ {𝑘}) → 𝑛 ∈ 𝑉) |
7 | 5, 6 | anim12i 588 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑉 USGrph 𝐸) ∧ 𝑘 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) → (𝑘 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) |
8 | 7 | adantr 480 |
. . . . . . . 8
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑉 USGrph 𝐸) ∧ 𝑘 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → (𝑘 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) |
9 | | usgraf1o 25887 |
. . . . . . . . . . . . 13
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
10 | 9 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
11 | | prcom 4211 |
. . . . . . . . . . . . . . 15
⊢ {𝑛, 𝑘} = {𝑘, 𝑛} |
12 | 11 | eleq1i 2679 |
. . . . . . . . . . . . . 14
⊢ ({𝑛, 𝑘} ∈ ran 𝐸 ↔ {𝑘, 𝑛} ∈ ran 𝐸) |
13 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . 14
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝑘, 𝑛} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{𝑘, 𝑛})) = {𝑘, 𝑛}) |
14 | 12, 13 | sylan2b 491 |
. . . . . . . . . . . . 13
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝑛, 𝑘} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{𝑘, 𝑛})) = {𝑘, 𝑛}) |
15 | 14 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝐸‘(◡𝐸‘{𝑘, 𝑛})) = {𝑘, 𝑛})) |
16 | 10, 15 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝐸‘(◡𝐸‘{𝑘, 𝑛})) = {𝑘, 𝑛})) |
17 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) ∧ 𝑘 ∈ 𝑉) → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝐸‘(◡𝐸‘{𝑘, 𝑛})) = {𝑘, 𝑛})) |
18 | 17 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑉 USGrph 𝐸) ∧ 𝑘 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) → ({𝑛, 𝑘} ∈ ran 𝐸 → (𝐸‘(◡𝐸‘{𝑘, 𝑛})) = {𝑘, 𝑛})) |
19 | 18 | imp 444 |
. . . . . . . 8
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑉 USGrph 𝐸) ∧ 𝑘 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{𝑘, 𝑛})) = {𝑘, 𝑛}) |
20 | | 1pthon2v 26123 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑘 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ (𝐸‘(◡𝐸‘{𝑘, 𝑛})) = {𝑘, 𝑛}) → ∃𝑓∃𝑝 𝑓(𝑘(𝑉 PathOn 𝐸)𝑛)𝑝) |
21 | 4, 8, 19, 20 | syl3anc 1318 |
. . . . . . 7
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑉 USGrph 𝐸) ∧ 𝑘 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) ∧ {𝑛, 𝑘} ∈ ran 𝐸) → ∃𝑓∃𝑝 𝑓(𝑘(𝑉 PathOn 𝐸)𝑛)𝑝) |
22 | 21 | ex 449 |
. . . . . 6
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
𝑉 USGrph 𝐸) ∧ 𝑘 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑘})) → ({𝑛, 𝑘} ∈ ran 𝐸 → ∃𝑓∃𝑝 𝑓(𝑘(𝑉 PathOn 𝐸)𝑛)𝑝)) |
23 | 22 | ralimdva 2945 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) ∧ 𝑘 ∈ 𝑉) → (∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 → ∀𝑛 ∈ (𝑉 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(𝑉 PathOn 𝐸)𝑛)𝑝)) |
24 | 23 | ralimdva 2945 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 → ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(𝑉 PathOn 𝐸)𝑛)𝑝)) |
25 | 24 | expimpd 627 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸) → ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(𝑉 PathOn 𝐸)𝑛)𝑝)) |
26 | | iscusgra 25985 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸))) |
27 | | isconngra1 26201 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ConnGrph 𝐸 ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(𝑉 PathOn 𝐸)𝑛)𝑝)) |
28 | 25, 26, 27 | 3imtr4d 282 |
. 2
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ComplUSGrph 𝐸 → 𝑉 ConnGrph 𝐸)) |
29 | 3, 28 | mpcom 37 |
1
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 ConnGrph 𝐸) |