Step | Hyp | Ref
| Expression |
1 | | iscusgra0 25986 |
. 2
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸)) |
2 | | usgraf0 25877 |
. . 3
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
3 | | f1f 6014 |
. . . . . . 7
⊢ (𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
4 | | df-f 5808 |
. . . . . . . 8
⊢ (𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
5 | | ssel 3562 |
. . . . . . . . 9
⊢ (ran
𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → (𝑒 ∈ ran 𝐸 → 𝑒 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
6 | 5 | adantl 481 |
. . . . . . . 8
⊢ ((𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) → (𝑒 ∈ ran 𝐸 → 𝑒 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
7 | 4, 6 | sylbi 206 |
. . . . . . 7
⊢ (𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → (𝑒 ∈ ran 𝐸 → 𝑒 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
8 | 3, 7 | syl 17 |
. . . . . 6
⊢ (𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → (𝑒 ∈ ran 𝐸 → 𝑒 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
9 | 8 | adantr 480 |
. . . . 5
⊢ ((𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸) → (𝑒 ∈ ran 𝐸 → 𝑒 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
10 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑒 → (#‘𝑥) = (#‘𝑒)) |
11 | 10 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑥 = 𝑒 → ((#‘𝑥) = 2 ↔ (#‘𝑒) = 2)) |
12 | 11 | elrab 3331 |
. . . . . . . 8
⊢ (𝑒 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ↔ (𝑒 ∈ 𝒫 𝑉 ∧ (#‘𝑒) = 2)) |
13 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑒 ∈ V |
14 | | hash2prde 13109 |
. . . . . . . . . . 11
⊢ ((𝑒 ∈ V ∧ (#‘𝑒) = 2) → ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) |
15 | 13, 14 | mpan 702 |
. . . . . . . . . 10
⊢
((#‘𝑒) = 2
→ ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) |
16 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = {𝑎, 𝑏} → (𝑒 ∈ 𝒫 𝑉 ↔ {𝑎, 𝑏} ∈ 𝒫 𝑉)) |
17 | | prex 4836 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑎, 𝑏} ∈ V |
18 | 17 | elpw 4114 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑎, 𝑏} ∈ 𝒫 𝑉 ↔ {𝑎, 𝑏} ⊆ 𝑉) |
19 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑎 ∈ V |
20 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑏 ∈ V |
21 | 19, 20 | prss 4291 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ↔ {𝑎, 𝑏} ⊆ 𝑉) |
22 | 18, 21 | bitr4i 266 |
. . . . . . . . . . . . . . 15
⊢ ({𝑎, 𝑏} ∈ 𝒫 𝑉 ↔ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) |
23 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = {𝑎, 𝑏} ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑎 ∈ 𝑉) |
24 | 23 | anim1i 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒 = {𝑎, 𝑏} ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑎 ≠ 𝑏) → (𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏)) |
25 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ (𝑉 ∖ {𝑏}) ↔ (𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏)) |
26 | 24, 25 | sylibr 223 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 = {𝑎, 𝑏} ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑎 ≠ 𝑏) → 𝑎 ∈ (𝑉 ∖ {𝑏})) |
27 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒 = {𝑎, 𝑏} ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑎 ≠ 𝑏) → 𝑏 ∈ 𝑉) |
28 | | sneq 4135 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑏 → {𝑘} = {𝑏}) |
29 | 28 | difeq2d 3690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑏 → (𝑉 ∖ {𝑘}) = (𝑉 ∖ {𝑏})) |
30 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑏 → {𝑙, 𝑘} = {𝑙, 𝑏}) |
31 | 30 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑏 → ({𝑙, 𝑘} ∈ ran 𝐸 ↔ {𝑙, 𝑏} ∈ ran 𝐸)) |
32 | 29, 31 | raleqbidv 3129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑏 → (∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 ↔ ∀𝑙 ∈ (𝑉 ∖ {𝑏}){𝑙, 𝑏} ∈ ran 𝐸)) |
33 | 32 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ 𝑉 → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → ∀𝑙 ∈ (𝑉 ∖ {𝑏}){𝑙, 𝑏} ∈ ran 𝐸)) |
34 | 27, 33 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 = {𝑎, 𝑏} ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑎 ≠ 𝑏) → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → ∀𝑙 ∈ (𝑉 ∖ {𝑏}){𝑙, 𝑏} ∈ ran 𝐸)) |
35 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑎 → {𝑙, 𝑏} = {𝑎, 𝑏}) |
36 | 35 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑎 → ({𝑙, 𝑏} ∈ ran 𝐸 ↔ {𝑎, 𝑏} ∈ ran 𝐸)) |
37 | 36 | rspcv 3278 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ (𝑉 ∖ {𝑏}) → (∀𝑙 ∈ (𝑉 ∖ {𝑏}){𝑙, 𝑏} ∈ ran 𝐸 → {𝑎, 𝑏} ∈ ran 𝐸)) |
38 | 26, 34, 37 | sylsyld 59 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 = {𝑎, 𝑏} ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑎 ≠ 𝑏) → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → {𝑎, 𝑏} ∈ ran 𝐸)) |
39 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = {𝑎, 𝑏} → (𝑒 ∈ ran 𝐸 ↔ {𝑎, 𝑏} ∈ ran 𝐸)) |
40 | 39 | bicomd 212 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = {𝑎, 𝑏} → ({𝑎, 𝑏} ∈ ran 𝐸 ↔ 𝑒 ∈ ran 𝐸)) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = {𝑎, 𝑏} ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ({𝑎, 𝑏} ∈ ran 𝐸 ↔ 𝑒 ∈ ran 𝐸)) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 = {𝑎, 𝑏} ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑎 ≠ 𝑏) → ({𝑎, 𝑏} ∈ ran 𝐸 ↔ 𝑒 ∈ ran 𝐸)) |
43 | 38, 42 | sylibd 228 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 = {𝑎, 𝑏} ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑎 ≠ 𝑏) → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → 𝑒 ∈ ran 𝐸)) |
44 | 43 | exp31 628 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = {𝑎, 𝑏} → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑎 ≠ 𝑏 → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → 𝑒 ∈ ran 𝐸)))) |
45 | 22, 44 | syl5bi 231 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = {𝑎, 𝑏} → ({𝑎, 𝑏} ∈ 𝒫 𝑉 → (𝑎 ≠ 𝑏 → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → 𝑒 ∈ ran 𝐸)))) |
46 | 16, 45 | sylbid 229 |
. . . . . . . . . . . . 13
⊢ (𝑒 = {𝑎, 𝑏} → (𝑒 ∈ 𝒫 𝑉 → (𝑎 ≠ 𝑏 → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → 𝑒 ∈ ran 𝐸)))) |
47 | 46 | com23 84 |
. . . . . . . . . . . 12
⊢ (𝑒 = {𝑎, 𝑏} → (𝑎 ≠ 𝑏 → (𝑒 ∈ 𝒫 𝑉 → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → 𝑒 ∈ ran 𝐸)))) |
48 | 47 | impcom 445 |
. . . . . . . . . . 11
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → (𝑒 ∈ 𝒫 𝑉 → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → 𝑒 ∈ ran 𝐸))) |
49 | 48 | exlimivv 1847 |
. . . . . . . . . 10
⊢
(∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → (𝑒 ∈ 𝒫 𝑉 → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → 𝑒 ∈ ran 𝐸))) |
50 | 15, 49 | syl 17 |
. . . . . . . . 9
⊢
((#‘𝑒) = 2
→ (𝑒 ∈ 𝒫
𝑉 → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → 𝑒 ∈ ran 𝐸))) |
51 | 50 | impcom 445 |
. . . . . . . 8
⊢ ((𝑒 ∈ 𝒫 𝑉 ∧ (#‘𝑒) = 2) → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → 𝑒 ∈ ran 𝐸)) |
52 | 12, 51 | sylbi 206 |
. . . . . . 7
⊢ (𝑒 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → 𝑒 ∈ ran 𝐸)) |
53 | 52 | com12 32 |
. . . . . 6
⊢
(∀𝑘 ∈
𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸 → (𝑒 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → 𝑒 ∈ ran 𝐸)) |
54 | 53 | adantl 481 |
. . . . 5
⊢ ((𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸) → (𝑒 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} → 𝑒 ∈ ran 𝐸)) |
55 | 9, 54 | impbid 201 |
. . . 4
⊢ ((𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸) → (𝑒 ∈ ran 𝐸 ↔ 𝑒 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) |
56 | 55 | eqrdv 2608 |
. . 3
⊢ ((𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸) → ran 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
57 | 2, 56 | sylan 487 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘}){𝑙, 𝑘} ∈ ran 𝐸) → ran 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |
58 | 1, 57 | syl 17 |
1
⊢ (𝑉 ComplUSGrph 𝐸 → ran 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) |