Step | Hyp | Ref
| Expression |
1 | | structtousgr.p |
. . 3
⊢ 𝑃 = {𝑥 ∈ 𝒫 (Base‘𝑆) ∣ (#‘𝑥) = 2} |
2 | | structtousgr.s |
. . 3
⊢ (𝜑 → 𝑆 Struct 𝑋) |
3 | | structtousgr.g |
. . 3
⊢ 𝐺 = (𝑆 sSet 〈(.ef‘ndx), ( I ↾
𝑃)〉) |
4 | | structtousgr.b |
. . 3
⊢ (𝜑 → (Base‘ndx) ∈
dom 𝑆) |
5 | 1, 2, 3, 4 | structtousgr 26341 |
. 2
⊢ (𝜑 → 𝐺 ∈ USGraph ) |
6 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) → 𝑣 ∈ (Vtx‘𝐺)) |
7 | | eldifi 3732 |
. . . . . . . 8
⊢ (𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣}) → 𝑛 ∈ (Vtx‘𝐺)) |
8 | 6, 7 | anim12ci 591 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → (𝑛 ∈ (Vtx‘𝐺) ∧ 𝑣 ∈ (Vtx‘𝐺))) |
9 | | eldifsni 4320 |
. . . . . . . 8
⊢ (𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣}) → 𝑛 ≠ 𝑣) |
10 | 9 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → 𝑛 ≠ 𝑣) |
11 | | fvexd 6203 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → (Base‘𝑆) ∈ V) |
12 | 3 | fveq2i 6194 |
. . . . . . . . . . . . . 14
⊢
(Vtx‘𝐺) =
(Vtx‘(𝑆 sSet
〈(.ef‘ndx), ( I ↾ 𝑃)〉)) |
13 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(.ef‘ndx) = (.ef‘ndx) |
14 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝑆)
∈ V |
15 | 1 | cusgrexilem1 26335 |
. . . . . . . . . . . . . . . 16
⊢
((Base‘𝑆)
∈ V → ( I ↾ 𝑃) ∈ V) |
16 | 14, 15 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ( I ↾ 𝑃) ∈ V) |
17 | 13, 2, 4, 16 | setsvtx 25927 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (Vtx‘(𝑆 sSet 〈(.ef‘ndx), ( I
↾ 𝑃)〉)) =
(Base‘𝑆)) |
18 | 12, 17 | syl5eq 2668 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Vtx‘𝐺) = (Base‘𝑆)) |
19 | 18 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑣 ∈ (Vtx‘𝐺) ↔ 𝑣 ∈ (Base‘𝑆))) |
20 | 19 | biimpd 219 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑣 ∈ (Vtx‘𝐺) → 𝑣 ∈ (Base‘𝑆))) |
21 | 20 | imp 445 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) → 𝑣 ∈ (Base‘𝑆)) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → 𝑣 ∈ (Base‘𝑆)) |
23 | 18 | difeq1d 3727 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((Vtx‘𝐺) ∖ {𝑣}) = ((Base‘𝑆) ∖ {𝑣})) |
24 | 23 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣}) ↔ 𝑛 ∈ ((Base‘𝑆) ∖ {𝑣}))) |
25 | 24 | biimpd 219 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣}) → 𝑛 ∈ ((Base‘𝑆) ∖ {𝑣}))) |
26 | 25 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣}) → 𝑛 ∈ ((Base‘𝑆) ∖ {𝑣}))) |
27 | 26 | imp 445 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → 𝑛 ∈ ((Base‘𝑆) ∖ {𝑣})) |
28 | 1 | cusgrexilem2 26338 |
. . . . . . . . 9
⊢
((((Base‘𝑆)
∈ V ∧ 𝑣 ∈
(Base‘𝑆)) ∧ 𝑛 ∈ ((Base‘𝑆) ∖ {𝑣})) → ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒) |
29 | 11, 22, 27, 28 | syl21anc 1325 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒) |
30 | | edgval 25941 |
. . . . . . . . . . 11
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
31 | 3 | fveq2i 6194 |
. . . . . . . . . . . . 13
⊢
(iEdg‘𝐺) =
(iEdg‘(𝑆 sSet
〈(.ef‘ndx), ( I ↾ 𝑃)〉)) |
32 | 13, 2, 4, 16 | setsiedg 25928 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (iEdg‘(𝑆 sSet 〈(.ef‘ndx), ( I
↾ 𝑃)〉)) = ( I
↾ 𝑃)) |
33 | 31, 32 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ (𝜑 → (iEdg‘𝐺) = ( I ↾ 𝑃)) |
34 | 33 | rneqd 5353 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (iEdg‘𝐺) = ran ( I ↾ 𝑃)) |
35 | 30, 34 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (𝜑 → (Edg‘𝐺) = ran ( I ↾ 𝑃)) |
36 | 35 | rexeqdv 3145 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒)) |
37 | 36 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → (∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒)) |
38 | 29, 37 | mpbird 247 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → ∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒) |
39 | 5 | elexd 3214 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ V) |
40 | 39 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → 𝐺 ∈ V) |
41 | | eqid 2622 |
. . . . . . . . 9
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
42 | | eqid 2622 |
. . . . . . . . 9
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
43 | 41, 42 | nbgrel 26238 |
. . . . . . . 8
⊢ (𝐺 ∈ V → (𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ ((𝑛 ∈ (Vtx‘𝐺) ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ≠ 𝑣 ∧ ∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒))) |
44 | 40, 43 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → (𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ ((𝑛 ∈ (Vtx‘𝐺) ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ≠ 𝑣 ∧ ∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒))) |
45 | 8, 10, 38, 44 | mpbir3and 1245 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) ∧ 𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})) → 𝑛 ∈ (𝐺 NeighbVtx 𝑣)) |
46 | 45 | ralrimiva 2966 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) → ∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)) |
47 | 39 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) → 𝐺 ∈ V) |
48 | 41 | uvtxael 26288 |
. . . . . 6
⊢ (𝐺 ∈ V → (𝑣 ∈ (UnivVtx‘𝐺) ↔ (𝑣 ∈ (Vtx‘𝐺) ∧ ∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)))) |
49 | 47, 48 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝑣 ∈ (UnivVtx‘𝐺) ↔ (𝑣 ∈ (Vtx‘𝐺) ∧ ∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)))) |
50 | 6, 46, 49 | mpbir2and 957 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ (Vtx‘𝐺)) → 𝑣 ∈ (UnivVtx‘𝐺)) |
51 | 50 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑣 ∈ (Vtx‘𝐺)𝑣 ∈ (UnivVtx‘𝐺)) |
52 | 41 | iscplgr 26310 |
. . . 4
⊢ (𝐺 ∈ V → (𝐺 ∈ ComplGraph ↔
∀𝑣 ∈
(Vtx‘𝐺)𝑣 ∈ (UnivVtx‘𝐺))) |
53 | 39, 52 | syl 17 |
. . 3
⊢ (𝜑 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ (Vtx‘𝐺)𝑣 ∈ (UnivVtx‘𝐺))) |
54 | 51, 53 | mpbird 247 |
. 2
⊢ (𝜑 → 𝐺 ∈ ComplGraph) |
55 | | iscusgr 26314 |
. 2
⊢ (𝐺 ∈ ComplUSGraph ↔
(𝐺 ∈ USGraph ∧
𝐺 ∈
ComplGraph)) |
56 | 5, 54, 55 | sylanbrc 698 |
1
⊢ (𝜑 → 𝐺 ∈ ComplUSGraph) |