Metamath Proof Explorer


Theorem prprval

Description: The set of all proper unordered pairs over a given set V . (Contributed by AV, 29-Apr-2023)

Ref Expression
Assertion prprval ( 𝑉𝑊 → ( Pairsproper𝑉 ) = { 𝑝 ∣ ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } )

Proof

Step Hyp Ref Expression
1 df-prpr Pairsproper = ( 𝑣 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎𝑣𝑏𝑣 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } )
2 rexeq ( 𝑣 = 𝑉 → ( ∃ 𝑏𝑣 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) ) )
3 2 rexeqbi1dv ( 𝑣 = 𝑉 → ( ∃ 𝑎𝑣𝑏𝑣 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) ) )
4 3 abbidv ( 𝑣 = 𝑉 → { 𝑝 ∣ ∃ 𝑎𝑣𝑏𝑣 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } = { 𝑝 ∣ ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } )
5 4 adantl ( ( 𝑉𝑊𝑣 = 𝑉 ) → { 𝑝 ∣ ∃ 𝑎𝑣𝑏𝑣 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } = { 𝑝 ∣ ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } )
6 elex ( 𝑉𝑊𝑉 ∈ V )
7 simpr ( ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) → 𝑝 = { 𝑎 , 𝑏 } )
8 7 ss2abi { 𝑝 ∣ ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ⊆ { 𝑝𝑝 = { 𝑎 , 𝑏 } }
9 zfpair2 { 𝑎 , 𝑏 } ∈ V
10 9 eueqi ∃! 𝑝 𝑝 = { 𝑎 , 𝑏 }
11 euabex ( ∃! 𝑝 𝑝 = { 𝑎 , 𝑏 } → { 𝑝𝑝 = { 𝑎 , 𝑏 } } ∈ V )
12 10 11 mp1i ( 𝑉𝑊 → { 𝑝𝑝 = { 𝑎 , 𝑏 } } ∈ V )
13 ssexg ( ( { 𝑝 ∣ ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ⊆ { 𝑝𝑝 = { 𝑎 , 𝑏 } } ∧ { 𝑝𝑝 = { 𝑎 , 𝑏 } } ∈ V ) → { 𝑝 ∣ ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ∈ V )
14 8 12 13 sylancr ( 𝑉𝑊 → { 𝑝 ∣ ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ∈ V )
15 14 ralrimivw ( 𝑉𝑊 → ∀ 𝑏𝑉 { 𝑝 ∣ ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ∈ V )
16 abrexex2g ( ( 𝑉𝑊 ∧ ∀ 𝑏𝑉 { 𝑝 ∣ ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ∈ V ) → { 𝑝 ∣ ∃ 𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ∈ V )
17 15 16 mpdan ( 𝑉𝑊 → { 𝑝 ∣ ∃ 𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ∈ V )
18 17 ralrimivw ( 𝑉𝑊 → ∀ 𝑎𝑉 { 𝑝 ∣ ∃ 𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ∈ V )
19 abrexex2g ( ( 𝑉𝑊 ∧ ∀ 𝑎𝑉 { 𝑝 ∣ ∃ 𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ∈ V ) → { 𝑝 ∣ ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ∈ V )
20 18 19 mpdan ( 𝑉𝑊 → { 𝑝 ∣ ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } ∈ V )
21 1 5 6 20 fvmptd2 ( 𝑉𝑊 → ( Pairsproper𝑉 ) = { 𝑝 ∣ ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑝 = { 𝑎 , 𝑏 } ) } )