Step | Hyp | Ref
| Expression |
1 | | df-frgr 41429 |
. . 3
⊢
FriendGraph = {𝑔 ∣
(𝑔 ∈ USGraph ∧
[(Vtx‘𝑔) /
𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)} |
2 | 1 | eleq2i 2680 |
. 2
⊢ (𝐺 ∈ FriendGraph ↔ 𝐺 ∈ {𝑔 ∣ (𝑔 ∈ USGraph ∧
[(Vtx‘𝑔) /
𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)}) |
3 | | eleq1 2676 |
. . . 4
⊢ (ℎ = 𝐺 → (ℎ ∈ USGraph ↔ 𝐺 ∈ USGraph )) |
4 | | fveq2 6103 |
. . . . . 6
⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = (Vtx‘𝐺)) |
5 | | isfrgr.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
6 | 4, 5 | syl6eqr 2662 |
. . . . 5
⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = 𝑉) |
7 | 6 | difeq1d 3689 |
. . . . . 6
⊢ (ℎ = 𝐺 → ((Vtx‘ℎ) ∖ {𝑘}) = (𝑉 ∖ {𝑘})) |
8 | | biidd 251 |
. . . . . . . . 9
⊢
((Vtx‘ℎ) =
𝑉 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))) |
9 | 8 | reueqd 3125 |
. . . . . . . 8
⊢
((Vtx‘ℎ) =
𝑉 → (∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))) |
10 | 6, 9 | syl 17 |
. . . . . . 7
⊢ (ℎ = 𝐺 → (∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))) |
11 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (ℎ = 𝐺 → (Edg‘ℎ) = (Edg‘𝐺)) |
12 | | isfrgr.e |
. . . . . . . . . 10
⊢ 𝐸 = (Edg‘𝐺) |
13 | 11, 12 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (ℎ = 𝐺 → (Edg‘ℎ) = 𝐸) |
14 | 13 | sseq2d 3596 |
. . . . . . . 8
⊢ (ℎ = 𝐺 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)) |
15 | 14 | reubidv 3103 |
. . . . . . 7
⊢ (ℎ = 𝐺 → (∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)) |
16 | 10, 15 | bitrd 267 |
. . . . . 6
⊢ (ℎ = 𝐺 → (∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)) |
17 | 7, 16 | raleqbidv 3129 |
. . . . 5
⊢ (ℎ = 𝐺 → (∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)) |
18 | 6, 17 | raleqbidv 3129 |
. . . 4
⊢ (ℎ = 𝐺 → (∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ) ↔ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)) |
19 | 3, 18 | anbi12d 743 |
. . 3
⊢ (ℎ = 𝐺 → ((ℎ ∈ USGraph ∧ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)) ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))) |
20 | | eleq1 2676 |
. . . . 5
⊢ (𝑔 = ℎ → (𝑔 ∈ USGraph ↔ ℎ ∈ USGraph )) |
21 | | fvex 6113 |
. . . . . . 7
⊢
(Vtx‘𝑔) ∈
V |
22 | 21 | a1i 11 |
. . . . . 6
⊢ (𝑔 = ℎ → (Vtx‘𝑔) ∈ V) |
23 | | fveq2 6103 |
. . . . . 6
⊢ (𝑔 = ℎ → (Vtx‘𝑔) = (Vtx‘ℎ)) |
24 | | fvex 6113 |
. . . . . . . 8
⊢
(Edg‘𝑔) ∈
V |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (Edg‘𝑔) ∈ V) |
26 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑔 = ℎ → (Edg‘𝑔) = (Edg‘ℎ)) |
27 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (Edg‘𝑔) = (Edg‘ℎ)) |
28 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → 𝑣 = (Vtx‘ℎ)) |
29 | 28 | adantr 480 |
. . . . . . . 8
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → 𝑣 = (Vtx‘ℎ)) |
30 | | difeq1 3683 |
. . . . . . . . . 10
⊢ (𝑣 = (Vtx‘ℎ) → (𝑣 ∖ {𝑘}) = ((Vtx‘ℎ) ∖ {𝑘})) |
31 | 30 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (𝑣 ∖ {𝑘}) = ((Vtx‘ℎ) ∖ {𝑘})) |
32 | | biidd 251 |
. . . . . . . . . . . 12
⊢ (𝑣 = (Vtx‘ℎ) → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)) |
33 | 32 | reueqd 3125 |
. . . . . . . . . . 11
⊢ (𝑣 = (Vtx‘ℎ) → (∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)) |
34 | 33 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)) |
35 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → 𝑒 = (Edg‘ℎ)) |
36 | 35 | sseq2d 3596 |
. . . . . . . . . . 11
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))) |
37 | 36 | reubidv 3103 |
. . . . . . . . . 10
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))) |
38 | 34, 37 | bitrd 267 |
. . . . . . . . 9
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))) |
39 | 31, 38 | raleqbidv 3129 |
. . . . . . . 8
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))) |
40 | 29, 39 | raleqbidv 3129 |
. . . . . . 7
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (Edg‘ℎ)) → (∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))) |
41 | 25, 27, 40 | sbcied2 3440 |
. . . . . 6
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → ([(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))) |
42 | 22, 23, 41 | sbcied2 3440 |
. . . . 5
⊢ (𝑔 = ℎ → ([(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒 ↔ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))) |
43 | 20, 42 | anbi12d 743 |
. . . 4
⊢ (𝑔 = ℎ → ((𝑔 ∈ USGraph ∧
[(Vtx‘𝑔) /
𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒) ↔ (ℎ ∈ USGraph ∧ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ)))) |
44 | 43 | cbvabv 2734 |
. . 3
⊢ {𝑔 ∣ (𝑔 ∈ USGraph ∧
[(Vtx‘𝑔) /
𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)} = {ℎ ∣ (ℎ ∈ USGraph ∧ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑙 ∈ ((Vtx‘ℎ) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘ℎ){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘ℎ))} |
45 | 19, 44 | elab2g 3322 |
. 2
⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ {𝑔 ∣ (𝑔 ∈ USGraph ∧
[(Vtx‘𝑔) /
𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)} ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))) |
46 | 2, 45 | syl5bb 271 |
1
⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧
∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))) |