Step | Hyp | Ref
| Expression |
1 | | usgraf0 25877 |
. . 3
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2}) |
2 | | f1f 6014 |
. . 3
⊢ (𝐸:dom 𝐸–1-1→{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} → 𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2}) |
3 | | ffvelrn 6265 |
. . . . 5
⊢ ((𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} ∧ 𝑋 ∈ dom 𝐸) → (𝐸‘𝑋) ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2}) |
4 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = (𝐸‘𝑋) → (#‘𝑦) = (#‘(𝐸‘𝑋))) |
5 | 4 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑦 = (𝐸‘𝑋) → ((#‘𝑦) = 2 ↔ (#‘(𝐸‘𝑋)) = 2)) |
6 | 5 | elrab 3331 |
. . . . . 6
⊢ ((𝐸‘𝑋) ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} ↔ ((𝐸‘𝑋) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑋)) = 2)) |
7 | | hash2pr 13108 |
. . . . . . 7
⊢ (((𝐸‘𝑋) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑋)) = 2) → ∃𝑎∃𝑏(𝐸‘𝑋) = {𝑎, 𝑏}) |
8 | | 19.42vv 1907 |
. . . . . . . . . . 11
⊢
(∃𝑎∃𝑏(𝑌 ∈ (𝐸‘𝑋) ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ↔ (𝑌 ∈ (𝐸‘𝑋) ∧ ∃𝑎∃𝑏(𝐸‘𝑋) = {𝑎, 𝑏})) |
9 | | eleq2 2677 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸‘𝑋) = {𝑎, 𝑏} → (𝑌 ∈ (𝐸‘𝑋) ↔ 𝑌 ∈ {𝑎, 𝑏})) |
10 | | elpri 4145 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ {𝑎, 𝑏} → (𝑌 = 𝑎 ∨ 𝑌 = 𝑏)) |
11 | | andir 908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑌 = 𝑎 ∨ 𝑌 = 𝑏) ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ↔ ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}))) |
12 | 11 | biimpi 205 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑌 = 𝑎 ∨ 𝑌 = 𝑏) ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) → ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}))) |
13 | 12 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑌 = 𝑎 ∨ 𝑌 = 𝑏) → ((𝐸‘𝑋) = {𝑎, 𝑏} → ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏})))) |
14 | 10, 13 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ∈ {𝑎, 𝑏} → ((𝐸‘𝑋) = {𝑎, 𝑏} → ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏})))) |
15 | 9, 14 | syl6bi 242 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸‘𝑋) = {𝑎, 𝑏} → (𝑌 ∈ (𝐸‘𝑋) → ((𝐸‘𝑋) = {𝑎, 𝑏} → ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}))))) |
16 | 15 | pm2.43a 52 |
. . . . . . . . . . . . . 14
⊢ ((𝐸‘𝑋) = {𝑎, 𝑏} → (𝑌 ∈ (𝐸‘𝑋) → ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏})))) |
17 | 16 | impcom 445 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ (𝐸‘𝑋) ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) → ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}))) |
18 | 17 | 2eximi 1753 |
. . . . . . . . . . . 12
⊢
(∃𝑎∃𝑏(𝑌 ∈ (𝐸‘𝑋) ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) → ∃𝑎∃𝑏((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}))) |
19 | | 19.43 1799 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑏((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏})) ↔ (∃𝑏(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ ∃𝑏(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}))) |
20 | 19 | exbii 1764 |
. . . . . . . . . . . . . 14
⊢
(∃𝑎∃𝑏((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏})) ↔ ∃𝑎(∃𝑏(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ ∃𝑏(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}))) |
21 | | 19.43 1799 |
. . . . . . . . . . . . . 14
⊢
(∃𝑎(∃𝑏(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ ∃𝑏(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏})) ↔ (∃𝑎∃𝑏(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ ∃𝑎∃𝑏(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}))) |
22 | 20, 21 | bitri 263 |
. . . . . . . . . . . . 13
⊢
(∃𝑎∃𝑏((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏})) ↔ (∃𝑎∃𝑏(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ ∃𝑎∃𝑏(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}))) |
23 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑦 → {𝑎, 𝑏} = {𝑎, 𝑦}) |
24 | 23 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑦 → ((𝐸‘𝑋) = {𝑎, 𝑏} ↔ (𝐸‘𝑋) = {𝑎, 𝑦})) |
25 | 24 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑦 → ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ↔ (𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑦}))) |
26 | 25 | cbvexv 2263 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑏(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ↔ ∃𝑦(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑦})) |
27 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = 𝑌 → {𝑎, 𝑦} = {𝑌, 𝑦}) |
28 | 27 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑌 = 𝑎 → {𝑎, 𝑦} = {𝑌, 𝑦}) |
29 | 28 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑌 = 𝑎 → ((𝐸‘𝑋) = {𝑎, 𝑦} ↔ (𝐸‘𝑋) = {𝑌, 𝑦})) |
30 | 29 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑦}) → (𝐸‘𝑋) = {𝑌, 𝑦}) |
31 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑎 ∈ V |
32 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑌 = 𝑎 → (𝑌 ∈ V ↔ 𝑎 ∈ V)) |
33 | 31, 32 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑌 = 𝑎 → 𝑌 ∈ V) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑦}) → 𝑌 ∈ V) |
35 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐸‘𝑋) = {𝑌, 𝑦} → ((𝐸‘𝑋) ∈ 𝒫 𝑉 ↔ {𝑌, 𝑦} ∈ 𝒫 𝑉)) |
36 | | prex 4836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ {𝑌, 𝑦} ∈ V |
37 | 36 | elpw 4114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ({𝑌, 𝑦} ∈ 𝒫 𝑉 ↔ {𝑌, 𝑦} ⊆ 𝑉) |
38 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑦 ∈ V |
39 | | prssg 4290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑌 ∈ V ∧ 𝑦 ∈ V) → ((𝑌 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ↔ {𝑌, 𝑦} ⊆ 𝑉)) |
40 | 39 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑌 ∈ V ∧ 𝑦 ∈ V) → ({𝑌, 𝑦} ⊆ 𝑉 ↔ (𝑌 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) |
41 | 38, 40 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑌 ∈ V → ({𝑌, 𝑦} ⊆ 𝑉 ↔ (𝑌 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) |
42 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑌 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
43 | 41, 42 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑌 ∈ V → ({𝑌, 𝑦} ⊆ 𝑉 → 𝑦 ∈ 𝑉)) |
44 | 43 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ({𝑌, 𝑦} ⊆ 𝑉 → (𝑌 ∈ V → 𝑦 ∈ 𝑉)) |
45 | 37, 44 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({𝑌, 𝑦} ∈ 𝒫 𝑉 → (𝑌 ∈ V → 𝑦 ∈ 𝑉)) |
46 | 35, 45 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐸‘𝑋) = {𝑌, 𝑦} → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (𝑌 ∈ V → 𝑦 ∈ 𝑉))) |
47 | 46 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐸‘𝑋) = {𝑌, 𝑦} → (𝑌 ∈ V → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → 𝑦 ∈ 𝑉))) |
48 | 47 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐸‘𝑋) = {𝑌, 𝑦} ∧ 𝑌 ∈ V) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → 𝑦 ∈ 𝑉)) |
49 | 48 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐸‘𝑋) = {𝑌, 𝑦} ∧ 𝑌 ∈ V) ∧ (𝐸‘𝑋) ∈ 𝒫 𝑉) → 𝑦 ∈ 𝑉) |
50 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐸‘𝑋) = {𝑌, 𝑦} ∧ 𝑌 ∈ V) ∧ (𝐸‘𝑋) ∈ 𝒫 𝑉) → (𝐸‘𝑋) = {𝑌, 𝑦}) |
51 | 49, 50 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐸‘𝑋) = {𝑌, 𝑦} ∧ 𝑌 ∈ V) ∧ (𝐸‘𝑋) ∈ 𝒫 𝑉) → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝑋) = {𝑌, 𝑦})) |
52 | 51 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐸‘𝑋) = {𝑌, 𝑦} ∧ 𝑌 ∈ V) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝑋) = {𝑌, 𝑦}))) |
53 | 30, 34, 52 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑦}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝑋) = {𝑌, 𝑦}))) |
54 | 53 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑦}) → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝑋) = {𝑌, 𝑦}))) |
55 | 54 | eximdv 1833 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (∃𝑦(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑦}) → ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝑋) = {𝑌, 𝑦}))) |
56 | | df-rex 2902 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦 ∈
𝑉 (𝐸‘𝑋) = {𝑌, 𝑦} ↔ ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝑋) = {𝑌, 𝑦})) |
57 | 55, 56 | syl6ibr 241 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (∃𝑦(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑦}) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
58 | 57 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑦(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑦}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
59 | 26, 58 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑏(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
60 | 59 | exlimiv 1845 |
. . . . . . . . . . . . . 14
⊢
(∃𝑎∃𝑏(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
61 | | excom 2029 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑎∃𝑏(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ↔ ∃𝑏∃𝑎(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏})) |
62 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑦 → {𝑎, 𝑏} = {𝑦, 𝑏}) |
63 | 62 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑦 → ((𝐸‘𝑋) = {𝑎, 𝑏} ↔ (𝐸‘𝑋) = {𝑦, 𝑏})) |
64 | 63 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑦 → ((𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ↔ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑦, 𝑏}))) |
65 | 64 | cbvexv 2263 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑎(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ↔ ∃𝑦(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑦, 𝑏})) |
66 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑏 = 𝑌 → {𝑦, 𝑏} = {𝑦, 𝑌}) |
67 | 66 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑌 = 𝑏 → {𝑦, 𝑏} = {𝑦, 𝑌}) |
68 | 67 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑌 = 𝑏 → ((𝐸‘𝑋) = {𝑦, 𝑏} ↔ (𝐸‘𝑋) = {𝑦, 𝑌})) |
69 | 68 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑦, 𝑏}) → (𝐸‘𝑋) = {𝑦, 𝑌}) |
70 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑏 ∈ V |
71 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑌 = 𝑏 → (𝑌 ∈ V ↔ 𝑏 ∈ V)) |
72 | 70, 71 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑌 = 𝑏 → 𝑌 ∈ V) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑦, 𝑏}) → 𝑌 ∈ V) |
74 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐸‘𝑋) = {𝑦, 𝑌} → ((𝐸‘𝑋) ∈ 𝒫 𝑉 ↔ {𝑦, 𝑌} ∈ 𝒫 𝑉)) |
75 | | prex 4836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ {𝑦, 𝑌} ∈ V |
76 | 75 | elpw 4114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({𝑦, 𝑌} ∈ 𝒫 𝑉 ↔ {𝑦, 𝑌} ⊆ 𝑉) |
77 | | prssg 4290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑦 ∈ V ∧ 𝑌 ∈ V) → ((𝑦 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ↔ {𝑦, 𝑌} ⊆ 𝑉)) |
78 | 77 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 ∈ V ∧ 𝑌 ∈ V) → ({𝑦, 𝑌} ⊆ 𝑉 ↔ (𝑦 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
79 | 38, 78 | mpan 702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑌 ∈ V → ({𝑦, 𝑌} ⊆ 𝑉 ↔ (𝑦 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
80 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑦 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
81 | 79, 80 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑌 ∈ V → ({𝑦, 𝑌} ⊆ 𝑉 → 𝑦 ∈ 𝑉)) |
82 | 81 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({𝑦, 𝑌} ⊆ 𝑉 → (𝑌 ∈ V → 𝑦 ∈ 𝑉)) |
83 | 76, 82 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({𝑦, 𝑌} ∈ 𝒫 𝑉 → (𝑌 ∈ V → 𝑦 ∈ 𝑉)) |
84 | 74, 83 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐸‘𝑋) = {𝑦, 𝑌} → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (𝑌 ∈ V → 𝑦 ∈ 𝑉))) |
85 | 84 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐸‘𝑋) = {𝑦, 𝑌} → (𝑌 ∈ V → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → 𝑦 ∈ 𝑉))) |
86 | 85 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐸‘𝑋) = {𝑦, 𝑌} ∧ 𝑌 ∈ V) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → 𝑦 ∈ 𝑉)) |
87 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {𝑦, 𝑌} = {𝑌, 𝑦} |
88 | 87 | eqeq2i 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐸‘𝑋) = {𝑦, 𝑌} ↔ (𝐸‘𝑋) = {𝑌, 𝑦}) |
89 | 88 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐸‘𝑋) = {𝑦, 𝑌} → (𝐸‘𝑋) = {𝑌, 𝑦}) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐸‘𝑋) = {𝑦, 𝑌} ∧ 𝑌 ∈ V) → (𝐸‘𝑋) = {𝑌, 𝑦}) |
91 | 86, 90 | jctird 565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐸‘𝑋) = {𝑦, 𝑌} ∧ 𝑌 ∈ V) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝑋) = {𝑌, 𝑦}))) |
92 | 69, 73, 91 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑦, 𝑏}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝑋) = {𝑌, 𝑦}))) |
93 | 92 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ((𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑦, 𝑏}) → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝑋) = {𝑌, 𝑦}))) |
94 | 93 | eximdv 1833 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (∃𝑦(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑦, 𝑏}) → ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝑋) = {𝑌, 𝑦}))) |
95 | 94, 56 | syl6ibr 241 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (∃𝑦(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑦, 𝑏}) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
96 | 95 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑦(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑦, 𝑏}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
97 | 65, 96 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑎(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
98 | 97 | exlimiv 1845 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑏∃𝑎(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
99 | 61, 98 | sylbi 206 |
. . . . . . . . . . . . . 14
⊢
(∃𝑎∃𝑏(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
100 | 60, 99 | jaoi 393 |
. . . . . . . . . . . . 13
⊢
((∃𝑎∃𝑏(𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ ∃𝑎∃𝑏(𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏})) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
101 | 22, 100 | sylbi 206 |
. . . . . . . . . . . 12
⊢
(∃𝑎∃𝑏((𝑌 = 𝑎 ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸‘𝑋) = {𝑎, 𝑏})) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
102 | 18, 101 | syl 17 |
. . . . . . . . . . 11
⊢
(∃𝑎∃𝑏(𝑌 ∈ (𝐸‘𝑋) ∧ (𝐸‘𝑋) = {𝑎, 𝑏}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
103 | 8, 102 | sylbir 224 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ (𝐸‘𝑋) ∧ ∃𝑎∃𝑏(𝐸‘𝑋) = {𝑎, 𝑏}) → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
104 | 103 | ex 449 |
. . . . . . . . 9
⊢ (𝑌 ∈ (𝐸‘𝑋) → (∃𝑎∃𝑏(𝐸‘𝑋) = {𝑎, 𝑏} → ((𝐸‘𝑋) ∈ 𝒫 𝑉 → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}))) |
105 | 104 | com13 86 |
. . . . . . . 8
⊢ ((𝐸‘𝑋) ∈ 𝒫 𝑉 → (∃𝑎∃𝑏(𝐸‘𝑋) = {𝑎, 𝑏} → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}))) |
106 | 105 | adantr 480 |
. . . . . . 7
⊢ (((𝐸‘𝑋) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑋)) = 2) → (∃𝑎∃𝑏(𝐸‘𝑋) = {𝑎, 𝑏} → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}))) |
107 | 7, 106 | mpd 15 |
. . . . . 6
⊢ (((𝐸‘𝑋) ∈ 𝒫 𝑉 ∧ (#‘(𝐸‘𝑋)) = 2) → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
108 | 6, 107 | sylbi 206 |
. . . . 5
⊢ ((𝐸‘𝑋) ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
109 | 3, 108 | syl 17 |
. . . 4
⊢ ((𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} ∧ 𝑋 ∈ dom 𝐸) → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦})) |
110 | 109 | ex 449 |
. . 3
⊢ (𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} → (𝑋 ∈ dom 𝐸 → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}))) |
111 | 1, 2, 110 | 3syl 18 |
. 2
⊢ (𝑉 USGrph 𝐸 → (𝑋 ∈ dom 𝐸 → (𝑌 ∈ (𝐸‘𝑋) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}))) |
112 | 111 | 3imp 1249 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ (𝐸‘𝑋)) → ∃𝑦 ∈ 𝑉 (𝐸‘𝑋) = {𝑌, 𝑦}) |