Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. 2
⊢ (𝐾 ∈ 𝐵 → 𝐾 ∈ V) |
2 | | lineset.n |
. . 3
⊢ 𝑁 = (Lines‘𝐾) |
3 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) |
4 | | lineset.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
5 | 3, 4 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) |
6 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) |
7 | | lineset.l |
. . . . . . . . . . . . 13
⊢ ≤ =
(le‘𝐾) |
8 | 6, 7 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) |
9 | 8 | breqd 4594 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟) ↔ 𝑝 ≤ (𝑞(join‘𝑘)𝑟))) |
10 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾)) |
11 | | lineset.j |
. . . . . . . . . . . . . 14
⊢ ∨ =
(join‘𝐾) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ ) |
13 | 12 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (𝑞(join‘𝑘)𝑟) = (𝑞 ∨ 𝑟)) |
14 | 13 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (𝑝 ≤ (𝑞(join‘𝑘)𝑟) ↔ 𝑝 ≤ (𝑞 ∨ 𝑟))) |
15 | 9, 14 | bitrd 267 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟) ↔ 𝑝 ≤ (𝑞 ∨ 𝑟))) |
16 | 5, 15 | rabeqbidv 3168 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)} = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}) |
17 | 16 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)} ↔ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})) |
18 | 17 | anbi2d 736 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}) ↔ (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |
19 | 5, 18 | rexeqbidv 3130 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}) ↔ ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |
20 | 5, 19 | rexeqbidv 3130 |
. . . . 5
⊢ (𝑘 = 𝐾 → (∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}) ↔ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |
21 | 20 | abbidv 2728 |
. . . 4
⊢ (𝑘 = 𝐾 → {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})} = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})}) |
22 | | df-lines 33805 |
. . . 4
⊢ Lines =
(𝑘 ∈ V ↦ {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})}) |
23 | | fvex 6113 |
. . . . . 6
⊢
(Atoms‘𝐾)
∈ V |
24 | 4, 23 | eqeltri 2684 |
. . . . 5
⊢ 𝐴 ∈ V |
25 | | df-sn 4126 |
. . . . . . 7
⊢ {{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}} = {𝑠 ∣ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}} |
26 | | snex 4835 |
. . . . . . 7
⊢ {{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}} ∈ V |
27 | 25, 26 | eqeltrri 2685 |
. . . . . 6
⊢ {𝑠 ∣ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}} ∈ V |
28 | | simpr 476 |
. . . . . . 7
⊢ ((𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}) → 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}) |
29 | 28 | ss2abi 3637 |
. . . . . 6
⊢ {𝑠 ∣ (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})} ⊆ {𝑠 ∣ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}} |
30 | 27, 29 | ssexi 4731 |
. . . . 5
⊢ {𝑠 ∣ (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})} ∈ V |
31 | 24, 24, 30 | ab2rexex2 7051 |
. . . 4
⊢ {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})} ∈ V |
32 | 21, 22, 31 | fvmpt 6191 |
. . 3
⊢ (𝐾 ∈ V →
(Lines‘𝐾) = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})}) |
33 | 2, 32 | syl5eq 2656 |
. 2
⊢ (𝐾 ∈ V → 𝑁 = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})}) |
34 | 1, 33 | syl 17 |
1
⊢ (𝐾 ∈ 𝐵 → 𝑁 = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})}) |