Step | Hyp | Ref
| Expression |
1 | | 0ex 4718 |
. . . . 5
⊢ ∅
∈ V |
2 | | isuvtx 26016 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ ∅ ∈
V) → (𝑉 UnivVertex
∅) = {𝑥 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅}) |
3 | 1, 2 | mpan2 703 |
. . . 4
⊢ (𝑉 ∈ V → (𝑉 UnivVertex ∅) = {𝑥 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅}) |
4 | 3 | neeq1d 2841 |
. . 3
⊢ (𝑉 ∈ V → ((𝑉 UnivVertex ∅) ≠
∅ ↔ {𝑥 ∈
𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅} ≠
∅)) |
5 | | rabn0 3912 |
. . . 4
⊢ ({𝑥 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅} ≠ ∅ ↔
∃𝑥 ∈ 𝑉 ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝑉 ∈ V → ({𝑥 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅} ≠ ∅ ↔
∃𝑥 ∈ 𝑉 ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅)) |
7 | | df-rex 2902 |
. . . 4
⊢
(∃𝑥 ∈
𝑉 ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅ ↔ ∃𝑥(𝑥 ∈ 𝑉 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅)) |
8 | | noel 3878 |
. . . . . . . . . 10
⊢ ¬
{𝑘, 𝑥} ∈ ∅ |
9 | | rn0 5298 |
. . . . . . . . . . 11
⊢ ran
∅ = ∅ |
10 | 9 | eleq2i 2680 |
. . . . . . . . . 10
⊢ ({𝑘, 𝑥} ∈ ran ∅ ↔ {𝑘, 𝑥} ∈ ∅) |
11 | 8, 10 | mtbir 312 |
. . . . . . . . 9
⊢ ¬
{𝑘, 𝑥} ∈ ran ∅ |
12 | 11 | ralf0 4030 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅ ↔ (𝑉 ∖ {𝑥}) = ∅) |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝑉 ∈ V → (∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅ ↔ (𝑉 ∖ {𝑥}) = ∅)) |
14 | 13 | anbi2d 736 |
. . . . . 6
⊢ (𝑉 ∈ V → ((𝑥 ∈ 𝑉 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅) ↔ (𝑥 ∈ 𝑉 ∧ (𝑉 ∖ {𝑥}) = ∅))) |
15 | | ssdif0 3896 |
. . . . . . . . 9
⊢ (𝑉 ⊆ {𝑥} ↔ (𝑉 ∖ {𝑥}) = ∅) |
16 | 15 | a1i 11 |
. . . . . . . 8
⊢ (𝑉 ∈ V → (𝑉 ⊆ {𝑥} ↔ (𝑉 ∖ {𝑥}) = ∅)) |
17 | 16 | bicomd 212 |
. . . . . . 7
⊢ (𝑉 ∈ V → ((𝑉 ∖ {𝑥}) = ∅ ↔ 𝑉 ⊆ {𝑥})) |
18 | 17 | anbi2d 736 |
. . . . . 6
⊢ (𝑉 ∈ V → ((𝑥 ∈ 𝑉 ∧ (𝑉 ∖ {𝑥}) = ∅) ↔ (𝑥 ∈ 𝑉 ∧ 𝑉 ⊆ {𝑥}))) |
19 | | sssn 4298 |
. . . . . . . . 9
⊢ (𝑉 ⊆ {𝑥} ↔ (𝑉 = ∅ ∨ 𝑉 = {𝑥})) |
20 | 19 | anbi2i 726 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑉 ⊆ {𝑥}) ↔ (𝑥 ∈ 𝑉 ∧ (𝑉 = ∅ ∨ 𝑉 = {𝑥}))) |
21 | | n0i 3879 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑉 → ¬ 𝑉 = ∅) |
22 | 21 | pm2.21d 117 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑉 → (𝑉 = ∅ → 𝑉 = {𝑥})) |
23 | 22 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑉 = ∅) → 𝑉 = {𝑥}) |
24 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑉 = {𝑥}) → 𝑉 = {𝑥}) |
25 | 23, 24 | jaodan 822 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑉 ∧ (𝑉 = ∅ ∨ 𝑉 = {𝑥})) → 𝑉 = {𝑥}) |
26 | | vsnid 4156 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ {𝑥} |
27 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝑥} → (𝑥 ∈ 𝑉 ↔ 𝑥 ∈ {𝑥})) |
28 | 26, 27 | mpbiri 247 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑥} → 𝑥 ∈ 𝑉) |
29 | | olc 398 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑥} → (𝑉 = ∅ ∨ 𝑉 = {𝑥})) |
30 | 28, 29 | jca 553 |
. . . . . . . . 9
⊢ (𝑉 = {𝑥} → (𝑥 ∈ 𝑉 ∧ (𝑉 = ∅ ∨ 𝑉 = {𝑥}))) |
31 | 25, 30 | impbii 198 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ (𝑉 = ∅ ∨ 𝑉 = {𝑥})) ↔ 𝑉 = {𝑥}) |
32 | 20, 31 | bitri 263 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑉 ⊆ {𝑥}) ↔ 𝑉 = {𝑥}) |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝑉 ∈ V → ((𝑥 ∈ 𝑉 ∧ 𝑉 ⊆ {𝑥}) ↔ 𝑉 = {𝑥})) |
34 | 14, 18, 33 | 3bitrd 293 |
. . . . 5
⊢ (𝑉 ∈ V → ((𝑥 ∈ 𝑉 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅) ↔ 𝑉 = {𝑥})) |
35 | 34 | exbidv 1837 |
. . . 4
⊢ (𝑉 ∈ V → (∃𝑥(𝑥 ∈ 𝑉 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅) ↔ ∃𝑥 𝑉 = {𝑥})) |
36 | 7, 35 | syl5bb 271 |
. . 3
⊢ (𝑉 ∈ V → (∃𝑥 ∈ 𝑉 ∀𝑘 ∈ (𝑉 ∖ {𝑥}){𝑘, 𝑥} ∈ ran ∅ ↔ ∃𝑥 𝑉 = {𝑥})) |
37 | 4, 6, 36 | 3bitrd 293 |
. 2
⊢ (𝑉 ∈ V → ((𝑉 UnivVertex ∅) ≠
∅ ↔ ∃𝑥
𝑉 = {𝑥})) |
38 | | id 22 |
. . . . . . 7
⊢ (¬
𝑉 ∈ V → ¬
𝑉 ∈
V) |
39 | 38 | intnanrd 954 |
. . . . . 6
⊢ (¬
𝑉 ∈ V → ¬
(𝑉 ∈ V ∧ ∅
∈ V)) |
40 | | df-uvtx 25951 |
. . . . . . 7
⊢
UnivVertex = (𝑣 ∈ V,
𝑒 ∈ V ↦ {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒}) |
41 | 40 | mpt2ndm0 6773 |
. . . . . 6
⊢ (¬
(𝑉 ∈ V ∧ ∅
∈ V) → (𝑉
UnivVertex ∅) = ∅) |
42 | 39, 41 | syl 17 |
. . . . 5
⊢ (¬
𝑉 ∈ V → (𝑉 UnivVertex ∅) =
∅) |
43 | 42 | notnotd 137 |
. . . 4
⊢ (¬
𝑉 ∈ V → ¬
¬ (𝑉 UnivVertex
∅) = ∅) |
44 | | df-ne 2782 |
. . . 4
⊢ ((𝑉 UnivVertex ∅) ≠
∅ ↔ ¬ (𝑉
UnivVertex ∅) = ∅) |
45 | 43, 44 | sylnibr 318 |
. . 3
⊢ (¬
𝑉 ∈ V → ¬
(𝑉 UnivVertex ∅) ≠
∅) |
46 | | snex 4835 |
. . . . . 6
⊢ {𝑥} ∈ V |
47 | | eleq1 2676 |
. . . . . 6
⊢ (𝑉 = {𝑥} → (𝑉 ∈ V ↔ {𝑥} ∈ V)) |
48 | 46, 47 | mpbiri 247 |
. . . . 5
⊢ (𝑉 = {𝑥} → 𝑉 ∈ V) |
49 | 48 | exlimiv 1845 |
. . . 4
⊢
(∃𝑥 𝑉 = {𝑥} → 𝑉 ∈ V) |
50 | 49 | con3i 149 |
. . 3
⊢ (¬
𝑉 ∈ V → ¬
∃𝑥 𝑉 = {𝑥}) |
51 | 45, 50 | 2falsed 365 |
. 2
⊢ (¬
𝑉 ∈ V → ((𝑉 UnivVertex ∅) ≠
∅ ↔ ∃𝑥
𝑉 = {𝑥})) |
52 | 37, 51 | pm2.61i 175 |
1
⊢ ((𝑉 UnivVertex ∅) ≠
∅ ↔ ∃𝑥
𝑉 = {𝑥}) |