Step | Hyp | Ref
| Expression |
1 | | df-uvtx 25951 |
. 2
⊢
UnivVertex = (𝑣 ∈ V,
𝑒 ∈ V ↦ {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒}) |
2 | | elex 3185 |
. . . 4
⊢ (𝑉 ∈ 𝑋 → 𝑉 ∈ V) |
3 | 2 | adantr 480 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝑉 ∈ V) |
4 | | elex 3185 |
. . . . 5
⊢ (𝐸 ∈ 𝑌 → 𝐸 ∈ V) |
5 | 4 | adantl 481 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ∈ V) |
6 | 5 | adantr 480 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑣 = 𝑉) → 𝐸 ∈ V) |
7 | | vex 3176 |
. . . 4
⊢ 𝑣 ∈ V |
8 | | rabexg 4739 |
. . . 4
⊢ (𝑣 ∈ V → {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒} ∈ V) |
9 | 7, 8 | mp1i 13 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒} ∈ V) |
10 | | simprl 790 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → 𝑣 = 𝑉) |
11 | | difeq1 3683 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → (𝑣 ∖ {𝑛}) = (𝑉 ∖ {𝑛})) |
12 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 ∖ {𝑛}) = (𝑉 ∖ {𝑛})) |
13 | | rneq 5272 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → ran 𝑒 = ran 𝐸) |
14 | 13 | eleq2d 2673 |
. . . . . . 7
⊢ (𝑒 = 𝐸 → ({𝑘, 𝑛} ∈ ran 𝑒 ↔ {𝑘, 𝑛} ∈ ran 𝐸)) |
15 | 14 | adantl 481 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ({𝑘, 𝑛} ∈ ran 𝑒 ↔ {𝑘, 𝑛} ∈ ran 𝐸)) |
16 | 12, 15 | raleqbidv 3129 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒 ↔ ∀𝑘 ∈ (𝑉 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝐸)) |
17 | 16 | adantl 481 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒 ↔ ∀𝑘 ∈ (𝑉 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝐸)) |
18 | 10, 17 | rabeqbidv 3168 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒} = {𝑛 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝐸}) |
19 | 3, 6, 9, 18 | ovmpt2dv2 6692 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ( UnivVertex = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑛 ∈ 𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒}) → (𝑉 UnivVertex 𝐸) = {𝑛 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝐸})) |
20 | 1, 19 | mpi 20 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 UnivVertex 𝐸) = {𝑛 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝐸}) |