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 ‘ 𝑉 ) = { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } )