Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. 2
⊢ (𝐾 ∈ 𝐵 → 𝐾 ∈ V) |
2 | | paddfval.p |
. . 3
⊢ + =
(+𝑃‘𝐾) |
3 | | fveq2 6103 |
. . . . . . 7
⊢ (ℎ = 𝐾 → (Atoms‘ℎ) = (Atoms‘𝐾)) |
4 | | paddfval.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
5 | 3, 4 | syl6eqr 2662 |
. . . . . 6
⊢ (ℎ = 𝐾 → (Atoms‘ℎ) = 𝐴) |
6 | 5 | pweqd 4113 |
. . . . 5
⊢ (ℎ = 𝐾 → 𝒫 (Atoms‘ℎ) = 𝒫 𝐴) |
7 | | eqidd 2611 |
. . . . . . . . 9
⊢ (ℎ = 𝐾 → 𝑝 = 𝑝) |
8 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (ℎ = 𝐾 → (le‘ℎ) = (le‘𝐾)) |
9 | | paddfval.l |
. . . . . . . . . 10
⊢ ≤ =
(le‘𝐾) |
10 | 8, 9 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (ℎ = 𝐾 → (le‘ℎ) = ≤ ) |
11 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (ℎ = 𝐾 → (join‘ℎ) = (join‘𝐾)) |
12 | | paddfval.j |
. . . . . . . . . . 11
⊢ ∨ =
(join‘𝐾) |
13 | 11, 12 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (ℎ = 𝐾 → (join‘ℎ) = ∨ ) |
14 | 13 | oveqd 6566 |
. . . . . . . . 9
⊢ (ℎ = 𝐾 → (𝑞(join‘ℎ)𝑟) = (𝑞 ∨ 𝑟)) |
15 | 7, 10, 14 | breq123d 4597 |
. . . . . . . 8
⊢ (ℎ = 𝐾 → (𝑝(le‘ℎ)(𝑞(join‘ℎ)𝑟) ↔ 𝑝 ≤ (𝑞 ∨ 𝑟))) |
16 | 15 | 2rexbidv 3039 |
. . . . . . 7
⊢ (ℎ = 𝐾 → (∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘ℎ)(𝑞(join‘ℎ)𝑟) ↔ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟))) |
17 | 5, 16 | rabeqbidv 3168 |
. . . . . 6
⊢ (ℎ = 𝐾 → {𝑝 ∈ (Atoms‘ℎ) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘ℎ)(𝑞(join‘ℎ)𝑟)} = {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}) |
18 | 17 | uneq2d 3729 |
. . . . 5
⊢ (ℎ = 𝐾 → ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘ℎ) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘ℎ)(𝑞(join‘ℎ)𝑟)}) = ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)})) |
19 | 6, 6, 18 | mpt2eq123dv 6615 |
. . . 4
⊢ (ℎ = 𝐾 → (𝑚 ∈ 𝒫 (Atoms‘ℎ), 𝑛 ∈ 𝒫 (Atoms‘ℎ) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘ℎ) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘ℎ)(𝑞(join‘ℎ)𝑟)})) = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |
20 | | df-padd 34100 |
. . . 4
⊢
+𝑃 = (ℎ ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘ℎ), 𝑛 ∈ 𝒫 (Atoms‘ℎ) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘ℎ) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘ℎ)(𝑞(join‘ℎ)𝑟)}))) |
21 | | fvex 6113 |
. . . . . . 7
⊢
(Atoms‘𝐾)
∈ V |
22 | 4, 21 | eqeltri 2684 |
. . . . . 6
⊢ 𝐴 ∈ V |
23 | 22 | pwex 4774 |
. . . . 5
⊢ 𝒫
𝐴 ∈ V |
24 | 23, 23 | mpt2ex 7136 |
. . . 4
⊢ (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)})) ∈ V |
25 | 19, 20, 24 | fvmpt 6191 |
. . 3
⊢ (𝐾 ∈ V →
(+𝑃‘𝐾) = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |
26 | 2, 25 | syl5eq 2656 |
. 2
⊢ (𝐾 ∈ V → + = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |
27 | 1, 26 | syl 17 |
1
⊢ (𝐾 ∈ 𝐵 → + = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |