Metamath Proof Explorer

Theorem sprsymrelfolem1

Description: Lemma 1 for sprsymrelfo . (Contributed by AV, 22-Nov-2021)

Ref Expression
Hypothesis sprsymrelfo.q ⊢ Q = q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a R b
Assertion sprsymrelfolem1 ⊢ Q ∈ 𝒫 Pairs ⁡ V

Proof

Step Hyp Ref Expression
1 sprsymrelfo.q ⊢ Q = q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a R b
2 fvex ⊢ Pairs ⁡ V ∈ V
3 ssrab2 ⊢ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a R b ⊆ Pairs ⁡ V
4 2 3 elpwi2 ⊢ q ∈ Pairs ⁡ V | ∀ a ∈ V ∀ b ∈ V q = a b → a R b ∈ 𝒫 Pairs ⁡ V
5 1 4 eqeltri ⊢ Q ∈ 𝒫 Pairs ⁡ V