Proof of Theorem umgraex
Step | Hyp | Ref
| Expression |
1 | | umgran0 25849 |
. . . 4
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅) |
2 | | n0 3890 |
. . . 4
⊢ ((𝐸‘𝐹) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐸‘𝐹)) |
3 | 1, 2 | sylib 207 |
. . 3
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 𝑥 ∈ (𝐸‘𝐹)) |
4 | | umgrass 25848 |
. . . . . . 7
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ⊆ 𝑉) |
5 | 4 | sselda 3568 |
. . . . . 6
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → 𝑥 ∈ 𝑉) |
6 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → 𝑥 ∈ 𝑉) |
7 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → ((𝐸‘𝐹) ∖ {𝑥}) = ∅) |
8 | | ssdif0 3896 |
. . . . . . . . . 10
⊢ ((𝐸‘𝐹) ⊆ {𝑥} ↔ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) |
9 | 7, 8 | sylibr 223 |
. . . . . . . . 9
⊢ ((((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → (𝐸‘𝐹) ⊆ {𝑥}) |
10 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → 𝑥 ∈ (𝐸‘𝐹)) |
11 | 10 | snssd 4281 |
. . . . . . . . . 10
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → {𝑥} ⊆ (𝐸‘𝐹)) |
12 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → {𝑥} ⊆ (𝐸‘𝐹)) |
13 | 9, 12 | eqssd 3585 |
. . . . . . . 8
⊢ ((((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → (𝐸‘𝐹) = {𝑥}) |
14 | | preq2 4213 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → {𝑥, 𝑦} = {𝑥, 𝑥}) |
15 | | dfsn2 4138 |
. . . . . . . . . . 11
⊢ {𝑥} = {𝑥, 𝑥} |
16 | 14, 15 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → {𝑥, 𝑦} = {𝑥}) |
17 | 16 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝐸‘𝐹) = {𝑥, 𝑦} ↔ (𝐸‘𝐹) = {𝑥})) |
18 | 17 | rspcev 3282 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥}) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
19 | 6, 13, 18 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) = ∅) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
20 | | n0 3890 |
. . . . . . . 8
⊢ (((𝐸‘𝐹) ∖ {𝑥}) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) |
21 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) ⊆ 𝑉) |
22 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) |
23 | 22 | eldifad 3552 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ∈ (𝐸‘𝐹)) |
24 | 21, 23 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ∈ 𝑉) |
25 | | umgrafi 25851 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ∈ Fin) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) ∈ Fin) |
27 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑥 ∈ (𝐸‘𝐹)) |
28 | | prssi 4293 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ (𝐸‘𝐹)) → {𝑥, 𝑦} ⊆ (𝐸‘𝐹)) |
29 | 27, 23, 28 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} ⊆ (𝐸‘𝐹)) |
30 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸‘𝐹) ∈ V |
31 | | ssdomg 7887 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘𝐹) ∈ V → ({𝑥, 𝑦} ⊆ (𝐸‘𝐹) → {𝑥, 𝑦} ≼ (𝐸‘𝐹))) |
32 | 30, 29, 31 | mpsyl 66 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} ≼ (𝐸‘𝐹)) |
33 | | umgrale 25850 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (#‘(𝐸‘𝐹)) ≤ 2) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (#‘(𝐸‘𝐹)) ≤ 2) |
35 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}) → 𝑦 ≠ 𝑥) |
36 | 35 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑦 ≠ 𝑥) |
37 | 36 | necomd 2837 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → 𝑥 ≠ 𝑦) |
38 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
39 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
40 | | hashprgOLD 13044 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ≠ 𝑦 ↔ (#‘{𝑥, 𝑦}) = 2)) |
41 | 38, 39, 40 | mp2an 704 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ≠ 𝑦 ↔ (#‘{𝑥, 𝑦}) = 2) |
42 | 37, 41 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (#‘{𝑥, 𝑦}) = 2) |
43 | 34, 42 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (#‘(𝐸‘𝐹)) ≤ (#‘{𝑥, 𝑦})) |
44 | | prfi 8120 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥, 𝑦} ∈ Fin |
45 | | hashdom 13029 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐸‘𝐹) ∈ Fin ∧ {𝑥, 𝑦} ∈ Fin) → ((#‘(𝐸‘𝐹)) ≤ (#‘{𝑥, 𝑦}) ↔ (𝐸‘𝐹) ≼ {𝑥, 𝑦})) |
46 | 26, 44, 45 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → ((#‘(𝐸‘𝐹)) ≤ (#‘{𝑥, 𝑦}) ↔ (𝐸‘𝐹) ≼ {𝑥, 𝑦})) |
47 | 43, 46 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) ≼ {𝑥, 𝑦}) |
48 | | sbth 7965 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑥, 𝑦} ≼ (𝐸‘𝐹) ∧ (𝐸‘𝐹) ≼ {𝑥, 𝑦}) → {𝑥, 𝑦} ≈ (𝐸‘𝐹)) |
49 | 32, 47, 48 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} ≈ (𝐸‘𝐹)) |
50 | | fisseneq 8056 |
. . . . . . . . . . . . . . 15
⊢ (((𝐸‘𝐹) ∈ Fin ∧ {𝑥, 𝑦} ⊆ (𝐸‘𝐹) ∧ {𝑥, 𝑦} ≈ (𝐸‘𝐹)) → {𝑥, 𝑦} = (𝐸‘𝐹)) |
51 | 26, 29, 49, 50 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → {𝑥, 𝑦} = (𝐸‘𝐹)) |
52 | 51 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝐸‘𝐹) = {𝑥, 𝑦}) |
53 | 24, 52 | jca 553 |
. . . . . . . . . . . 12
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ (𝑥 ∈ (𝐸‘𝐹) ∧ 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}))) → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦})) |
54 | 53 | expr 641 |
. . . . . . . . . . 11
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → (𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}) → (𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦}))) |
55 | 54 | eximdv 1833 |
. . . . . . . . . 10
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → (∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥}) → ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦}))) |
56 | 55 | imp 444 |
. . . . . . . . 9
⊢ ((((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) → ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦})) |
57 | | df-rex 2902 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
𝑉 (𝐸‘𝐹) = {𝑥, 𝑦} ↔ ∃𝑦(𝑦 ∈ 𝑉 ∧ (𝐸‘𝐹) = {𝑥, 𝑦})) |
58 | 56, 57 | sylibr 223 |
. . . . . . . 8
⊢ ((((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ∃𝑦 𝑦 ∈ ((𝐸‘𝐹) ∖ {𝑥})) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
59 | 20, 58 | sylan2b 491 |
. . . . . . 7
⊢ ((((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) ∧ ((𝐸‘𝐹) ∖ {𝑥}) ≠ ∅) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
60 | 19, 59 | pm2.61dane 2869 |
. . . . . 6
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |
61 | 5, 60 | jca 553 |
. . . . 5
⊢ (((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝑥 ∈ (𝐸‘𝐹)) → (𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})) |
62 | 61 | ex 449 |
. . . 4
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝑥 ∈ (𝐸‘𝐹) → (𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}))) |
63 | 62 | eximdv 1833 |
. . 3
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (∃𝑥 𝑥 ∈ (𝐸‘𝐹) → ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}))) |
64 | 3, 63 | mpd 15 |
. 2
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})) |
65 | | df-rex 2902 |
. 2
⊢
(∃𝑥 ∈
𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦} ↔ ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})) |
66 | 64, 65 | sylibr 223 |
1
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) |