Description: The set G of the "simple pseudographs" with a fixed set of vertices V and the class R of the symmetric relations on the fixed set V are equinumerous. For more details about the class G of all "simple pseudographs" see comments on uspgrbisymrel . (Contributed by AV, 27-Nov-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | uspgrbisymrel.g | ⊢ 𝐺 = { 〈 𝑣 , 𝑒 〉 ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } | |
uspgrbisymrel.r | ⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) } | ||
Assertion | uspgrymrelen | ⊢ ( 𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑅 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uspgrbisymrel.g | ⊢ 𝐺 = { 〈 𝑣 , 𝑒 〉 ∣ ( 𝑣 = 𝑉 ∧ ∃ 𝑞 ∈ USPGraph ( ( Vtx ‘ 𝑞 ) = 𝑣 ∧ ( Edg ‘ 𝑞 ) = 𝑒 ) ) } | |
2 | uspgrbisymrel.r | ⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) } | |
3 | eqid | ⊢ 𝒫 ( Pairs ‘ 𝑉 ) = 𝒫 ( Pairs ‘ 𝑉 ) | |
4 | 3 1 | uspgrspren | ⊢ ( 𝑉 ∈ 𝑊 → 𝐺 ≈ 𝒫 ( Pairs ‘ 𝑉 ) ) |
5 | 3 2 | sprsymrelen | ⊢ ( 𝑉 ∈ 𝑊 → 𝒫 ( Pairs ‘ 𝑉 ) ≈ 𝑅 ) |
6 | entr | ⊢ ( ( 𝐺 ≈ 𝒫 ( Pairs ‘ 𝑉 ) ∧ 𝒫 ( Pairs ‘ 𝑉 ) ≈ 𝑅 ) → 𝐺 ≈ 𝑅 ) | |
7 | 4 5 6 | syl2anc | ⊢ ( 𝑉 ∈ 𝑊 → 𝐺 ≈ 𝑅 ) |