Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. 2
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
2 | | iscusgra 25985 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑥 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸))) |
3 | 2 | baibd 946 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → (𝑉 ComplUSGrph 𝐸 ↔ ∀𝑥 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸)) |
4 | | dfcleq 2604 |
. . . . 5
⊢ ({𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} = 𝑉 ↔ ∀𝑥(𝑥 ∈ {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} ↔ 𝑥 ∈ 𝑉)) |
5 | 4 | a1i 11 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → ({𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} = 𝑉 ↔ ∀𝑥(𝑥 ∈ {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} ↔ 𝑥 ∈ 𝑉))) |
6 | | isuvtx 26016 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 UnivVertex 𝐸) = {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸}) |
7 | 6 | eqeq1d 2612 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑉 UnivVertex 𝐸) = 𝑉 ↔ {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} = 𝑉)) |
8 | 7 | adantr 480 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → ((𝑉 UnivVertex 𝐸) = 𝑉 ↔ {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} = 𝑉)) |
9 | | df-ral 2901 |
. . . . 5
⊢
(∀𝑥 ∈
𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸 ↔ ∀𝑥(𝑥 ∈ 𝑉 → ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸)) |
10 | | bicom 211 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ↔ (𝑥 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸)) ↔ ((𝑥 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸) ↔ 𝑥 ∈ 𝑉)) |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → ((𝑥 ∈ 𝑉 ↔ (𝑥 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸)) ↔ ((𝑥 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸) ↔ 𝑥 ∈ 𝑉))) |
12 | | pm4.71 660 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 → ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸) ↔ (𝑥 ∈ 𝑉 ↔ (𝑥 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸))) |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → ((𝑥 ∈ 𝑉 → ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸) ↔ (𝑥 ∈ 𝑉 ↔ (𝑥 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸)))) |
14 | | sneq 4135 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑥 → {𝑘} = {𝑥}) |
15 | 14 | difeq2d 3690 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑥 → (𝑉 ∖ {𝑘}) = (𝑉 ∖ {𝑥})) |
16 | | preq2 4213 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑥 → {𝑛, 𝑘} = {𝑛, 𝑥}) |
17 | 16 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑥 → ({𝑛, 𝑘} ∈ ran 𝐸 ↔ {𝑛, 𝑥} ∈ ran 𝐸)) |
18 | 15, 17 | raleqbidv 3129 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑥 → (∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸)) |
19 | 18 | elrab 3331 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} ↔ (𝑥 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸)) |
20 | 19 | a1i 11 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → (𝑥 ∈ {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} ↔ (𝑥 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸))) |
21 | 20 | bibi1d 332 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → ((𝑥 ∈ {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} ↔ 𝑥 ∈ 𝑉) ↔ ((𝑥 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸) ↔ 𝑥 ∈ 𝑉))) |
22 | 11, 13, 21 | 3bitr4d 299 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → ((𝑥 ∈ 𝑉 → ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸) ↔ (𝑥 ∈ {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} ↔ 𝑥 ∈ 𝑉))) |
23 | 22 | albidv 1836 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → (∀𝑥(𝑥 ∈ 𝑉 → ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸) ↔ ∀𝑥(𝑥 ∈ {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} ↔ 𝑥 ∈ 𝑉))) |
24 | 9, 23 | syl5bb 271 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → (∀𝑥 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸 ↔ ∀𝑥(𝑥 ∈ {𝑘 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸} ↔ 𝑥 ∈ 𝑉))) |
25 | 5, 8, 24 | 3bitr4rd 300 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → (∀𝑥 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑥}){𝑛, 𝑥} ∈ ran 𝐸 ↔ (𝑉 UnivVertex 𝐸) = 𝑉)) |
26 | 3, 25 | bitrd 267 |
. 2
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑉 USGrph 𝐸) → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 UnivVertex 𝐸) = 𝑉)) |
27 | 1, 26 | mpancom 700 |
1
⊢ (𝑉 USGrph 𝐸 → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 UnivVertex 𝐸) = 𝑉)) |