Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . . . 6
⊢
(〈𝑉, 𝐸〉 Neighbors 𝑥) ∈ V |
2 | | mptexg 6389 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 Neighbors 𝑥) ∈ V → (𝑢 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↦ (℩𝑤 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑦){𝑢, 𝑤} ∈ ran 𝐸)) ∈ V) |
3 | 1, 2 | mp1i 13 |
. . . . 5
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (𝑢 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↦ (℩𝑤 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑦){𝑢, 𝑤} ∈ ran 𝐸)) ∈ V) |
4 | | eqid 2610 |
. . . . . 6
⊢
(〈𝑉, 𝐸〉 Neighbors 𝑥) = (〈𝑉, 𝐸〉 Neighbors 𝑥) |
5 | | eqid 2610 |
. . . . . 6
⊢
(〈𝑉, 𝐸〉 Neighbors 𝑦) = (〈𝑉, 𝐸〉 Neighbors 𝑦) |
6 | | simpllr 795 |
. . . . . 6
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → 𝑥 ∈ 𝑉) |
7 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑉 ∖ {𝑥}) → 𝑦 ∈ 𝑉) |
8 | 7 | ad2antlr 759 |
. . . . . 6
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → 𝑦 ∈ 𝑉) |
9 | | eldif 3550 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝑉 ∖ {𝑥}) ↔ (𝑦 ∈ 𝑉 ∧ ¬ 𝑦 ∈ {𝑥})) |
10 | | velsn 4141 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥) |
11 | 10 | biimpri 217 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → 𝑦 ∈ {𝑥}) |
12 | 11 | equcoms 1934 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝑦 ∈ {𝑥}) |
13 | 12 | necon3bi 2808 |
. . . . . . . . 9
⊢ (¬
𝑦 ∈ {𝑥} → 𝑥 ≠ 𝑦) |
14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑉 ∧ ¬ 𝑦 ∈ {𝑥}) → 𝑥 ≠ 𝑦) |
15 | 9, 14 | sylbi 206 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑉 ∖ {𝑥}) → 𝑥 ≠ 𝑦) |
16 | 15 | ad2antlr 759 |
. . . . . 6
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → 𝑥 ≠ 𝑦) |
17 | | simpr 476 |
. . . . . 6
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) |
18 | | simplll 794 |
. . . . . 6
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → 𝑉 FriendGrph 𝐸) |
19 | | eqid 2610 |
. . . . . 6
⊢ (𝑢 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↦ (℩𝑤 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑦){𝑢, 𝑤} ∈ ran 𝐸)) = (𝑢 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↦ (℩𝑤 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑦){𝑢, 𝑤} ∈ ran 𝐸)) |
20 | 4, 5, 6, 8, 16, 17, 18, 19 | frgrancvvdeqlem8 26567 |
. . . . 5
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → (𝑢 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↦ (℩𝑤 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑦){𝑢, 𝑤} ∈ ran 𝐸)):(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦)) |
21 | | f1oeq1 6040 |
. . . . . 6
⊢ (𝑓 = (𝑢 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↦ (℩𝑤 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑦){𝑢, 𝑤} ∈ ran 𝐸)) → (𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦) ↔ (𝑢 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↦ (℩𝑤 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑦){𝑢, 𝑤} ∈ ran 𝐸)):(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
22 | 21 | spcegv 3267 |
. . . . 5
⊢ ((𝑢 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↦ (℩𝑤 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑦){𝑢, 𝑤} ∈ ran 𝐸)) ∈ V → ((𝑢 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑥) ↦ (℩𝑤 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑦){𝑢, 𝑤} ∈ ran 𝐸)):(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
23 | 3, 20, 22 | sylc 63 |
. . . 4
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) ∧ 𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥)) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦)) |
24 | 23 | ex 449 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) ∧ 𝑦 ∈ (𝑉 ∖ {𝑥})) → (𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
25 | 24 | ralrimiva 2949 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑥 ∈ 𝑉) → ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |
26 | 25 | ralrimiva 2949 |
1
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) |