Theorem sprssspr

Description: The set of all unordered pairs over a given set V is a subset of the set of all unordered pairs. (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	sprssspr	⊢ ( Pairs ‘ 𝑉 ) ⊆ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } }

Proof

Step	Hyp	Ref	Expression
1		sprval	⊢ ( 𝑉 ∈ V → ( Pairs ‘ 𝑉 ) = { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )
2		r2ex	⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑝 = { 𝑎 , 𝑏 } ) )
3		simpr	⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑝 = { 𝑎 , 𝑏 } ) → 𝑝 = { 𝑎 , 𝑏 } )
4	3	2eximi	⊢ ( ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } )
5	2 4	sylbi	⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } → ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } )
6	5	ax-gen	⊢ ∀ 𝑝 ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } → ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } )
7	6	a1i	⊢ ( 𝑉 ∈ V → ∀ 𝑝 ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } → ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } ) )
8		ss2ab	⊢ ( { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ⊆ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } ↔ ∀ 𝑝 ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } → ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } ) )
9	7 8	sylibr	⊢ ( 𝑉 ∈ V → { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ⊆ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } )
10	1 9	eqsstrd	⊢ ( 𝑉 ∈ V → ( Pairs ‘ 𝑉 ) ⊆ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } )
11		fvprc	⊢ ( ¬ 𝑉 ∈ V → ( Pairs ‘ 𝑉 ) = ∅ )
12		0ss	⊢ ∅ ⊆ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } }
13	12	a1i	⊢ ( ¬ 𝑉 ∈ V → ∅ ⊆ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } )
14	11 13	eqsstrd	⊢ ( ¬ 𝑉 ∈ V → ( Pairs ‘ 𝑉 ) ⊆ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } } )
15	10 14	pm2.61i	⊢ ( Pairs ‘ 𝑉 ) ⊆ { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } }