Proof of Theorem upgrex
Step | Hyp | Ref
| Expression |
1 | | isupgr.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | isupgr.e |
. . . . 5
⊢ 𝐸 = (iEdg‘𝐺) |
3 | 1, 2 | upgrn0 25756 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅) |
4 | | n0 3890 |
. . . 4
⊢ ((𝐸‘𝐹) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐸‘𝐹)) |
5 | 3, 4 | sylib 207 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 𝑥 ∈ (𝐸‘𝐹)) |
6 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → 𝐺 ∈ UPGraph ) |
7 | | fndm 5904 |
. . . . . . . . . . . . 13
⊢ (𝐸 Fn 𝐴 → dom 𝐸 = 𝐴) |
8 | 7 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ (𝐸 Fn 𝐴 → 𝐴 = dom 𝐸) |
9 | 8 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝐸 Fn 𝐴 → (𝐹 ∈ 𝐴 ↔ 𝐹 ∈ dom 𝐸)) |
10 | 9 | biimpd 218 |
. . . . . . . . . 10
⊢ (𝐸 Fn 𝐴 → (𝐹 ∈ 𝐴 → 𝐹 ∈ dom 𝐸)) |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (𝐺 ∈ UPGraph → (𝐸 Fn 𝐴 → (𝐹 ∈ 𝐴 → 𝐹 ∈ dom 𝐸))) |
12 | 11 | 3imp 1249 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → 𝐹 ∈ dom 𝐸) |
13 | 1, 2 | upgrss 25755 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉) |
14 | 6, 12, 13 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ⊆ 𝑉) |
15 | 14 | sselda 3568 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → 𝑥 ∈ 𝑉) |
16 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → 𝑥 ∈ 𝑉) |
17 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → ((𝐸‘𝐹) ∖ {𝑥}) = ∅) |
18 | | ssdif0 3896 |
. . . . . . . . . 10
⊢ ((𝐸‘𝐹) ⊆ {𝑥} ↔ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) |
19 | 17, 18 | sylibr 223 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → (𝐸‘𝐹) ⊆ {𝑥}) |
20 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → 𝑥 ∈ (𝐸‘𝐹)) |
21 | 20 | snssd 4281 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → {𝑥} ⊆ (𝐸‘𝐹)) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → {𝑥} ⊆ (𝐸‘𝐹)) |
23 | 19, 22 | eqssd 3585 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → (𝐸‘𝐹) = {𝑥}) |
24 | | preq2 4213 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → {𝑥, 𝑦} = {𝑥, 𝑥}) |
25 | | dfsn2 4138 |
. . . . . . . . . . 11
⊢ {𝑥} = {𝑥, 𝑥} |
26 | 24, 25 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → {𝑥, 𝑦} = {𝑥}) |
27 | 26 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝐸‘𝐹) = {𝑥, 𝑦} ↔ (𝐸‘𝐹) = {𝑥})) |
28 | 27 | rspcev 3282 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥}) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
29 | 16, 23, 28 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
30 | | n0 3890 |
. . . . . . . 8
⊢ (((𝐸‘𝐹) ∖ {𝑥}) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) |
31 | 14 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) ⊆ 𝑉) |
32 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) |
33 | 32 | eldifad 3552 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ∈ (𝐸‘𝐹)) |
34 | 31, 33 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ∈ 𝑉) |
35 | 1, 2 | upgrfi 25758 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ∈ Fin) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) ∈ Fin) |
37 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑥 ∈ (𝐸‘𝐹)) |
38 | 37, 33 | prssd 4294 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} ⊆ (𝐸‘𝐹)) |
39 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸‘𝐹) ∈ V |
40 | | ssdomg 7887 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘𝐹) ∈ V → ({𝑥, 𝑦} ⊆ (𝐸‘𝐹) → {𝑥, 𝑦} ≼ (𝐸‘𝐹))) |
41 | 39, 38, 40 | mpsyl 66 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} ≼ (𝐸‘𝐹)) |
42 | 1, 2 | upgrle 25757 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (#‘(𝐸‘𝐹)) ≤ 2) |
43 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (#‘(𝐸‘𝐹)) ≤ 2) |
44 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}) → 𝑦 ≠ 𝑥) |
45 | 44 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ≠ 𝑥) |
46 | 45 | necomd 2837 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑥 ≠ 𝑦) |
47 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
48 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
49 | | hashprg 13043 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ≠ 𝑦 ↔ (#‘{𝑥, 𝑦}) = 2)) |
50 | 47, 48, 49 | mp2an 704 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ≠ 𝑦 ↔ (#‘{𝑥, 𝑦}) = 2) |
51 | 46, 50 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (#‘{𝑥, 𝑦}) = 2) |
52 | 43, 51 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (#‘(𝐸‘𝐹)) ≤ (#‘{𝑥, 𝑦})) |
53 | | prfi 8120 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥, 𝑦} ∈ Fin |
54 | | hashdom 13029 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐸‘𝐹) ∈ Fin ∧ {𝑥, 𝑦} ∈ Fin) → ((#‘(𝐸‘𝐹)) ≤ (#‘{𝑥, 𝑦}) ↔ (𝐸‘𝐹) ≼ {𝑥, 𝑦})) |
55 | 36, 53, 54 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → ((#‘(𝐸‘𝐹)) ≤ (#‘{𝑥, 𝑦}) ↔ (𝐸‘𝐹) ≼ {𝑥, 𝑦})) |
56 | 52, 55 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) ≼ {𝑥, 𝑦}) |
57 | | sbth 7965 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑥, 𝑦} ≼ (𝐸‘𝐹) ∧ (𝐸‘𝐹) ≼ {𝑥, 𝑦}) → {𝑥, 𝑦} ≈ (𝐸‘𝐹)) |
58 | 41, 56, 57 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} ≈ (𝐸‘𝐹)) |
59 | | fisseneq 8056 |
. . . . . . . . . . . . . . 15
⊢ (((𝐸‘𝐹) ∈ Fin ∧ {𝑥, 𝑦} ⊆ (𝐸‘𝐹) ∧ {𝑥, 𝑦} ≈ (𝐸‘𝐹)) → {𝑥, 𝑦} = (𝐸‘𝐹)) |
60 | 36, 38, 58, 59 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} = (𝐸‘𝐹)) |
61 | 60 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) = {𝑥, 𝑦}) |
62 | 34, 61 | jca 553 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦})) |
63 | 62 | expr 641 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → (𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}) → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦}))) |
64 | 63 | eximdv 1833 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → (∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}) → ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦}))) |
65 | 64 | imp 444 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) → ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦})) |
66 | | df-rex 2902 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
𝑉 (𝐸‘𝐹) = {𝑥, 𝑦} ↔ ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦})) |
67 | 65, 66 | sylibr 223 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
68 | 30, 67 | sylan2b 491 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) ≠ ∅) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
69 | 29, 68 | pm2.61dane 2869 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
70 | 15, 69 | jca 553 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → (𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})) |
71 | 70 | ex 449 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝑥 ∈ (𝐸‘𝐹) → (𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}))) |
72 | 71 | eximdv 1833 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (∃𝑥 𝑥 ∈ (𝐸‘𝐹) → ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}))) |
73 | 5, 72 | mpd 15 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})) |
74 | | df-rex 2902 |
. 2
⊢
(∃𝑥 ∈
𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦} ↔ ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})) |
75 | 73, 74 | sylibr 223 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |