![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uhgreq12g | Structured version Visualization version GIF version |
Description: If two sets have the same vertices and the same edges, one set is a hypergraph iff the other set is a hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.) |
Ref | Expression |
---|---|
uhgrf.v | ⊢ 𝑉 = (Vtx‘𝐺) |
uhgrf.e | ⊢ 𝐸 = (iEdg‘𝐺) |
uhgreq12g.w | ⊢ 𝑊 = (Vtx‘𝐻) |
uhgreq12g.f | ⊢ 𝐹 = (iEdg‘𝐻) |
Ref | Expression |
---|---|
uhgreq12g | ⊢ (((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝐺 ∈ UHGraph ↔ 𝐻 ∈ UHGraph)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uhgrf.v | . . . . 5 ⊢ 𝑉 = (Vtx‘𝐺) | |
2 | uhgrf.e | . . . . 5 ⊢ 𝐸 = (iEdg‘𝐺) | |
3 | 1, 2 | isuhgr 28901 | . . . 4 ⊢ (𝐺 ∈ 𝑋 → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
4 | 3 | adantr 479 | . . 3 ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
5 | 4 | adantr 479 | . 2 ⊢ (((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
6 | simpr 483 | . . . 4 ⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → 𝐸 = 𝐹) | |
7 | 6 | dmeqd 5912 | . . . 4 ⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → dom 𝐸 = dom 𝐹) |
8 | pweq 4620 | . . . . . 6 ⊢ (𝑉 = 𝑊 → 𝒫 𝑉 = 𝒫 𝑊) | |
9 | 8 | difeq1d 4121 | . . . . 5 ⊢ (𝑉 = 𝑊 → (𝒫 𝑉 ∖ {∅}) = (𝒫 𝑊 ∖ {∅})) |
10 | 9 | adantr 479 | . . . 4 ⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → (𝒫 𝑉 ∖ {∅}) = (𝒫 𝑊 ∖ {∅})) |
11 | 6, 7, 10 | feq123d 6716 | . . 3 ⊢ ((𝑉 = 𝑊 ∧ 𝐸 = 𝐹) → (𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}) ↔ 𝐹:dom 𝐹⟶(𝒫 𝑊 ∖ {∅}))) |
12 | uhgreq12g.w | . . . . . 6 ⊢ 𝑊 = (Vtx‘𝐻) | |
13 | uhgreq12g.f | . . . . . 6 ⊢ 𝐹 = (iEdg‘𝐻) | |
14 | 12, 13 | isuhgr 28901 | . . . . 5 ⊢ (𝐻 ∈ 𝑌 → (𝐻 ∈ UHGraph ↔ 𝐹:dom 𝐹⟶(𝒫 𝑊 ∖ {∅}))) |
15 | 14 | adantl 480 | . . . 4 ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) → (𝐻 ∈ UHGraph ↔ 𝐹:dom 𝐹⟶(𝒫 𝑊 ∖ {∅}))) |
16 | 15 | bicomd 222 | . . 3 ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) → (𝐹:dom 𝐹⟶(𝒫 𝑊 ∖ {∅}) ↔ 𝐻 ∈ UHGraph)) |
17 | 11, 16 | sylan9bbr 509 | . 2 ⊢ (((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}) ↔ 𝐻 ∈ UHGraph)) |
18 | 5, 17 | bitrd 278 | 1 ⊢ (((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝐺 ∈ UHGraph ↔ 𝐻 ∈ UHGraph)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ∈ wcel 2098 ∖ cdif 3946 ∅c0 4326 𝒫 cpw 4606 {csn 4632 dom cdm 5682 ⟶wf 6549 ‘cfv 6553 Vtxcvtx 28837 iEdgciedg 28838 UHGraphcuhgr 28897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 ax-nul 5310 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-rab 3431 df-v 3475 df-sbc 3779 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-pw 4608 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-br 5153 df-opab 5215 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-iota 6505 df-fun 6555 df-fn 6556 df-f 6557 df-fv 6561 df-uhgr 28899 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |