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 | frgrncvvdeqlem5 41473 |
. 2
⊢ (𝜑 → 𝐴:𝐷⟶𝑁) |
12 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐺 ∈ FriendGraph ) |
13 | 4 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑁 ↔ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) |
14 | | frgrusgr 41432 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
15 | 1 | nbgrisvtx 40581 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ USGraph ∧ 𝑛 ∈ (𝐺 NeighbVtx 𝑌)) → 𝑛 ∈ 𝑉) |
16 | 15 | ex 449 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑌) → 𝑛 ∈ 𝑉)) |
17 | 9, 14, 16 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ (𝐺 NeighbVtx 𝑌) → 𝑛 ∈ 𝑉)) |
18 | 13, 17 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑁 → 𝑛 ∈ 𝑉)) |
19 | 18 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑛 ∈ 𝑉) |
20 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑋 ∈ 𝑉) |
21 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | frgrncvvdeqlem2 41470 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∉ 𝑁) |
22 | | df-nel 2783 |
. . . . . . . . . . 11
⊢ (𝑋 ∉ 𝑁 ↔ ¬ 𝑋 ∈ 𝑁) |
23 | | nelelne 2880 |
. . . . . . . . . . 11
⊢ (¬
𝑋 ∈ 𝑁 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
24 | 22, 23 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝑋 ∉ 𝑁 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
25 | 21, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
26 | 25 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑛 ≠ 𝑋) |
27 | 19, 20, 26 | 3jca 1235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋)) |
28 | 12, 27 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (𝐺 ∈ FriendGraph ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋))) |
29 | 1, 2 | frcond2 41439 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph →
((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋) → ∃!𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
30 | 29 | imp 444 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋)) → ∃!𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) |
31 | | reurex 3137 |
. . . . . . 7
⊢
(∃!𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → ∃𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) |
32 | | df-rex 2902 |
. . . . . . 7
⊢
(∃𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) ↔ ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
33 | 31, 32 | sylib 207 |
. . . . . 6
⊢
(∃!𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
34 | 28, 30, 33 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) |
35 | 9, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ USGraph ) |
36 | | simprrr 801 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) → {𝑚, 𝑋} ∈ 𝐸) |
37 | 3 | eleq2i 2680 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ 𝐷 ↔ 𝑚 ∈ (𝐺 NeighbVtx 𝑋)) |
38 | 2 | nbusgreledg 40575 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ USGraph → (𝑚 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑚, 𝑋} ∈ 𝐸)) |
39 | 38 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ 𝑛 ∈ 𝑁) → (𝑚 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑚, 𝑋} ∈ 𝐸)) |
40 | 39 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) → (𝑚 ∈ (𝐺 NeighbVtx 𝑋) ↔ {𝑚, 𝑋} ∈ 𝐸)) |
41 | 37, 40 | syl5bb 271 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) → (𝑚 ∈ 𝐷 ↔ {𝑚, 𝑋} ∈ 𝐸)) |
42 | 36, 41 | mpbird 246 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) → 𝑚 ∈ 𝐷) |
43 | 2 | nbusgreledg 40575 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ USGraph → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) ↔ {𝑛, 𝑚} ∈ 𝐸)) |
44 | 43 | biimprcd 239 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑛, 𝑚} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝐺 ∈ USGraph → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝐺 ∈ USGraph → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
47 | 46 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
48 | 47 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ 𝑛 ∈ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚))) |
49 | 48 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) → 𝑛 ∈ (𝐺 NeighbVtx 𝑚)) |
50 | | elin 3758 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) ↔ (𝑛 ∈ (𝐺 NeighbVtx 𝑚) ∧ 𝑛 ∈ 𝑁)) |
51 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝜑) |
52 | 38 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 ∈ USGraph → ({𝑚, 𝑋} ∈ 𝐸 ↔ 𝑚 ∈ (𝐺 NeighbVtx 𝑋))) |
53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝐺 ∈ USGraph ) → ({𝑚, 𝑋} ∈ 𝐸 ↔ 𝑚 ∈ (𝐺 NeighbVtx 𝑋))) |
54 | 53 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑚 ∈ (𝐺 NeighbVtx 𝑋)) |
55 | 54, 37 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ {𝑚, 𝑋} ∈ 𝐸) → 𝑚 ∈ 𝐷) |
56 | 51, 55 | jca 553 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝜑 ∧ 𝑚 ∈ 𝐷)) |
57 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑚 → {𝑥, 𝑦} = {𝑚, 𝑦}) |
58 | 57 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑚 → ({𝑥, 𝑦} ∈ 𝐸 ↔ {𝑚, 𝑦} ∈ 𝐸)) |
59 | 58 | riotabidv 6513 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑚 → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) = (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ 𝐸)) |
60 | 59 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) = (𝑚 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ 𝐸)) |
61 | 10, 60 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐴 = (𝑚 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ 𝐸)) |
62 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 61 | frgrncvvdeqlem6 41474 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐷) → {(𝐴‘𝑚)} = ((𝐺 NeighbVtx 𝑚) ∩ 𝑁)) |
63 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 NeighbVtx 𝑚) ∩ 𝑁) = {(𝐴‘𝑚)} → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) ↔ 𝑛 ∈ {(𝐴‘𝑚)})) |
64 | 63 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({(𝐴‘𝑚)} = ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) ↔ 𝑛 ∈ {(𝐴‘𝑚)})) |
65 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ {(𝐴‘𝑚)} → 𝑛 = (𝐴‘𝑚)) |
66 | 64, 65 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({(𝐴‘𝑚)} = ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚))) |
67 | 56, 62, 66 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ {𝑚, 𝑋} ∈ 𝐸) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚))) |
68 | 67 | expcom 450 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑚, 𝑋} ∈ 𝐸 → ((𝜑 ∧ 𝐺 ∈ USGraph ) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚)))) |
69 | 68 | ad2antll 761 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → ((𝜑 ∧ 𝐺 ∈ USGraph ) → (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚)))) |
70 | 69 | com3r 85 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ((𝐺 NeighbVtx 𝑚) ∩ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → ((𝜑 ∧ 𝐺 ∈ USGraph ) → 𝑛 = (𝐴‘𝑚)))) |
71 | 50, 70 | sylbir 224 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (𝐺 NeighbVtx 𝑚) ∧ 𝑛 ∈ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → ((𝜑 ∧ 𝐺 ∈ USGraph ) → 𝑛 = (𝐴‘𝑚)))) |
72 | 71 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → (𝑛 ∈ 𝑁 → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → ((𝜑 ∧ 𝐺 ∈ USGraph ) → 𝑛 = (𝐴‘𝑚))))) |
73 | 72 | com14 94 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐺 ∈ USGraph ) → (𝑛 ∈ 𝑁 → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → 𝑛 = (𝐴‘𝑚))))) |
74 | 73 | imp31 447 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) → (𝑛 ∈ (𝐺 NeighbVtx 𝑚) → 𝑛 = (𝐴‘𝑚))) |
75 | 49, 74 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) → 𝑛 = (𝐴‘𝑚)) |
76 | 42, 75 | jca 553 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐺 ∈ USGraph ) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸))) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
77 | 76 | exp31 628 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐺 ∈ USGraph ) → (𝑛 ∈ 𝑁 → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))))) |
78 | 35, 77 | mpdan 699 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ 𝑁 → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))))) |
79 | 78 | imp 444 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
80 | 79 | eximdv 1833 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ 𝐸 ∧ {𝑚, 𝑋} ∈ 𝐸)) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
81 | 34, 80 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
82 | | df-rex 2902 |
. . . 4
⊢
(∃𝑚 ∈
𝐷 𝑛 = (𝐴‘𝑚) ↔ ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
83 | 81, 82 | sylibr 223 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚)) |
84 | 83 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚)) |
85 | | dffo3 6282 |
. 2
⊢ (𝐴:𝐷–onto→𝑁 ↔ (𝐴:𝐷⟶𝑁 ∧ ∀𝑛 ∈ 𝑁 ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚))) |
86 | 11, 84, 85 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐴:𝐷–onto→𝑁) |