Proof of Theorem usgra2edg
Step | Hyp | Ref
| Expression |
1 | | usgrafun 25878 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
2 | | funfn 5833 |
. . . . . 6
⊢ (Fun
𝐸 ↔ 𝐸 Fn dom 𝐸) |
3 | 1, 2 | sylib 207 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → 𝐸 Fn dom 𝐸) |
4 | 3 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → 𝐸 Fn dom 𝐸) |
5 | | fvelrnb 6153 |
. . . . 5
⊢ (𝐸 Fn dom 𝐸 → ({𝑁, 𝑏} ∈ ran 𝐸 ↔ ∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑁, 𝑏})) |
6 | | fvelrnb 6153 |
. . . . 5
⊢ (𝐸 Fn dom 𝐸 → ({𝑐, 𝑁} ∈ ran 𝐸 ↔ ∃𝑦 ∈ dom 𝐸(𝐸‘𝑦) = {𝑐, 𝑁})) |
7 | 5, 6 | anbi12d 743 |
. . . 4
⊢ (𝐸 Fn dom 𝐸 → (({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸) ↔ (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑁, 𝑏} ∧ ∃𝑦 ∈ dom 𝐸(𝐸‘𝑦) = {𝑐, 𝑁}))) |
8 | 4, 7 | syl 17 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → (({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸) ↔ (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑁, 𝑏} ∧ ∃𝑦 ∈ dom 𝐸(𝐸‘𝑦) = {𝑐, 𝑁}))) |
9 | | reeanv 3086 |
. . . 4
⊢
(∃𝑥 ∈ dom
𝐸∃𝑦 ∈ dom 𝐸((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) ↔ (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑁, 𝑏} ∧ ∃𝑦 ∈ dom 𝐸(𝐸‘𝑦) = {𝑐, 𝑁})) |
10 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝐸‘𝑥) = (𝐸‘𝑦)) |
11 | 10 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝐸‘𝑥) = {𝑁, 𝑏} ↔ (𝐸‘𝑦) = {𝑁, 𝑏})) |
12 | 11 | anbi1d 737 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) ↔ ((𝐸‘𝑦) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}))) |
13 | | eqtr2 2630 |
. . . . . . . . . . . . . 14
⊢ (((𝐸‘𝑦) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) → {𝑁, 𝑏} = {𝑐, 𝑁}) |
14 | | prcom 4211 |
. . . . . . . . . . . . . . . 16
⊢ {𝑐, 𝑁} = {𝑁, 𝑐} |
15 | 14 | eqeq2i 2622 |
. . . . . . . . . . . . . . 15
⊢ ({𝑁, 𝑏} = {𝑐, 𝑁} ↔ {𝑁, 𝑏} = {𝑁, 𝑐}) |
16 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑏 ∈ V |
17 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑐 ∈ V |
18 | 16, 17 | preqr2 4321 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑁, 𝑏} = {𝑁, 𝑐} → 𝑏 = 𝑐) |
19 | | eqneqall 2793 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑐 → (𝑏 ≠ 𝑐 → 𝑥 ≠ 𝑦)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ({𝑁, 𝑏} = {𝑁, 𝑐} → (𝑏 ≠ 𝑐 → 𝑥 ≠ 𝑦)) |
21 | 15, 20 | sylbi 206 |
. . . . . . . . . . . . . 14
⊢ ({𝑁, 𝑏} = {𝑐, 𝑁} → (𝑏 ≠ 𝑐 → 𝑥 ≠ 𝑦)) |
22 | 13, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐸‘𝑦) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) → (𝑏 ≠ 𝑐 → 𝑥 ≠ 𝑦)) |
23 | 12, 22 | syl6bi 242 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) → (𝑏 ≠ 𝑐 → 𝑥 ≠ 𝑦))) |
24 | 23 | com23 84 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑏 ≠ 𝑐 → (((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) → 𝑥 ≠ 𝑦))) |
25 | 24 | impd 446 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑏 ≠ 𝑐 ∧ ((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁})) → 𝑥 ≠ 𝑦)) |
26 | | ax-1 6 |
. . . . . . . . . 10
⊢ (𝑥 ≠ 𝑦 → ((𝑏 ≠ 𝑐 ∧ ((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁})) → 𝑥 ≠ 𝑦)) |
27 | 25, 26 | pm2.61ine 2865 |
. . . . . . . . 9
⊢ ((𝑏 ≠ 𝑐 ∧ ((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁})) → 𝑥 ≠ 𝑦) |
28 | 27 | 3ad2antl3 1218 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) ∧ ((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁})) → 𝑥 ≠ 𝑦) |
29 | | prid1g 4239 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝑁, 𝑏}) |
30 | 29 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → 𝑁 ∈ {𝑁, 𝑏}) |
31 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ ((𝐸‘𝑥) = {𝑁, 𝑏} → (𝑁 ∈ (𝐸‘𝑥) ↔ 𝑁 ∈ {𝑁, 𝑏})) |
32 | 30, 31 | syl5ibr 235 |
. . . . . . . . . 10
⊢ ((𝐸‘𝑥) = {𝑁, 𝑏} → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → 𝑁 ∈ (𝐸‘𝑥))) |
33 | 32 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → 𝑁 ∈ (𝐸‘𝑥))) |
34 | 33 | impcom 445 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) ∧ ((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁})) → 𝑁 ∈ (𝐸‘𝑥)) |
35 | | prid2g 4240 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ 𝑉 → 𝑁 ∈ {𝑐, 𝑁}) |
36 | 35 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → 𝑁 ∈ {𝑐, 𝑁}) |
37 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ ((𝐸‘𝑦) = {𝑐, 𝑁} → (𝑁 ∈ (𝐸‘𝑦) ↔ 𝑁 ∈ {𝑐, 𝑁})) |
38 | 36, 37 | syl5ibr 235 |
. . . . . . . . . 10
⊢ ((𝐸‘𝑦) = {𝑐, 𝑁} → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → 𝑁 ∈ (𝐸‘𝑦))) |
39 | 38 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) → ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → 𝑁 ∈ (𝐸‘𝑦))) |
40 | 39 | impcom 445 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) ∧ ((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁})) → 𝑁 ∈ (𝐸‘𝑦)) |
41 | 28, 34, 40 | 3jca 1235 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) ∧ ((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁})) → (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑦))) |
42 | 41 | ex 449 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → (((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) → (𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑦)))) |
43 | 42 | reximdv 2999 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → (∃𝑦 ∈ dom 𝐸((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) → ∃𝑦 ∈ dom 𝐸(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑦)))) |
44 | 43 | reximdv 2999 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → (∃𝑥 ∈ dom 𝐸∃𝑦 ∈ dom 𝐸((𝐸‘𝑥) = {𝑁, 𝑏} ∧ (𝐸‘𝑦) = {𝑐, 𝑁}) → ∃𝑥 ∈ dom 𝐸∃𝑦 ∈ dom 𝐸(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑦)))) |
45 | 9, 44 | syl5bir 232 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → ((∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑁, 𝑏} ∧ ∃𝑦 ∈ dom 𝐸(𝐸‘𝑦) = {𝑐, 𝑁}) → ∃𝑥 ∈ dom 𝐸∃𝑦 ∈ dom 𝐸(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑦)))) |
46 | 8, 45 | sylbid 229 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) → (({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸) → ∃𝑥 ∈ dom 𝐸∃𝑦 ∈ dom 𝐸(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑦)))) |
47 | 46 | imp 444 |
1
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ 𝑏 ≠ 𝑐) ∧ ({𝑁, 𝑏} ∈ ran 𝐸 ∧ {𝑐, 𝑁} ∈ ran 𝐸)) → ∃𝑥 ∈ dom 𝐸∃𝑦 ∈ dom 𝐸(𝑥 ≠ 𝑦 ∧ 𝑁 ∈ (𝐸‘𝑥) ∧ 𝑁 ∈ (𝐸‘𝑦))) |