Step | Hyp | Ref
| Expression |
1 | | eldifsn 4260 |
. . . . . . 7
⊢ (𝑣 ∈ (𝑉 ∖ {𝑁}) ↔ (𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑁)) |
2 | | simpl 472 |
. . . . . . 7
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑁) → 𝑣 ∈ 𝑉) |
3 | 1, 2 | sylbi 206 |
. . . . . 6
⊢ (𝑣 ∈ (𝑉 ∖ {𝑁}) → 𝑣 ∈ 𝑉) |
4 | | simpr 476 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉) |
5 | | prelpwi 4842 |
. . . . . 6
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → {𝑣, 𝑁} ∈ 𝒫 𝑉) |
6 | 3, 4, 5 | syl2anr 494 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑣 ∈ (𝑉 ∖ {𝑁})) → {𝑣, 𝑁} ∈ 𝒫 𝑉) |
7 | 1 | biimpi 205 |
. . . . . . 7
⊢ (𝑣 ∈ (𝑉 ∖ {𝑁}) → (𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑁)) |
8 | 7 | adantl 481 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑣 ∈ (𝑉 ∖ {𝑁})) → (𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑁)) |
9 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑁) → 𝑣 ≠ 𝑁) |
10 | 1, 9 | sylbi 206 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝑉 ∖ {𝑁}) → 𝑣 ≠ 𝑁) |
11 | 10 | adantl 481 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑣 ∈ (𝑉 ∖ {𝑁})) → 𝑣 ≠ 𝑁) |
12 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑣 ∈ (𝑉 ∖ {𝑁})) → {𝑣, 𝑁} = {𝑣, 𝑁}) |
13 | 11, 12 | jca 553 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑣 ∈ (𝑉 ∖ {𝑁})) → (𝑣 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑣, 𝑁})) |
14 | | neeq1 2844 |
. . . . . . . . 9
⊢ (𝑎 = 𝑣 → (𝑎 ≠ 𝑁 ↔ 𝑣 ≠ 𝑁)) |
15 | | preq1 4212 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑣 → {𝑎, 𝑁} = {𝑣, 𝑁}) |
16 | 15 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑎 = 𝑣 → ({𝑣, 𝑁} = {𝑎, 𝑁} ↔ {𝑣, 𝑁} = {𝑣, 𝑁})) |
17 | 14, 16 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑎 = 𝑣 → ((𝑎 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑎, 𝑁}) ↔ (𝑣 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑣, 𝑁}))) |
18 | 17 | adantl 481 |
. . . . . . 7
⊢ (((𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑁) ∧ 𝑎 = 𝑣) → ((𝑎 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑎, 𝑁}) ↔ (𝑣 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑣, 𝑁}))) |
19 | 2, 18 | rspcedv 3286 |
. . . . . 6
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑁) → ((𝑣 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑣, 𝑁}) → ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑎, 𝑁}))) |
20 | 8, 13, 19 | sylc 63 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑣 ∈ (𝑉 ∖ {𝑁})) → ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑎, 𝑁})) |
21 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑥 = {𝑣, 𝑁} → (𝑥 = {𝑎, 𝑁} ↔ {𝑣, 𝑁} = {𝑎, 𝑁})) |
22 | 21 | anbi2d 736 |
. . . . . . 7
⊢ (𝑥 = {𝑣, 𝑁} → ((𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁}) ↔ (𝑎 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑎, 𝑁}))) |
23 | 22 | rexbidv 3034 |
. . . . . 6
⊢ (𝑥 = {𝑣, 𝑁} → (∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁}) ↔ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑎, 𝑁}))) |
24 | | cusgrafi.p |
. . . . . 6
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} |
25 | 23, 24 | elrab2 3333 |
. . . . 5
⊢ ({𝑣, 𝑁} ∈ 𝑃 ↔ ({𝑣, 𝑁} ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ {𝑣, 𝑁} = {𝑎, 𝑁}))) |
26 | 6, 20, 25 | sylanbrc 695 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑣 ∈ (𝑉 ∖ {𝑁})) → {𝑣, 𝑁} ∈ 𝑃) |
27 | 26 | ralrimiva 2949 |
. . 3
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ 𝑃) |
28 | | preq1 4212 |
. . . . 5
⊢ (𝑥 = 𝑣 → {𝑥, 𝑁} = {𝑣, 𝑁}) |
29 | 28 | eleq1d 2672 |
. . . 4
⊢ (𝑥 = 𝑣 → ({𝑥, 𝑁} ∈ 𝑃 ↔ {𝑣, 𝑁} ∈ 𝑃)) |
30 | 29 | cbvralv 3147 |
. . 3
⊢
(∀𝑥 ∈
(𝑉 ∖ {𝑁}){𝑥, 𝑁} ∈ 𝑃 ↔ ∀𝑣 ∈ (𝑉 ∖ {𝑁}){𝑣, 𝑁} ∈ 𝑃) |
31 | 27, 30 | sylibr 223 |
. 2
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → ∀𝑥 ∈ (𝑉 ∖ {𝑁}){𝑥, 𝑁} ∈ 𝑃) |
32 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}) → 𝑎 ≠ 𝑁) |
33 | 32 | anim2i 591 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) → (𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑁)) |
34 | 33 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) → (𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑁)) |
35 | | eldifsn 4260 |
. . . . . . . . 9
⊢ (𝑎 ∈ (𝑉 ∖ {𝑁}) ↔ (𝑎 ∈ 𝑉 ∧ 𝑎 ≠ 𝑁)) |
36 | 34, 35 | sylibr 223 |
. . . . . . . 8
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) → 𝑎 ∈ (𝑉 ∖ {𝑁})) |
37 | | eqeq1 2614 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = {𝑎, 𝑁} → (𝑒 = {𝑥, 𝑁} ↔ {𝑎, 𝑁} = {𝑥, 𝑁})) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}) → (𝑒 = {𝑥, 𝑁} ↔ {𝑎, 𝑁} = {𝑥, 𝑁})) |
39 | 38 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑒 = {𝑥, 𝑁} ↔ {𝑎, 𝑁} = {𝑥, 𝑁})) |
40 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑎 ∈ V |
41 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
42 | 40, 41 | preqr1 4319 |
. . . . . . . . . . . . 13
⊢ ({𝑎, 𝑁} = {𝑥, 𝑁} → 𝑎 = 𝑥) |
43 | 42 | equcomd 1933 |
. . . . . . . . . . . 12
⊢ ({𝑎, 𝑁} = {𝑥, 𝑁} → 𝑥 = 𝑎) |
44 | 39, 43 | syl6bi 242 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑒 = {𝑥, 𝑁} → 𝑥 = 𝑎)) |
45 | 44 | adantll 746 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑒 = {𝑥, 𝑁} → 𝑥 = 𝑎)) |
46 | | preq1 4212 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → {𝑎, 𝑁} = {𝑥, 𝑁}) |
47 | 46 | equcoms 1934 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → {𝑎, 𝑁} = {𝑥, 𝑁}) |
48 | 47 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑒 = {𝑎, 𝑁} ↔ 𝑒 = {𝑥, 𝑁})) |
49 | 48 | biimpcd 238 |
. . . . . . . . . . . . 13
⊢ (𝑒 = {𝑎, 𝑁} → (𝑥 = 𝑎 → 𝑒 = {𝑥, 𝑁})) |
50 | 49 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}) → (𝑥 = 𝑎 → 𝑒 = {𝑥, 𝑁})) |
51 | 50 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) → (𝑥 = 𝑎 → 𝑒 = {𝑥, 𝑁})) |
52 | 51 | ad2antlr 759 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑥 = 𝑎 → 𝑒 = {𝑥, 𝑁})) |
53 | 45, 52 | impbid 201 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) ∧ 𝑥 ∈ (𝑉 ∖ {𝑁})) → (𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎)) |
54 | 53 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) → ∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎)) |
55 | 36, 54 | jca 553 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝒫 𝑉) ∧ (𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) → (𝑎 ∈ (𝑉 ∖ {𝑁}) ∧ ∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎))) |
56 | 55 | ex 449 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝒫 𝑉) → ((𝑎 ∈ 𝑉 ∧ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) → (𝑎 ∈ (𝑉 ∖ {𝑁}) ∧ ∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎)))) |
57 | 56 | reximdv2 2997 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) ∧ 𝑒 ∈ 𝒫 𝑉) → (∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}) → ∃𝑎 ∈ (𝑉 ∖ {𝑁})∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎))) |
58 | 57 | expimpd 627 |
. . . 4
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → ((𝑒 ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁})) → ∃𝑎 ∈ (𝑉 ∖ {𝑁})∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎))) |
59 | | eqeq1 2614 |
. . . . . . 7
⊢ (𝑥 = 𝑒 → (𝑥 = {𝑎, 𝑁} ↔ 𝑒 = {𝑎, 𝑁})) |
60 | 59 | anbi2d 736 |
. . . . . 6
⊢ (𝑥 = 𝑒 → ((𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁}) ↔ (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) |
61 | 60 | rexbidv 3034 |
. . . . 5
⊢ (𝑥 = 𝑒 → (∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁}) ↔ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) |
62 | 61, 24 | elrab2 3333 |
. . . 4
⊢ (𝑒 ∈ 𝑃 ↔ (𝑒 ∈ 𝒫 𝑉 ∧ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑒 = {𝑎, 𝑁}))) |
63 | | reu6 3362 |
. . . 4
⊢
(∃!𝑥 ∈
(𝑉 ∖ {𝑁})𝑒 = {𝑥, 𝑁} ↔ ∃𝑎 ∈ (𝑉 ∖ {𝑁})∀𝑥 ∈ (𝑉 ∖ {𝑁})(𝑒 = {𝑥, 𝑁} ↔ 𝑥 = 𝑎)) |
64 | 58, 62, 63 | 3imtr4g 284 |
. . 3
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → (𝑒 ∈ 𝑃 → ∃!𝑥 ∈ (𝑉 ∖ {𝑁})𝑒 = {𝑥, 𝑁})) |
65 | 64 | ralrimiv 2948 |
. 2
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → ∀𝑒 ∈ 𝑃 ∃!𝑥 ∈ (𝑉 ∖ {𝑁})𝑒 = {𝑥, 𝑁}) |
66 | | cusgrafi.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) |
67 | 66 | f1ompt 6290 |
. 2
⊢ (𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃 ↔ (∀𝑥 ∈ (𝑉 ∖ {𝑁}){𝑥, 𝑁} ∈ 𝑃 ∧ ∀𝑒 ∈ 𝑃 ∃!𝑥 ∈ (𝑉 ∖ {𝑁})𝑒 = {𝑥, 𝑁})) |
68 | 31, 65, 67 | sylanbrc 695 |
1
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃) |