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