Step | Hyp | Ref
| Expression |
1 | | f1oi 6086 |
. . 3
⊢ ( I
↾ ran 𝐸):ran 𝐸–1-1-onto→ran
𝐸 |
2 | | f1of1 6049 |
. . 3
⊢ (( I
↾ ran 𝐸):ran 𝐸–1-1-onto→ran
𝐸 → ( I ↾ ran
𝐸):ran 𝐸–1-1→ran 𝐸) |
3 | 1, 2 | ax-mp 5 |
. 2
⊢ ( I
↾ ran 𝐸):ran 𝐸–1-1→ran 𝐸 |
4 | | iscusgra0 25986 |
. . . . 5
⊢ (𝑉 ComplUSGrph 𝐹 → (𝑉 USGrph 𝐹 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹)) |
5 | | usgrarnedg 25913 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑒 ∈ ran 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) |
6 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ≠ 𝑏 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑏 ∈ 𝑉) |
7 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ (𝑉 ∖ {𝑏}) ↔ (𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏)) |
8 | 7 | simplbi2 653 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ 𝑉 → (𝑎 ≠ 𝑏 → 𝑎 ∈ (𝑉 ∖ {𝑏}))) |
9 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑎 ≠ 𝑏 → 𝑎 ∈ (𝑉 ∖ {𝑏}))) |
10 | 9 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ≠ 𝑏 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑎 ∈ (𝑉 ∖ {𝑏})) |
11 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ≠ 𝑏 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑥 = 𝑏) → 𝑎 ∈ (𝑉 ∖ {𝑏})) |
12 | | sneq 4135 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑏 → {𝑥} = {𝑏}) |
13 | 12 | difeq2d 3690 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑏 → (𝑉 ∖ {𝑥}) = (𝑉 ∖ {𝑏})) |
14 | 13 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑏 → (𝑎 ∈ (𝑉 ∖ {𝑥}) ↔ 𝑎 ∈ (𝑉 ∖ {𝑏}))) |
15 | 14 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ≠ 𝑏 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑥 = 𝑏) → (𝑎 ∈ (𝑉 ∖ {𝑥}) ↔ 𝑎 ∈ (𝑉 ∖ {𝑏}))) |
16 | 11, 15 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ≠ 𝑏 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑥 = 𝑏) → 𝑎 ∈ (𝑉 ∖ {𝑥})) |
17 | | preq12 4214 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 = 𝑎 ∧ 𝑥 = 𝑏) → {𝑦, 𝑥} = {𝑎, 𝑏}) |
18 | 17 | expcom 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑏 → (𝑦 = 𝑎 → {𝑦, 𝑥} = {𝑎, 𝑏})) |
19 | 18 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ≠ 𝑏 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑥 = 𝑏) → (𝑦 = 𝑎 → {𝑦, 𝑥} = {𝑎, 𝑏})) |
20 | 19 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ≠ 𝑏 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑥 = 𝑏) ∧ 𝑦 = 𝑎) → {𝑦, 𝑥} = {𝑎, 𝑏}) |
21 | 20 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ≠ 𝑏 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑥 = 𝑏) ∧ 𝑦 = 𝑎) → ({𝑦, 𝑥} ∈ ran 𝐹 ↔ {𝑎, 𝑏} ∈ ran 𝐹)) |
22 | 16, 21 | rspcdv 3285 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ≠ 𝑏 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑥 = 𝑏) → (∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹 → {𝑎, 𝑏} ∈ ran 𝐹)) |
23 | 6, 22 | rspcimdv 3283 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ≠ 𝑏 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹 → {𝑎, 𝑏} ∈ ran 𝐹)) |
24 | 23 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑎 ≠ 𝑏 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹 → {𝑎, 𝑏} ∈ ran 𝐹))) |
25 | 24 | com13 86 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑎 ≠ 𝑏 → {𝑎, 𝑏} ∈ ran 𝐹))) |
26 | 25 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐹 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑎 ≠ 𝑏 → {𝑎, 𝑏} ∈ ran 𝐹))) |
27 | 26 | imp 444 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐹 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 ≠ 𝑏 → {𝑎, 𝑏} ∈ ran 𝐹)) |
28 | 27 | com12 32 |
. . . . . . . . 9
⊢ (𝑎 ≠ 𝑏 → (((𝑉 USGrph 𝐹 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → {𝑎, 𝑏} ∈ ran 𝐹)) |
29 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑒 = {𝑎, 𝑏} → (𝑒 ∈ ran 𝐹 ↔ {𝑎, 𝑏} ∈ ran 𝐹)) |
30 | 29 | imbi2d 329 |
. . . . . . . . 9
⊢ (𝑒 = {𝑎, 𝑏} → ((((𝑉 USGrph 𝐹 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑒 ∈ ran 𝐹) ↔ (((𝑉 USGrph 𝐹 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → {𝑎, 𝑏} ∈ ran 𝐹))) |
31 | 28, 30 | syl5ibr 235 |
. . . . . . . 8
⊢ (𝑒 = {𝑎, 𝑏} → (𝑎 ≠ 𝑏 → (((𝑉 USGrph 𝐹 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑒 ∈ ran 𝐹))) |
32 | 31 | impcom 445 |
. . . . . . 7
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → (((𝑉 USGrph 𝐹 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑒 ∈ ran 𝐹)) |
33 | 32 | com12 32 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐹 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → 𝑒 ∈ ran 𝐹)) |
34 | 33 | rexlimdvva 3020 |
. . . . 5
⊢ ((𝑉 USGrph 𝐹 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥}){𝑦, 𝑥} ∈ ran 𝐹) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → 𝑒 ∈ ran 𝐹)) |
35 | 4, 5, 34 | syl2imc 40 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑒 ∈ ran 𝐸) → (𝑉 ComplUSGrph 𝐹 → 𝑒 ∈ ran 𝐹)) |
36 | 35 | impancom 455 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (𝑒 ∈ ran 𝐸 → 𝑒 ∈ ran 𝐹)) |
37 | 36 | ssrdv 3574 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → ran 𝐸 ⊆ ran 𝐹) |
38 | | f1ss 6019 |
. 2
⊢ ((( I
↾ ran 𝐸):ran 𝐸–1-1→ran 𝐸 ∧ ran 𝐸 ⊆ ran 𝐹) → ( I ↾ ran 𝐸):ran 𝐸–1-1→ran 𝐹) |
39 | 3, 37, 38 | sylancr 694 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → ( I ↾ ran 𝐸):ran 𝐸–1-1→ran 𝐹) |