Step |
Hyp |
Ref |
Expression |
1 |
|
paddfval.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
paddfval.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
paddfval.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
paddfval.p |
⊢ + = ( +𝑃 ‘ 𝐾 ) |
5 |
|
elex |
⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V ) |
6 |
|
fveq2 |
⊢ ( ℎ = 𝐾 → ( Atoms ‘ ℎ ) = ( Atoms ‘ 𝐾 ) ) |
7 |
6 3
|
eqtr4di |
⊢ ( ℎ = 𝐾 → ( Atoms ‘ ℎ ) = 𝐴 ) |
8 |
7
|
pweqd |
⊢ ( ℎ = 𝐾 → 𝒫 ( Atoms ‘ ℎ ) = 𝒫 𝐴 ) |
9 |
|
eqidd |
⊢ ( ℎ = 𝐾 → 𝑝 = 𝑝 ) |
10 |
|
fveq2 |
⊢ ( ℎ = 𝐾 → ( le ‘ ℎ ) = ( le ‘ 𝐾 ) ) |
11 |
10 1
|
eqtr4di |
⊢ ( ℎ = 𝐾 → ( le ‘ ℎ ) = ≤ ) |
12 |
|
fveq2 |
⊢ ( ℎ = 𝐾 → ( join ‘ ℎ ) = ( join ‘ 𝐾 ) ) |
13 |
12 2
|
eqtr4di |
⊢ ( ℎ = 𝐾 → ( join ‘ ℎ ) = ∨ ) |
14 |
13
|
oveqd |
⊢ ( ℎ = 𝐾 → ( 𝑞 ( join ‘ ℎ ) 𝑟 ) = ( 𝑞 ∨ 𝑟 ) ) |
15 |
9 11 14
|
breq123d |
⊢ ( ℎ = 𝐾 → ( 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) ↔ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) |
16 |
15
|
2rexbidv |
⊢ ( ℎ = 𝐾 → ( ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) ) |
17 |
7 16
|
rabeqbidv |
⊢ ( ℎ = 𝐾 → { 𝑝 ∈ ( Atoms ‘ ℎ ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) } = { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) |
18 |
17
|
uneq2d |
⊢ ( ℎ = 𝐾 → ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ ℎ ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) } ) = ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) |
19 |
8 8 18
|
mpoeq123dv |
⊢ ( ℎ = 𝐾 → ( 𝑚 ∈ 𝒫 ( Atoms ‘ ℎ ) , 𝑛 ∈ 𝒫 ( Atoms ‘ ℎ ) ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ ℎ ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) } ) ) = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) ) |
20 |
|
df-padd |
⊢ +𝑃 = ( ℎ ∈ V ↦ ( 𝑚 ∈ 𝒫 ( Atoms ‘ ℎ ) , 𝑛 ∈ 𝒫 ( Atoms ‘ ℎ ) ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ ℎ ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) } ) ) ) |
21 |
3
|
fvexi |
⊢ 𝐴 ∈ V |
22 |
21
|
pwex |
⊢ 𝒫 𝐴 ∈ V |
23 |
22 22
|
mpoex |
⊢ ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) ∈ V |
24 |
19 20 23
|
fvmpt |
⊢ ( 𝐾 ∈ V → ( +𝑃 ‘ 𝐾 ) = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) ) |
25 |
4 24
|
syl5eq |
⊢ ( 𝐾 ∈ V → + = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) ) |
26 |
5 25
|
syl |
⊢ ( 𝐾 ∈ 𝐵 → + = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) ) |