Step | Hyp | Ref
| Expression |
1 | | frgrncvvdeq.v1 |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | frgrncvvdeq.e |
. . 3
⊢ 𝐸 = (Edg‘𝐺) |
3 | | frgrncvvdeq.nx |
. . 3
⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) |
4 | | frgrncvvdeq.ny |
. . 3
⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) |
5 | | frgrncvvdeq.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
6 | | frgrncvvdeq.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
7 | | frgrncvvdeq.ne |
. . 3
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
8 | | frgrncvvdeq.xy |
. . 3
⊢ (𝜑 → 𝑌 ∉ 𝐷) |
9 | | frgrncvvdeq.f |
. . 3
⊢ (𝜑 → 𝐺 ∈ FriendGraph ) |
10 | | frgrncvvdeq.a |
. . 3
⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | frgrncvvdeqlem4 27166 |
. 2
⊢ (𝜑 → 𝐴:𝐷⟶𝑁) |
12 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐺 ∈ FriendGraph ) |
13 | 4 | eleq2i 2693 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑁 ↔ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) |
14 | | frgrusgr 27124 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
15 | 1 | nbgrisvtx 26255 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ USGraph ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) → 𝑛 ∈ 𝑉) |
16 | 15 | ex 450 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑌) → 𝑛 ∈ 𝑉)) |
17 | 9, 14, 16 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ (𝐺 NeighbVtx 𝑌) → 𝑛 ∈ 𝑉)) |
18 | 13, 17 | syl5bi 232 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑁 → 𝑛 ∈ 𝑉)) |
19 | 18 | imp 445 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑛 ∈ 𝑉) |
20 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑋 ∈ 𝑉) |
21 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | frgrncvvdeqlem1 27163 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∉ 𝑁) |
22 | | df-nel 2898 |
. . . . . . . . . . 11
⊢ (𝑋 ∉ 𝑁 ↔ ¬ 𝑋 ∈ 𝑁) |
23 | | nelelne 2892 |
. . . . . . . . . . 11
⊢ (¬
𝑋 ∈ 𝑁 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
24 | 22, 23 | sylbi 207 |
. . . . . . . . . 10
⊢ (𝑋 ∉ 𝑁 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
25 | 21, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
26 | 25 | imp 445 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑛 ≠ 𝑋) |
27 | 19, 20, 26 | 3jca 1242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋)) |
28 | 12, 27 | jca 554 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (𝐺 ∈ FriendGraph ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋))) |
29 | 1, 2 | frcond2 27131 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph →
((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋) → ∃!𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
30 | 29 | imp 445 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋)) → ∃!𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) |
31 | | reurex 3160 |
. . . . . . 7
⊢
(∃!𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → ∃𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) |
32 | | df-rex 2918 |
. . . . . . 7
⊢
(∃𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) ↔ ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
33 | 31, 32 | sylib 208 |
. . . . . 6
⊢
(∃!𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
34 | 28, 30, 33 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
35 | 2 | nbusgreledg 26249 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ USGraph → (𝑚 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑚, 𝑋} ∈ 𝐸)) |
36 | 35 | bicomd 213 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → ({𝑚, 𝑋} ∈ 𝐸 ↔ 𝑚 ∈ (𝐺 NeighbVtx 𝑋))) |
37 | 9, 14, 36 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ({𝑚, 𝑋} ∈ 𝐸 ↔ 𝑚 ∈ (𝐺 NeighbVtx 𝑋))) |
38 | 37 | biimpa 501 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑚 ∈ (𝐺 NeighbVtx 𝑋)) |
39 | 3 | eleq2i 2693 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ 𝐷 ↔ 𝑚 ∈ (𝐺 NeighbVtx 𝑋)) |
40 | 38, 39 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑚 ∈ 𝐷) |
41 | 40 | ad2ant2rl 785 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑁) ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → 𝑚 ∈ 𝐷) |
42 | 2 | nbusgreledg 26249 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) ↔ {𝑛, 𝑚} ∈ 𝐸)) |
43 | 42 | biimpar 502 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ {𝑛, 𝑚} ∈ 𝐸) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚)) |
44 | 43 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ USGraph ∧ {𝑛, 𝑚} ∈ 𝐸) → ({𝑚, 𝑋} ∈ 𝐸 → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
45 | 44 | expimpd 629 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
46 | 9, 14, 45 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
47 | 46 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
48 | 47 | imp 445 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑁) ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚)) |
49 | | elin 3796 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) ↔ (𝑛 ∈ (𝐺 NeighbVtx 𝑚) ∧ 𝑛 ∈ 𝑁)) |
50 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝜑) |
51 | 50, 40 | jca 554 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝜑 ∧ 𝑚 ∈ 𝐷)) |
52 | | preq1 4268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑚 → {𝑥, 𝑦} = {𝑚, 𝑦}) |
53 | 52 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑚 → ({𝑥, 𝑦} ∈ 𝐸 ↔ {𝑚, 𝑦} ∈ 𝐸)) |
54 | 53 | riotabidv 6613 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑚 → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ 𝐸)) |
55 | 54 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) = (𝑚 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ 𝐸)) |
56 | 10, 55 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐴 = (𝑚 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ 𝐸)) |
57 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 56 | frgrncvvdeqlem5 27167 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐷) → {(𝐴‘𝑚)} = ((𝐺 NeighbVtx 𝑚) ∩ 𝑁)) |
58 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 NeighbVtx 𝑚) ∩ 𝑁) = {(𝐴‘𝑚)} → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) ↔ 𝑛 ∈ {(𝐴‘𝑚)})) |
59 | 58 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({(𝐴‘𝑚)} = ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) ↔ 𝑛 ∈ {(𝐴‘𝑚)})) |
60 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ {(𝐴‘𝑚)} → 𝑛 = (𝐴‘𝑚)) |
61 | 59, 60 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({(𝐴‘𝑚)} = ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚))) |
62 | 51, 57, 61 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚))) |
63 | 62 | expcom 451 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑚, 𝑋} ∈ 𝐸 → (𝜑 → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚)))) |
64 | 63 | com3r 87 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → ({𝑚, 𝑋} ∈ 𝐸 → (𝜑 → 𝑛 = (𝐴‘𝑚)))) |
65 | 49, 64 | sylbir 225 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (𝐺 NeighbVtx 𝑚) ∧ 𝑛 ∈ 𝑁) → ({𝑚, 𝑋} ∈ 𝐸 → (𝜑 → 𝑛 = (𝐴‘𝑚)))) |
66 | 65 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → (𝑛 ∈ 𝑁 → ({𝑚, 𝑋} ∈ 𝐸 → (𝜑 → 𝑛 = (𝐴‘𝑚))))) |
67 | 66 | com14 96 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑛 ∈ 𝑁 → ({𝑚, 𝑋} ∈ 𝐸 → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → 𝑛 = (𝐴‘𝑚))))) |
68 | 67 | imp 445 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ({𝑚, 𝑋} ∈ 𝐸 → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → 𝑛 = (𝐴‘𝑚)))) |
69 | 68 | adantld 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → 𝑛 = (𝐴‘𝑚)))) |
70 | 69 | imp 445 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑁) ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → 𝑛 = (𝐴‘𝑚))) |
71 | 48, 70 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑁) ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → 𝑛 = (𝐴‘𝑚)) |
72 | 41, 71 | jca 554 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑁) ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
73 | 72 | ex 450 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
74 | 73 | adantld 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
75 | 74 | eximdv 1846 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
76 | 34, 75 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
77 | | df-rex 2918 |
. . . 4
⊢
(∃𝑚 ∈
𝐷 𝑛 = (𝐴‘𝑚) ↔ ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
78 | 76, 77 | sylibr 224 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚)) |
79 | 78 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚)) |
80 | | dffo3 6374 |
. 2
⊢ (𝐴:𝐷–onto→𝑁 ↔ (𝐴:𝐷⟶𝑁 ∧ ∀𝑛 ∈ 𝑁 ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚))) |
81 | 11, 79, 80 | sylanbrc 698 |
1
⊢ (𝜑 → 𝐴:𝐷–onto→𝑁) |