Step | Hyp | Ref
| Expression |
1 | | usgrarnedg 25913 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑒 ∈ ran 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) |
2 | | iscusgra0 25986 |
. . . . . . 7
⊢ (𝑉 ComplUSGrph 𝐹 → (𝑉 USGrph 𝐹 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹)) |
3 | | simplrr 797 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → 𝑏 ∈ 𝑉) |
4 | | sneq 4135 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑏 → {𝑘} = {𝑏}) |
5 | 4 | difeq2d 3690 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑏 → (𝑉 ∖ {𝑘}) = (𝑉 ∖ {𝑏})) |
6 | | preq2 4213 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑏 → {𝑛, 𝑘} = {𝑛, 𝑏}) |
7 | 6 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑏 → ({𝑛, 𝑘} ∈ ran 𝐹 ↔ {𝑛, 𝑏} ∈ ran 𝐹)) |
8 | 5, 7 | raleqbidv 3129 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑏 → (∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹 ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑏}){𝑛, 𝑏} ∈ ran 𝐹)) |
9 | 8 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ 𝑉 → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹 → ∀𝑛 ∈ (𝑉 ∖ {𝑏}){𝑛, 𝑏} ∈ ran 𝐹)) |
10 | 3, 9 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹 → ∀𝑛 ∈ (𝑉 ∖ {𝑏}){𝑛, 𝑏} ∈ ran 𝐹)) |
11 | | simplrl 796 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑎 ≠ 𝑏) → 𝑎 ∈ 𝑉) |
12 | | velsn 4141 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ {𝑏} ↔ 𝑎 = 𝑏) |
13 | | nne 2786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑎 ≠ 𝑏 ↔ 𝑎 = 𝑏) |
14 | 12, 13 | bitr4i 266 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ {𝑏} ↔ ¬ 𝑎 ≠ 𝑏) |
15 | 14 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ {𝑏} → ¬ 𝑎 ≠ 𝑏) |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 ∈ {𝑏} → ¬ 𝑎 ≠ 𝑏)) |
17 | 16 | con2d 128 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 ≠ 𝑏 → ¬ 𝑎 ∈ {𝑏})) |
18 | 17 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑎 ≠ 𝑏) → ¬ 𝑎 ∈ {𝑏}) |
19 | 11, 18 | eldifd 3551 |
. . . . . . . . . . . . 13
⊢ (((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑎 ≠ 𝑏) → 𝑎 ∈ (𝑉 ∖ {𝑏})) |
20 | 19 | adantrr 749 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → 𝑎 ∈ (𝑉 ∖ {𝑏})) |
21 | | preq1 4212 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑎 → {𝑛, 𝑏} = {𝑎, 𝑏}) |
22 | 21 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑎 → ({𝑛, 𝑏} ∈ ran 𝐹 ↔ {𝑎, 𝑏} ∈ ran 𝐹)) |
23 | 22 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (𝑉 ∖ {𝑏}) → (∀𝑛 ∈ (𝑉 ∖ {𝑏}){𝑛, 𝑏} ∈ ran 𝐹 → {𝑎, 𝑏} ∈ ran 𝐹)) |
24 | 20, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → (∀𝑛 ∈ (𝑉 ∖ {𝑏}){𝑛, 𝑏} ∈ ran 𝐹 → {𝑎, 𝑏} ∈ ran 𝐹)) |
25 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ ({𝑎, 𝑏} = 𝑒 → ({𝑎, 𝑏} ∈ ran 𝐹 ↔ 𝑒 ∈ ran 𝐹)) |
26 | 25 | eqcoms 2618 |
. . . . . . . . . . . . 13
⊢ (𝑒 = {𝑎, 𝑏} → ({𝑎, 𝑏} ∈ ran 𝐹 ↔ 𝑒 ∈ ran 𝐹)) |
27 | | equid 1926 |
. . . . . . . . . . . . . 14
⊢ 𝑒 = 𝑒 |
28 | | equequ2 1940 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑒 → (𝑒 = 𝑓 ↔ 𝑒 = 𝑒)) |
29 | 28 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 ∈ ran 𝐹 ∧ 𝑒 = 𝑒) → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓) |
30 | 27, 29 | mpan2 703 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ ran 𝐹 → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓) |
31 | 26, 30 | syl6bi 242 |
. . . . . . . . . . . 12
⊢ (𝑒 = {𝑎, 𝑏} → ({𝑎, 𝑏} ∈ ran 𝐹 → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓)) |
32 | 31 | ad2antll 761 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → ({𝑎, 𝑏} ∈ ran 𝐹 → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓)) |
33 | 10, 24, 32 | 3syld 58 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐹 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹 → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓)) |
34 | 33 | exp31 628 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐹 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹 → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓)))) |
35 | 34 | com24 93 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐹 → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹 → ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓)))) |
36 | 35 | imp 444 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐹 ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐹) → ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓))) |
37 | 2, 36 | syl 17 |
. . . . . 6
⊢ (𝑉 ComplUSGrph 𝐹 → ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓))) |
38 | 37 | com13 86 |
. . . . 5
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → (𝑉 ComplUSGrph 𝐹 → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓))) |
39 | 38 | rexlimivv 3018 |
. . . 4
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → (𝑉 ComplUSGrph 𝐹 → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓)) |
40 | 1, 39 | syl 17 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑒 ∈ ran 𝐸) → (𝑉 ComplUSGrph 𝐹 → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓)) |
41 | 40 | impancom 455 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (𝑒 ∈ ran 𝐸 → ∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓)) |
42 | 41 | ralrimiv 2948 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → ∀𝑒 ∈ ran 𝐸∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓) |