Theorem sprval

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

	Ref	Expression
Assertion	sprval	⊢ ( 𝑉 ∈ 𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )

Proof

Step	Hyp	Ref	Expression
1		df-spr	⊢ Pairs = ( 𝑣 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 } } )
2	1	a1i	⊢ ( 𝑉 ∈ 𝑊 → Pairs = ( 𝑣 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 } } ) )
3		id	⊢ ( 𝑣 = 𝑉 → 𝑣 = 𝑉 )
4		rexeq	⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
5	3 4	rexeqbidv	⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
6	5	adantl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑣 = 𝑉 ) → ( ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
7	6	abbidv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑣 = 𝑉 ) → { 𝑝 ∣ ∃ 𝑎 ∈ 𝑣 ∃ 𝑏 ∈ 𝑣 𝑝 = { 𝑎 , 𝑏 } } = { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )
8		elex	⊢ ( 𝑉 ∈ 𝑊 → 𝑉 ∈ V )
9		zfpair2	⊢ { 𝑎 , 𝑏 } ∈ V
10		eueq	⊢ ( { 𝑎 , 𝑏 } ∈ V ↔ ∃! 𝑝 𝑝 = { 𝑎 , 𝑏 } )
11	9 10	mpbi	⊢ ∃! 𝑝 𝑝 = { 𝑎 , 𝑏 }
12		euabex	⊢ ( ∃! 𝑝 𝑝 = { 𝑎 , 𝑏 } → { 𝑝 ∣ 𝑝 = { 𝑎 , 𝑏 } } ∈ V )
13	11 12	mp1i	⊢ ( 𝑉 ∈ 𝑊 → { 𝑝 ∣ 𝑝 = { 𝑎 , 𝑏 } } ∈ V )
14	13	ralrimivw	⊢ ( 𝑉 ∈ 𝑊 → ∀ 𝑏 ∈ 𝑉 { 𝑝 ∣ 𝑝 = { 𝑎 , 𝑏 } } ∈ V )
15		abrexex2g	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ∀ 𝑏 ∈ 𝑉 { 𝑝 ∣ 𝑝 = { 𝑎 , 𝑏 } } ∈ V ) → { 𝑝 ∣ ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ∈ V )
16	14 15	mpdan	⊢ ( 𝑉 ∈ 𝑊 → { 𝑝 ∣ ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ∈ V )
17	16	ralrimivw	⊢ ( 𝑉 ∈ 𝑊 → ∀ 𝑎 ∈ 𝑉 { 𝑝 ∣ ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ∈ V )
18		abrexex2g	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ∀ 𝑎 ∈ 𝑉 { 𝑝 ∣ ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ∈ V ) → { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ∈ V )
19	17 18	mpdan	⊢ ( 𝑉 ∈ 𝑊 → { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ∈ V )
20	2 7 8 19	fvmptd	⊢ ( 𝑉 ∈ 𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )