Description: The property of an unordered pair to be an alternatively defined simple graph, defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ausgr.1 | ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } } | |
| Assertion | isausgr | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( 𝑉 𝐺 𝐸 ↔ 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ausgr.1 | ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } } | |
| 2 | simpr | ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → 𝑒 = 𝐸 ) | |
| 3 | pweq | ⊢ ( 𝑣 = 𝑉 → 𝒫 𝑣 = 𝒫 𝑉 ) | |
| 4 | 3 | adantr | ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → 𝒫 𝑣 = 𝒫 𝑉 ) |
| 5 | 4 | rabeqdv | ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
| 6 | 2 5 | sseq12d | ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
| 7 | 6 1 | brabga | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( 𝑉 𝐺 𝐸 ↔ 𝐸 ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |