| 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 30321 |
. 2
⊢ (𝜑 → 𝐴:𝐷⟶𝑁) |
| 12 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐺 ∈ FriendGraph ) |
| 13 | 4 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑁 ↔ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) |
| 14 | 1 | nbgrisvtx 29358 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑌) → 𝑛 ∈ 𝑉) |
| 15 | 14 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ (𝐺 NeighbVtx 𝑌) → 𝑛 ∈ 𝑉)) |
| 16 | 13, 15 | biimtrid 242 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑁 → 𝑛 ∈ 𝑉)) |
| 17 | 16 | imp 406 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑛 ∈ 𝑉) |
| 18 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑋 ∈ 𝑉) |
| 19 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | frgrncvvdeqlem1 30318 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∉ 𝑁) |
| 20 | | df-nel 3047 |
. . . . . . . . . . 11
⊢ (𝑋 ∉ 𝑁 ↔ ¬ 𝑋 ∈ 𝑁) |
| 21 | | nelelne 3041 |
. . . . . . . . . . 11
⊢ (¬
𝑋 ∈ 𝑁 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
| 22 | 20, 21 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝑋 ∉ 𝑁 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
| 23 | 19, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
| 24 | 23 | imp 406 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑛 ≠ 𝑋) |
| 25 | 17, 18, 24 | 3jca 1129 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋)) |
| 26 | 12, 25 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (𝐺 ∈ FriendGraph ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋))) |
| 27 | 1, 2 | frcond2 30286 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph →
((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋) → ∃!𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
| 28 | 27 | imp 406 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋)) → ∃!𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) |
| 29 | | reurex 3384 |
. . . . . . 7
⊢
(∃!𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → ∃𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) |
| 30 | | df-rex 3071 |
. . . . . . 7
⊢
(∃𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) ↔ ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
| 31 | 29, 30 | sylib 218 |
. . . . . 6
⊢
(∃!𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
| 32 | 26, 28, 31 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
| 33 | | frgrusgr 30280 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈
USGraph) |
| 34 | 2 | nbusgreledg 29370 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ USGraph → (𝑚 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑚, 𝑋} ∈ 𝐸)) |
| 35 | 34 | bicomd 223 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → ({𝑚, 𝑋} ∈ 𝐸 ↔ 𝑚 ∈ (𝐺 NeighbVtx 𝑋))) |
| 36 | 9, 33, 35 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ({𝑚, 𝑋} ∈ 𝐸 ↔ 𝑚 ∈ (𝐺 NeighbVtx 𝑋))) |
| 37 | 36 | biimpa 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑚 ∈ (𝐺 NeighbVtx 𝑋)) |
| 38 | 3 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ 𝐷 ↔ 𝑚 ∈ (𝐺 NeighbVtx 𝑋)) |
| 39 | 37, 38 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑚 ∈ 𝐷) |
| 40 | 39 | ad2ant2rl 749 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑁) ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → 𝑚 ∈ 𝐷) |
| 41 | 2 | nbusgreledg 29370 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) ↔ {𝑛, 𝑚} ∈ 𝐸)) |
| 42 | 41 | biimpar 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ {𝑛, 𝑚} ∈ 𝐸) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚)) |
| 43 | 42 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ USGraph ∧ {𝑛, 𝑚} ∈ 𝐸) → ({𝑚, 𝑋} ∈ 𝐸 → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
| 44 | 43 | expimpd 453 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
| 45 | 9, 33, 44 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
| 47 | 46 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑁) ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚)) |
| 48 | | elin 3967 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) ↔ (𝑛 ∈ (𝐺 NeighbVtx 𝑚) ∧ 𝑛 ∈ 𝑁)) |
| 49 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝜑) |
| 50 | 49, 39 | jca 511 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝜑 ∧ 𝑚 ∈ 𝐷)) |
| 51 | | preq1 4733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑚 → {𝑥, 𝑦} = {𝑚, 𝑦}) |
| 52 | 51 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑚 → ({𝑥, 𝑦} ∈ 𝐸 ↔ {𝑚, 𝑦} ∈ 𝐸)) |
| 53 | 52 | riotabidv 7390 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑚 → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ 𝐸)) |
| 54 | 53 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) = (𝑚 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ 𝐸)) |
| 55 | 10, 54 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐴 = (𝑚 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ 𝐸)) |
| 56 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 55 | frgrncvvdeqlem5 30322 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐷) → {(𝐴‘𝑚)} = ((𝐺 NeighbVtx 𝑚) ∩ 𝑁)) |
| 57 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 NeighbVtx 𝑚) ∩ 𝑁) = {(𝐴‘𝑚)} → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) ↔ 𝑛 ∈ {(𝐴‘𝑚)})) |
| 58 | 57 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({(𝐴‘𝑚)} = ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) ↔ 𝑛 ∈ {(𝐴‘𝑚)})) |
| 59 | | elsni 4643 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ {(𝐴‘𝑚)} → 𝑛 = (𝐴‘𝑚)) |
| 60 | 58, 59 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({(𝐴‘𝑚)} = ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚))) |
| 61 | 50, 56, 60 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚))) |
| 62 | 61 | expcom 413 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑚, 𝑋} ∈ 𝐸 → (𝜑 → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚)))) |
| 63 | 62 | com3r 87 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → ({𝑚, 𝑋} ∈ 𝐸 → (𝜑 → 𝑛 = (𝐴‘𝑚)))) |
| 64 | 48, 63 | sylbir 235 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (𝐺 NeighbVtx 𝑚) ∧ 𝑛 ∈ 𝑁) → ({𝑚, 𝑋} ∈ 𝐸 → (𝜑 → 𝑛 = (𝐴‘𝑚)))) |
| 65 | 64 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → (𝑛 ∈ 𝑁 → ({𝑚, 𝑋} ∈ 𝐸 → (𝜑 → 𝑛 = (𝐴‘𝑚))))) |
| 66 | 65 | com14 96 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑛 ∈ 𝑁 → ({𝑚, 𝑋} ∈ 𝐸 → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → 𝑛 = (𝐴‘𝑚))))) |
| 67 | 66 | imp 406 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ({𝑚, 𝑋} ∈ 𝐸 → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → 𝑛 = (𝐴‘𝑚)))) |
| 68 | 67 | adantld 490 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → 𝑛 = (𝐴‘𝑚)))) |
| 69 | 68 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑁) ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → 𝑛 = (𝐴‘𝑚))) |
| 70 | 47, 69 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑁) ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → 𝑛 = (𝐴‘𝑚)) |
| 71 | 40, 70 | jca 511 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑁) ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
| 72 | 71 | ex 412 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
| 73 | 72 | adantld 490 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
| 74 | 73 | eximdv 1917 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
| 75 | 32, 74 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
| 76 | | df-rex 3071 |
. . . 4
⊢
(∃𝑚 ∈
𝐷 𝑛 = (𝐴‘𝑚) ↔ ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
| 77 | 75, 76 | sylibr 234 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚)) |
| 78 | 77 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚)) |
| 79 | | dffo3 7122 |
. 2
⊢ (𝐴:𝐷–onto→𝑁 ↔ (𝐴:𝐷⟶𝑁 ∧ ∀𝑛 ∈ 𝑁 ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚))) |
| 80 | 11, 78, 79 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐴:𝐷–onto→𝑁) |