Step | Hyp | Ref
| Expression |
1 | | biid 264 |
. 2
⊢ (𝐾 ∈ 𝐵 ↔ 𝐾 ∈ 𝐵) |
2 | | paddfval.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
3 | 2 | fvexi 6731 |
. . 3
⊢ 𝐴 ∈ V |
4 | 3 | elpw2 5238 |
. 2
⊢ (𝑋 ∈ 𝒫 𝐴 ↔ 𝑋 ⊆ 𝐴) |
5 | 3 | elpw2 5238 |
. 2
⊢ (𝑌 ∈ 𝒫 𝐴 ↔ 𝑌 ⊆ 𝐴) |
6 | | paddfval.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
7 | | paddfval.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
8 | | paddfval.p |
. . . . . 6
⊢ + =
(+𝑃‘𝐾) |
9 | 6, 7, 2, 8 | paddfval 37548 |
. . . . 5
⊢ (𝐾 ∈ 𝐵 → + = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |
10 | 9 | oveqd 7230 |
. . . 4
⊢ (𝐾 ∈ 𝐵 → (𝑋 + 𝑌) = (𝑋(𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))𝑌)) |
11 | 10 | 3ad2ant1 1135 |
. . 3
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → (𝑋 + 𝑌) = (𝑋(𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))𝑌)) |
12 | | simpl 486 |
. . . . . 6
⊢ ((𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → 𝑋 ∈ 𝒫 𝐴) |
13 | | simpr 488 |
. . . . . 6
⊢ ((𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → 𝑌 ∈ 𝒫 𝐴) |
14 | | unexg 7534 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → (𝑋 ∪ 𝑌) ∈ V) |
15 | 3 | rabex 5225 |
. . . . . . 7
⊢ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)} ∈ V |
16 | | unexg 7534 |
. . . . . . 7
⊢ (((𝑋 ∪ 𝑌) ∈ V ∧ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)} ∈ V) → ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}) ∈ V) |
17 | 14, 15, 16 | sylancl 589 |
. . . . . 6
⊢ ((𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}) ∈ V) |
18 | 12, 13, 17 | 3jca 1130 |
. . . . 5
⊢ ((𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → (𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ∧ ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}) ∈ V)) |
19 | 18 | 3adant1 1132 |
. . . 4
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → (𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ∧ ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}) ∈ V)) |
20 | | uneq1 4070 |
. . . . . 6
⊢ (𝑚 = 𝑋 → (𝑚 ∪ 𝑛) = (𝑋 ∪ 𝑛)) |
21 | | rexeq 3320 |
. . . . . . 7
⊢ (𝑚 = 𝑋 → (∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟) ↔ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟))) |
22 | 21 | rabbidv 3390 |
. . . . . 6
⊢ (𝑚 = 𝑋 → {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)} = {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}) |
23 | 20, 22 | uneq12d 4078 |
. . . . 5
⊢ (𝑚 = 𝑋 → ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}) = ((𝑋 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)})) |
24 | | uneq2 4071 |
. . . . . 6
⊢ (𝑛 = 𝑌 → (𝑋 ∪ 𝑛) = (𝑋 ∪ 𝑌)) |
25 | | rexeq 3320 |
. . . . . . . 8
⊢ (𝑛 = 𝑌 → (∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟) ↔ ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟))) |
26 | 25 | rexbidv 3216 |
. . . . . . 7
⊢ (𝑛 = 𝑌 → (∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟) ↔ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟))) |
27 | 26 | rabbidv 3390 |
. . . . . 6
⊢ (𝑛 = 𝑌 → {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)} = {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}) |
28 | 24, 27 | uneq12d 4078 |
. . . . 5
⊢ (𝑛 = 𝑌 → ((𝑋 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)})) |
29 | | eqid 2737 |
. . . . 5
⊢ (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)})) = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)})) |
30 | 23, 28, 29 | ovmpog 7368 |
. . . 4
⊢ ((𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ∧ ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}) ∈ V) → (𝑋(𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))𝑌) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)})) |
31 | 19, 30 | syl 17 |
. . 3
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → (𝑋(𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))𝑌) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)})) |
32 | 11, 31 | eqtrd 2777 |
. 2
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → (𝑋 + 𝑌) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)})) |
33 | 1, 4, 5, 32 | syl3anbr 1164 |
1
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)})) |