Proof of Theorem upgrex
Step | Hyp | Ref
| Expression |
1 | | isupgr.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | isupgr.e |
. . . . 5
⊢ 𝐸 = (iEdg‘𝐺) |
3 | 1, 2 | upgrn0 25984 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅) |
4 | | n0 3931 |
. . . 4
⊢ ((𝐸‘𝐹) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐸‘𝐹)) |
5 | 3, 4 | sylib 208 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 𝑥 ∈ (𝐸‘𝐹)) |
6 | | simp1 1061 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → 𝐺 ∈ UPGraph ) |
7 | | fndm 5990 |
. . . . . . . . . . . . 13
⊢ (𝐸 Fn 𝐴 → dom 𝐸 = 𝐴) |
8 | 7 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ (𝐸 Fn 𝐴 → 𝐴 = dom 𝐸) |
9 | 8 | eleq2d 2687 |
. . . . . . . . . . 11
⊢ (𝐸 Fn 𝐴 → (𝐹 ∈ 𝐴 ↔ 𝐹 ∈ dom 𝐸)) |
10 | 9 | biimpd 219 |
. . . . . . . . . 10
⊢ (𝐸 Fn 𝐴 → (𝐹 ∈ 𝐴 → 𝐹 ∈ dom 𝐸)) |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (𝐺 ∈ UPGraph → (𝐸 Fn 𝐴 → (𝐹 ∈ 𝐴 → 𝐹 ∈ dom 𝐸))) |
12 | 11 | 3imp 1256 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → 𝐹 ∈ dom 𝐸) |
13 | 1, 2 | upgrss 25983 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉) |
14 | 6, 12, 13 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ⊆ 𝑉) |
15 | 14 | sselda 3603 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → 𝑥 ∈ 𝑉) |
16 | 15 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → 𝑥 ∈ 𝑉) |
17 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → ((𝐸‘𝐹) ∖ {𝑥}) = ∅) |
18 | | ssdif0 3942 |
. . . . . . . . . 10
⊢ ((𝐸‘𝐹) ⊆ {𝑥} ↔ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) |
19 | 17, 18 | sylibr 224 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → (𝐸‘𝐹) ⊆ {𝑥}) |
20 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → 𝑥 ∈ (𝐸‘𝐹)) |
21 | 20 | snssd 4340 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → {𝑥} ⊆ (𝐸‘𝐹)) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → {𝑥} ⊆ (𝐸‘𝐹)) |
23 | 19, 22 | eqssd 3620 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → (𝐸‘𝐹) = {𝑥}) |
24 | | preq2 4269 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → {𝑥, 𝑦} = {𝑥, 𝑥}) |
25 | | dfsn2 4190 |
. . . . . . . . . . 11
⊢ {𝑥} = {𝑥, 𝑥} |
26 | 24, 25 | syl6eqr 2674 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → {𝑥, 𝑦} = {𝑥}) |
27 | 26 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝐸‘𝐹) = {𝑥, 𝑦} ↔ (𝐸‘𝐹) = {𝑥})) |
28 | 27 | rspcev 3309 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥}) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
29 | 16, 23, 28 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
30 | | n0 3931 |
. . . . . . . 8
⊢ (((𝐸‘𝐹) ∖ {𝑥}) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) |
31 | 14 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) ⊆ 𝑉) |
32 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) |
33 | 32 | eldifad 3586 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ∈ (𝐸‘𝐹)) |
34 | 31, 33 | sseldd 3604 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ∈ 𝑉) |
35 | 1, 2 | upgrfi 25986 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ∈ Fin) |
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) ∈ Fin) |
37 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑥 ∈ (𝐸‘𝐹)) |
38 | 37, 33 | prssd 4354 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} ⊆ (𝐸‘𝐹)) |
39 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸‘𝐹) ∈ V |
40 | | ssdomg 8001 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘𝐹) ∈ V → ({𝑥, 𝑦} ⊆ (𝐸‘𝐹) → {𝑥, 𝑦} ≼ (𝐸‘𝐹))) |
41 | 39, 38, 40 | mpsyl 68 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} ≼ (𝐸‘𝐹)) |
42 | 1, 2 | upgrle 25985 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (#‘(𝐸‘𝐹)) ≤ 2) |
43 | 42 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (#‘(𝐸‘𝐹)) ≤ 2) |
44 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}) → 𝑦 ≠ 𝑥) |
45 | 44 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ≠ 𝑥) |
46 | 45 | necomd 2849 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑥 ≠ 𝑦) |
47 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
48 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
49 | | hashprg 13182 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ≠ 𝑦 ↔ (#‘{𝑥, 𝑦}) = 2)) |
50 | 47, 48, 49 | mp2an 708 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ≠ 𝑦 ↔ (#‘{𝑥, 𝑦}) = 2) |
51 | 46, 50 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (#‘{𝑥, 𝑦}) = 2) |
52 | 43, 51 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (#‘(𝐸‘𝐹)) ≤ (#‘{𝑥, 𝑦})) |
53 | | prfi 8235 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥, 𝑦} ∈ Fin |
54 | | hashdom 13168 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐸‘𝐹) ∈ Fin ∧ {𝑥, 𝑦} ∈ Fin) → ((#‘(𝐸‘𝐹)) ≤ (#‘{𝑥, 𝑦}) ↔ (𝐸‘𝐹) ≼ {𝑥, 𝑦})) |
55 | 36, 53, 54 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → ((#‘(𝐸‘𝐹)) ≤ (#‘{𝑥, 𝑦}) ↔ (𝐸‘𝐹) ≼ {𝑥, 𝑦})) |
56 | 52, 55 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) ≼ {𝑥, 𝑦}) |
57 | | sbth 8080 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑥, 𝑦} ≼ (𝐸‘𝐹) ∧ (𝐸‘𝐹) ≼ {𝑥, 𝑦}) → {𝑥, 𝑦} ≈ (𝐸‘𝐹)) |
58 | 41, 56, 57 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} ≈ (𝐸‘𝐹)) |
59 | | fisseneq 8171 |
. . . . . . . . . . . . . . 15
⊢ (((𝐸‘𝐹) ∈ Fin ∧ {𝑥, 𝑦} ⊆ (𝐸‘𝐹) ∧ {𝑥, 𝑦} ≈ (𝐸‘𝐹)) → {𝑥, 𝑦} = (𝐸‘𝐹)) |
60 | 36, 38, 58, 59 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} = (𝐸‘𝐹)) |
61 | 60 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) = {𝑥, 𝑦}) |
62 | 34, 61 | jca 554 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦})) |
63 | 62 | expr 643 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → (𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}) → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦}))) |
64 | 63 | eximdv 1846 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → (∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}) → ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦}))) |
65 | 64 | imp 445 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) → ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦})) |
66 | | df-rex 2918 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
𝑉 (𝐸‘𝐹) = {𝑥, 𝑦} ↔ ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦})) |
67 | 65, 66 | sylibr 224 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
68 | 30, 67 | sylan2b 492 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) ≠ ∅) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
69 | 29, 68 | pm2.61dane 2881 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
70 | 15, 69 | jca 554 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → (𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})) |
71 | 70 | ex 450 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝑥 ∈ (𝐸‘𝐹) → (𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}))) |
72 | 71 | eximdv 1846 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (∃𝑥 𝑥 ∈ (𝐸‘𝐹) → ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}))) |
73 | 5, 72 | mpd 15 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})) |
74 | | df-rex 2918 |
. 2
⊢
(∃𝑥 ∈
𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦} ↔ ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})) |
75 | 73, 74 | sylibr 224 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |