Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | eqid 2610 |
. . . . . 6
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
3 | 1, 2 | iscplgredg 40639 |
. . . . 5
⊢ (𝐺 ∈ ComplGraph → (𝐺 ∈ ComplGraph ↔
∀𝑣 ∈
(Vtx‘𝐺)∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒)) |
4 | | edgaval 25794 |
. . . . . 6
⊢ (𝐺 ∈ ComplGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
5 | | simpl 472 |
. . . . . . . . . . . 12
⊢
(((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺)) →
(Vtx‘𝑔) =
(Vtx‘𝐺)) |
6 | 5 | adantl 481 |
. . . . . . . . . . 11
⊢
(((Edg‘𝐺) =
ran (iEdg‘𝐺) ∧
((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺))) →
(Vtx‘𝑔) =
(Vtx‘𝐺)) |
7 | 5 | difeq1d 3689 |
. . . . . . . . . . . . 13
⊢
(((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺)) →
((Vtx‘𝑔) ∖
{𝑣}) = ((Vtx‘𝐺) ∖ {𝑣})) |
8 | 7 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((Edg‘𝐺) =
ran (iEdg‘𝐺) ∧
((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺))) →
((Vtx‘𝑔) ∖
{𝑣}) = ((Vtx‘𝐺) ∖ {𝑣})) |
9 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑔 ∈ V |
10 | | edgaval 25794 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ∈ V →
(Edg‘𝑔) = ran
(iEdg‘𝑔)) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(Edg‘𝑔) = ran
(iEdg‘𝑔) |
12 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢
(((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺)) →
(iEdg‘𝑔) =
(iEdg‘𝐺)) |
13 | 12 | rneqd 5274 |
. . . . . . . . . . . . . . . 16
⊢
(((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺)) → ran
(iEdg‘𝑔) = ran
(iEdg‘𝐺)) |
14 | 11, 13 | syl5eq 2656 |
. . . . . . . . . . . . . . 15
⊢
(((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺)) →
(Edg‘𝑔) = ran
(iEdg‘𝐺)) |
15 | 14 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((Edg‘𝐺) =
ran (iEdg‘𝐺) ∧
((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺))) →
(Edg‘𝑔) = ran
(iEdg‘𝐺)) |
16 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢
(((Edg‘𝐺) =
ran (iEdg‘𝐺) ∧
((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺))) →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
17 | 15, 16 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢
(((Edg‘𝐺) =
ran (iEdg‘𝐺) ∧
((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺))) →
(Edg‘𝑔) =
(Edg‘𝐺)) |
18 | 17 | rexeqdv 3122 |
. . . . . . . . . . . 12
⊢
(((Edg‘𝐺) =
ran (iEdg‘𝐺) ∧
((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺))) →
(∃𝑒 ∈
(Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒)) |
19 | 8, 18 | raleqbidv 3129 |
. . . . . . . . . . 11
⊢
(((Edg‘𝐺) =
ran (iEdg‘𝐺) ∧
((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺))) →
(∀𝑛 ∈
((Vtx‘𝑔) ∖
{𝑣})∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒 ↔ ∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒)) |
20 | 6, 19 | raleqbidv 3129 |
. . . . . . . . . 10
⊢
(((Edg‘𝐺) =
ran (iEdg‘𝐺) ∧
((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺))) →
(∀𝑣 ∈
(Vtx‘𝑔)∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒 ↔ ∀𝑣 ∈ (Vtx‘𝐺)∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒)) |
21 | 20 | biimpar 501 |
. . . . . . . . 9
⊢
((((Edg‘𝐺) =
ran (iEdg‘𝐺) ∧
((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺))) ∧
∀𝑣 ∈
(Vtx‘𝐺)∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒) → ∀𝑣 ∈ (Vtx‘𝑔)∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒) |
22 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Vtx‘𝑔) =
(Vtx‘𝑔) |
23 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Edg‘𝑔) =
(Edg‘𝑔) |
24 | 22, 23 | iscplgredg 40639 |
. . . . . . . . . 10
⊢ (𝑔 ∈ V → (𝑔 ∈ ComplGraph ↔
∀𝑣 ∈
(Vtx‘𝑔)∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒)) |
25 | 9, 24 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑔 ∈ ComplGraph ↔
∀𝑣 ∈
(Vtx‘𝑔)∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒) |
26 | 21, 25 | sylibr 223 |
. . . . . . . 8
⊢
((((Edg‘𝐺) =
ran (iEdg‘𝐺) ∧
((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺))) ∧
∀𝑣 ∈
(Vtx‘𝐺)∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒) → 𝑔 ∈ ComplGraph) |
27 | 26 | expcom 450 |
. . . . . . 7
⊢
(∀𝑣 ∈
(Vtx‘𝐺)∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒 → (((Edg‘𝐺) = ran (iEdg‘𝐺) ∧ ((Vtx‘𝑔) = (Vtx‘𝐺) ∧ (iEdg‘𝑔) = (iEdg‘𝐺))) → 𝑔 ∈ ComplGraph)) |
28 | 27 | expd 451 |
. . . . . 6
⊢
(∀𝑣 ∈
(Vtx‘𝐺)∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒 → ((Edg‘𝐺) = ran (iEdg‘𝐺) → (((Vtx‘𝑔) = (Vtx‘𝐺) ∧ (iEdg‘𝑔) = (iEdg‘𝐺)) → 𝑔 ∈ ComplGraph))) |
29 | 4, 28 | syl5com 31 |
. . . . 5
⊢ (𝐺 ∈ ComplGraph →
(∀𝑣 ∈
(Vtx‘𝐺)∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝑣})∃𝑒 ∈ (Edg‘𝐺){𝑣, 𝑛} ⊆ 𝑒 → (((Vtx‘𝑔) = (Vtx‘𝐺) ∧ (iEdg‘𝑔) = (iEdg‘𝐺)) → 𝑔 ∈ ComplGraph))) |
30 | 3, 29 | sylbid 229 |
. . . 4
⊢ (𝐺 ∈ ComplGraph → (𝐺 ∈ ComplGraph →
(((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺)) →
𝑔 ∈
ComplGraph))) |
31 | 30 | pm2.43i 50 |
. . 3
⊢ (𝐺 ∈ ComplGraph →
(((Vtx‘𝑔) =
(Vtx‘𝐺) ∧
(iEdg‘𝑔) =
(iEdg‘𝐺)) →
𝑔 ∈
ComplGraph)) |
32 | 31 | alrimiv 1842 |
. 2
⊢ (𝐺 ∈ ComplGraph →
∀𝑔(((Vtx‘𝑔) = (Vtx‘𝐺) ∧ (iEdg‘𝑔) = (iEdg‘𝐺)) → 𝑔 ∈ ComplGraph)) |
33 | | fvex 6113 |
. . 3
⊢
(Vtx‘𝐺) ∈
V |
34 | 33 | a1i 11 |
. 2
⊢ (𝐺 ∈ ComplGraph →
(Vtx‘𝐺) ∈
V) |
35 | | fvex 6113 |
. . 3
⊢
(iEdg‘𝐺)
∈ V |
36 | 35 | a1i 11 |
. 2
⊢ (𝐺 ∈ ComplGraph →
(iEdg‘𝐺) ∈
V) |
37 | 32, 34, 36 | gropeld 25710 |
1
⊢ (𝐺 ∈ ComplGraph →
〈(Vtx‘𝐺),
(iEdg‘𝐺)〉 ∈
ComplGraph) |