Step | Hyp | Ref
| Expression |
1 | | frgrancvvdeq.nx |
. . 3
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) |
2 | | frgrancvvdeq.ny |
. . 3
⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) |
3 | | frgrancvvdeq.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
4 | | frgrancvvdeq.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
5 | | frgrancvvdeq.ne |
. . 3
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
6 | | frgrancvvdeq.xy |
. . 3
⊢ (𝜑 → 𝑌 ∉ 𝐷) |
7 | | frgrancvvdeq.f |
. . 3
⊢ (𝜑 → 𝑉 FriendGrph 𝐸) |
8 | | frgrancvvdeq.a |
. . 3
⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | frgrancvvdeqlem5 26561 |
. 2
⊢ (𝜑 → 𝐴:𝐷⟶𝑁) |
10 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑉 FriendGrph 𝐸) |
11 | 2 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑁 ↔ 𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑌)) |
12 | | frisusgra 26519 |
. . . . . . . . . . 11
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
13 | | nbgraisvtx 25960 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑌) → 𝑛 ∈ 𝑉)) |
14 | 7, 12, 13 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑌) → 𝑛 ∈ 𝑉)) |
15 | 11, 14 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑁 → 𝑛 ∈ 𝑉)) |
16 | 15 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑛 ∈ 𝑉) |
17 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑋 ∈ 𝑉) |
18 | 1, 2, 3, 4, 5, 6, 7, 8 | frgrancvvdeqlem2 26558 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∉ 𝑁) |
19 | | df-nel 2783 |
. . . . . . . . . . 11
⊢ (𝑋 ∉ 𝑁 ↔ ¬ 𝑋 ∈ 𝑁) |
20 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑋 → (𝑛 ∈ 𝑁 ↔ 𝑋 ∈ 𝑁)) |
21 | 20 | biimpcd 238 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑁 → (𝑛 = 𝑋 → 𝑋 ∈ 𝑁)) |
22 | 21 | con3rr3 150 |
. . . . . . . . . . . 12
⊢ (¬
𝑋 ∈ 𝑁 → (𝑛 ∈ 𝑁 → ¬ 𝑛 = 𝑋)) |
23 | | df-ne 2782 |
. . . . . . . . . . . 12
⊢ (𝑛 ≠ 𝑋 ↔ ¬ 𝑛 = 𝑋) |
24 | 22, 23 | syl6ibr 241 |
. . . . . . . . . . 11
⊢ (¬
𝑋 ∈ 𝑁 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
25 | 19, 24 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝑋 ∉ 𝑁 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
26 | 18, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋)) |
27 | 26 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝑛 ≠ 𝑋) |
28 | 16, 17, 27 | 3jca 1235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋)) |
29 | 10, 28 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (𝑉 FriendGrph 𝐸 ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋))) |
30 | | frgraun 26523 |
. . . . . . 7
⊢ (𝑉 FriendGrph 𝐸 → ((𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋) → ∃!𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) |
31 | 30 | imp 444 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋)) → ∃!𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) |
32 | | reurex 3137 |
. . . . . . 7
⊢
(∃!𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸) → ∃𝑚 ∈ 𝑉 ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) |
33 | | df-rex 2902 |
. . . . . . 7
⊢
(∃𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸) ↔ ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) |
34 | 32, 33 | sylib 207 |
. . . . . 6
⊢
(∃!𝑚 ∈
𝑉 ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸) → ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) |
35 | 29, 31, 34 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) |
36 | 7, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 USGrph 𝐸) |
37 | | simprrr 801 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) → {𝑚, 𝑋} ∈ ran 𝐸) |
38 | 1 | eleq2i 2680 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ 𝐷 ↔ 𝑚 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) |
39 | | nbgraeledg 25959 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 USGrph 𝐸 → (𝑚 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ↔ {𝑚, 𝑋} ∈ ran 𝐸)) |
40 | 39 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) → (𝑚 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ↔ {𝑚, 𝑋} ∈ ran 𝐸)) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) → (𝑚 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ↔ {𝑚, 𝑋} ∈ ran 𝐸)) |
42 | 38, 41 | syl5bb 271 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) → (𝑚 ∈ 𝐷 ↔ {𝑚, 𝑋} ∈ ran 𝐸)) |
43 | 37, 42 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) → 𝑚 ∈ 𝐷) |
44 | | nbgraeledg 25959 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 USGrph 𝐸 → (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚) ↔ {𝑛, 𝑚} ∈ ran 𝐸)) |
45 | 44 | biimprcd 239 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑛, 𝑚} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → 𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚))) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸) → (𝑉 USGrph 𝐸 → 𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚))) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → (𝑉 USGrph 𝐸 → 𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚))) |
48 | 47 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑉 USGrph 𝐸 → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → 𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚))) |
49 | 48 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → 𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚))) |
50 | 49 | imp 444 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) → 𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚)) |
51 | | elin 3758 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) ↔ (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚) ∧ 𝑛 ∈ 𝑁)) |
52 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ {𝑚, 𝑋} ∈ ran 𝐸) → 𝜑) |
53 | 39 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑉 USGrph 𝐸 → ({𝑚, 𝑋} ∈ ran 𝐸 ↔ 𝑚 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) |
54 | 53 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑉 USGrph 𝐸) → ({𝑚, 𝑋} ∈ ran 𝐸 ↔ 𝑚 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) |
55 | 54 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ {𝑚, 𝑋} ∈ ran 𝐸) → 𝑚 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) |
56 | 55, 38 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ {𝑚, 𝑋} ∈ ran 𝐸) → 𝑚 ∈ 𝐷) |
57 | 52, 56 | jca 553 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ {𝑚, 𝑋} ∈ ran 𝐸) → (𝜑 ∧ 𝑚 ∈ 𝐷)) |
58 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑚 → {𝑥, 𝑦} = {𝑚, 𝑦}) |
59 | 58 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑚 → ({𝑥, 𝑦} ∈ ran 𝐸 ↔ {𝑚, 𝑦} ∈ ran 𝐸)) |
60 | 59 | riotabidv 6513 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑚 → (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸) = (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ ran 𝐸)) |
61 | 60 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) = (𝑚 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ ran 𝐸)) |
62 | 8, 61 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐴 = (𝑚 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑚, 𝑦} ∈ ran 𝐸)) |
63 | 1, 2, 3, 4, 5, 6, 7, 62 | frgrancvvdeqlem6 26562 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐷) → {(𝐴‘𝑚)} = ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁)) |
64 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) = {(𝐴‘𝑚)} → (𝑛 ∈ ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) ↔ 𝑛 ∈ {(𝐴‘𝑚)})) |
65 | 64 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({(𝐴‘𝑚)} = ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) → (𝑛 ∈ ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) ↔ 𝑛 ∈ {(𝐴‘𝑚)})) |
66 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ {(𝐴‘𝑚)} → 𝑛 = (𝐴‘𝑚)) |
67 | 65, 66 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({(𝐴‘𝑚)} = ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) → (𝑛 ∈ ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚))) |
68 | 57, 63, 67 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ {𝑚, 𝑋} ∈ ran 𝐸) → (𝑛 ∈ ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚))) |
69 | 68 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑚, 𝑋} ∈ ran 𝐸 → ((𝜑 ∧ 𝑉 USGrph 𝐸) → (𝑛 ∈ ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚)))) |
70 | 69 | ad2antll 761 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → ((𝜑 ∧ 𝑉 USGrph 𝐸) → (𝑛 ∈ ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) → 𝑛 = (𝐴‘𝑚)))) |
71 | 70 | com3r 85 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ((〈𝑉, 𝐸〉 Neighbors 𝑚) ∩ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → ((𝜑 ∧ 𝑉 USGrph 𝐸) → 𝑛 = (𝐴‘𝑚)))) |
72 | 51, 71 | sylbir 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚) ∧ 𝑛 ∈ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → ((𝜑 ∧ 𝑉 USGrph 𝐸) → 𝑛 = (𝐴‘𝑚)))) |
73 | 72 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚) → (𝑛 ∈ 𝑁 → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → ((𝜑 ∧ 𝑉 USGrph 𝐸) → 𝑛 = (𝐴‘𝑚))))) |
74 | 73 | com14 94 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑉 USGrph 𝐸) → (𝑛 ∈ 𝑁 → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚) → 𝑛 = (𝐴‘𝑚))))) |
75 | 74 | imp31 447 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) → (𝑛 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑚) → 𝑛 = (𝐴‘𝑚))) |
76 | 50, 75 | mpd 15 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) → 𝑛 = (𝐴‘𝑚)) |
77 | 43, 76 | jca 553 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) ∧ (𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸))) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
78 | 77 | ex 449 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑉 USGrph 𝐸) ∧ 𝑛 ∈ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
79 | 78 | ex 449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑉 USGrph 𝐸) → (𝑛 ∈ 𝑁 → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))))) |
80 | 36, 79 | mpdan 699 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ 𝑁 → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))))) |
81 | 80 | imp 444 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ((𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → (𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
82 | 81 | eximdv 1833 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → (∃𝑚(𝑚 ∈ 𝑉 ∧ ({𝑛, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑋} ∈ ran 𝐸)) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚)))) |
83 | 35, 82 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
84 | | df-rex 2902 |
. . . 4
⊢
(∃𝑚 ∈
𝐷 𝑛 = (𝐴‘𝑚) ↔ ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = (𝐴‘𝑚))) |
85 | 83, 84 | sylibr 223 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚)) |
86 | 85 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚)) |
87 | | dffo3 6282 |
. 2
⊢ (𝐴:𝐷–onto→𝑁 ↔ (𝐴:𝐷⟶𝑁 ∧ ∀𝑛 ∈ 𝑁 ∃𝑚 ∈ 𝐷 𝑛 = (𝐴‘𝑚))) |
88 | 9, 86, 87 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐴:𝐷–onto→𝑁) |