Proof of Theorem uhgr2edg
Step | Hyp | Ref
| Expression |
1 | | simp1l 1078 |
. . . 4
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐺 ∈ UHGraph ) |
2 | | simp1r 1079 |
. . . 4
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴 ≠ 𝐵) |
3 | | simp23 1089 |
. . . . 5
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝑁 ∈ 𝑉) |
4 | | simp21 1087 |
. . . . 5
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → 𝐴 ∈ 𝑉) |
5 | | 3simpc 1053 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) |
6 | 5 | 3ad2ant2 1076 |
. . . . 5
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) |
7 | 3, 4, 6 | jca31 555 |
. . . 4
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
8 | 1, 2, 7 | jca31 555 |
. . 3
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))) |
9 | | simp3 1056 |
. . 3
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) |
10 | 8, 9 | jca 553 |
. 2
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸))) |
11 | | usgrf1oedg.e |
. . . . . . . . . 10
⊢ 𝐸 = (Edg‘𝐺) |
12 | 11 | a1i 11 |
. . . . . . . . 9
⊢ (𝐺 ∈ UHGraph → 𝐸 = (Edg‘𝐺)) |
13 | | edgaval 25794 |
. . . . . . . . 9
⊢ (𝐺 ∈ UHGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
14 | | usgrf1oedg.i |
. . . . . . . . . . . 12
⊢ 𝐼 = (iEdg‘𝐺) |
15 | 14 | eqcomi 2619 |
. . . . . . . . . . 11
⊢
(iEdg‘𝐺) =
𝐼 |
16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UHGraph →
(iEdg‘𝐺) = 𝐼) |
17 | 16 | rneqd 5274 |
. . . . . . . . 9
⊢ (𝐺 ∈ UHGraph → ran
(iEdg‘𝐺) = ran 𝐼) |
18 | 12, 13, 17 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝐺 ∈ UHGraph → 𝐸 = ran 𝐼) |
19 | 18 | eleq2d 2673 |
. . . . . . 7
⊢ (𝐺 ∈ UHGraph → ({𝑁, 𝐴} ∈ 𝐸 ↔ {𝑁, 𝐴} ∈ ran 𝐼)) |
20 | 18 | eleq2d 2673 |
. . . . . . 7
⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝑁} ∈ 𝐸 ↔ {𝐵, 𝑁} ∈ ran 𝐼)) |
21 | 19, 20 | anbi12d 743 |
. . . . . 6
⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ ({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼))) |
22 | | eqid 2610 |
. . . . . . . . . 10
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
23 | 22 | uhgrfun 25732 |
. . . . . . . . 9
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
24 | 14 | funeqi 5824 |
. . . . . . . . 9
⊢ (Fun
𝐼 ↔ Fun
(iEdg‘𝐺)) |
25 | 23, 24 | sylibr 223 |
. . . . . . . 8
⊢ (𝐺 ∈ UHGraph → Fun 𝐼) |
26 | | funfn 5833 |
. . . . . . . 8
⊢ (Fun
𝐼 ↔ 𝐼 Fn dom 𝐼) |
27 | 25, 26 | sylib 207 |
. . . . . . 7
⊢ (𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼) |
28 | | fvelrnb 6153 |
. . . . . . . 8
⊢ (𝐼 Fn dom 𝐼 → ({𝑁, 𝐴} ∈ ran 𝐼 ↔ ∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴})) |
29 | | fvelrnb 6153 |
. . . . . . . 8
⊢ (𝐼 Fn dom 𝐼 → ({𝐵, 𝑁} ∈ ran 𝐼 ↔ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})) |
30 | 28, 29 | anbi12d 743 |
. . . . . . 7
⊢ (𝐼 Fn dom 𝐼 → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}))) |
31 | 27, 30 | syl 17 |
. . . . . 6
⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ ran 𝐼 ∧ {𝐵, 𝑁} ∈ ran 𝐼) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}))) |
32 | 21, 31 | bitrd 267 |
. . . . 5
⊢ (𝐺 ∈ UHGraph → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}))) |
33 | 32 | ad2antrr 758 |
. . . 4
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}))) |
34 | | reeanv 3086 |
. . . . 5
⊢
(∃𝑥 ∈ dom
𝐼∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) ↔ (∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁})) |
35 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝐼‘𝑥) = (𝐼‘𝑦)) |
36 | 35 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝐼‘𝑥) = {𝑁, 𝐴} ↔ (𝐼‘𝑦) = {𝑁, 𝐴})) |
37 | 36 | anbi1d 737 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) ↔ ((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}))) |
38 | | eqtr2 2630 |
. . . . . . . . . . . . . 14
⊢ (((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → {𝑁, 𝐴} = {𝐵, 𝑁}) |
39 | | prcom 4211 |
. . . . . . . . . . . . . . . 16
⊢ {𝐵, 𝑁} = {𝑁, 𝐵} |
40 | 39 | eqeq2i 2622 |
. . . . . . . . . . . . . . 15
⊢ ({𝑁, 𝐴} = {𝐵, 𝑁} ↔ {𝑁, 𝐴} = {𝑁, 𝐵}) |
41 | | preq12bg 4326 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑁 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁)))) |
42 | 41 | ancom2s 840 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} ↔ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁)))) |
43 | | eqneqall 2793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦)) |
44 | 43 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦)) |
45 | | eqtr 2629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 = 𝑁 ∧ 𝑁 = 𝐵) → 𝐴 = 𝐵) |
46 | 45 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 = 𝐵 ∧ 𝐴 = 𝑁) → 𝐴 = 𝐵) |
47 | 46, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 = 𝐵 ∧ 𝐴 = 𝑁) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦)) |
48 | 44, 47 | jaoi 393 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁)) → (𝐴 ≠ 𝐵 → 𝑥 ≠ 𝑦)) |
49 | 48 | adantld 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 = 𝑁 ∧ 𝐴 = 𝐵) ∨ (𝑁 = 𝐵 ∧ 𝐴 = 𝑁)) → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → 𝑥 ≠ 𝑦)) |
50 | 42, 49 | syl6bi 242 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → 𝑥 ≠ 𝑦))) |
51 | 50 | com3l 87 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑁, 𝐴} = {𝑁, 𝐵} → ((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) → (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑥 ≠ 𝑦))) |
52 | 51 | impd 446 |
. . . . . . . . . . . . . . 15
⊢ ({𝑁, 𝐴} = {𝑁, 𝐵} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦)) |
53 | 40, 52 | sylbi 206 |
. . . . . . . . . . . . . 14
⊢ ({𝑁, 𝐴} = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦)) |
54 | 38, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐼‘𝑦) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦)) |
55 | 37, 54 | syl6bi 242 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑥 ≠ 𝑦))) |
56 | 55 | com23 84 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → 𝑥 ≠ 𝑦))) |
57 | 56 | impd 446 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦)) |
58 | | ax-1 6 |
. . . . . . . . . 10
⊢ (𝑥 ≠ 𝑦 → ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦)) |
59 | 57, 58 | pm2.61ine 2865 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑥 ≠ 𝑦) |
60 | | prid1g 4239 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝑁, 𝐴}) |
61 | 60 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑁 ∈ {𝑁, 𝐴}) |
62 | 61 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ {𝑁, 𝐴}) |
63 | | eleq2 2677 |
. . . . . . . . . . . 12
⊢ ((𝐼‘𝑥) = {𝑁, 𝐴} → (𝑁 ∈ (𝐼‘𝑥) ↔ 𝑁 ∈ {𝑁, 𝐴})) |
64 | 62, 63 | syl5ibr 235 |
. . . . . . . . . . 11
⊢ ((𝐼‘𝑥) = {𝑁, 𝐴} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑥))) |
65 | 64 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑥))) |
66 | 65 | impcom 445 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼‘𝑥)) |
67 | | prid2g 4240 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝐵, 𝑁}) |
68 | 67 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) → 𝑁 ∈ {𝐵, 𝑁}) |
69 | 68 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ {𝐵, 𝑁}) |
70 | | eleq2 2677 |
. . . . . . . . . . . 12
⊢ ((𝐼‘𝑦) = {𝐵, 𝑁} → (𝑁 ∈ (𝐼‘𝑦) ↔ 𝑁 ∈ {𝐵, 𝑁})) |
71 | 69, 70 | syl5ibr 235 |
. . . . . . . . . . 11
⊢ ((𝐼‘𝑦) = {𝐵, 𝑁} → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑦))) |
72 | 71 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → 𝑁 ∈ (𝐼‘𝑦))) |
73 | 72 | impcom 445 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → 𝑁 ∈ (𝐼‘𝑦)) |
74 | 59, 66, 73 | 3jca 1235 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁})) → (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))) |
75 | 74 | ex 449 |
. . . . . . 7
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))) |
76 | 75 | reximdv 2999 |
. . . . . 6
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))) |
77 | 76 | reximdv 2999 |
. . . . 5
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼((𝐼‘𝑥) = {𝑁, 𝐴} ∧ (𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))) |
78 | 34, 77 | syl5bir 232 |
. . . 4
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → ((∃𝑥 ∈ dom 𝐼(𝐼‘𝑥) = {𝑁, 𝐴} ∧ ∃𝑦 ∈ dom 𝐼(𝐼‘𝑦) = {𝐵, 𝑁}) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))) |
79 | 33, 78 | sylbid 229 |
. . 3
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) → (({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦)))) |
80 | 79 | imp 444 |
. 2
⊢ ((((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ ((𝑁 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))) |
81 | 10, 80 | syl 17 |
1
⊢ (((𝐺 ∈ UHGraph ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ ({𝑁, 𝐴} ∈ 𝐸 ∧ {𝐵, 𝑁} ∈ 𝐸)) → ∃𝑥 ∈ dom 𝐼∃𝑦 ∈ dom 𝐼(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐼‘𝑥) ∧ 𝑁 ∈ (𝐼‘𝑦))) |