Step | Hyp | Ref
| Expression |
1 | | elex 3426 |
. 2
⊢ (𝐾 ∈ 𝐵 → 𝐾 ∈ V) |
2 | | lineset.n |
. . 3
⊢ 𝑁 = (Lines‘𝐾) |
3 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) |
4 | | lineset.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
5 | 3, 4 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) |
6 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) |
7 | | lineset.l |
. . . . . . . . . . . . 13
⊢ ≤ =
(le‘𝐾) |
8 | 6, 7 | eqtr4di 2796 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) |
9 | 8 | breqd 5064 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟) ↔ 𝑝 ≤ (𝑞(join‘𝑘)𝑟))) |
10 | | fveq2 6717 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾)) |
11 | | lineset.j |
. . . . . . . . . . . . . 14
⊢ ∨ =
(join‘𝐾) |
12 | 10, 11 | eqtr4di 2796 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ ) |
13 | 12 | oveqd 7230 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (𝑞(join‘𝑘)𝑟) = (𝑞 ∨ 𝑟)) |
14 | 13 | breq2d 5065 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (𝑝 ≤ (𝑞(join‘𝑘)𝑟) ↔ 𝑝 ≤ (𝑞 ∨ 𝑟))) |
15 | 9, 14 | bitrd 282 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟) ↔ 𝑝 ≤ (𝑞 ∨ 𝑟))) |
16 | 5, 15 | rabeqbidv 3396 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)} = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}) |
17 | 16 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)} ↔ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})) |
18 | 17 | anbi2d 632 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}) ↔ (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |
19 | 5, 18 | rexeqbidv 3314 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}) ↔ ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |
20 | 5, 19 | rexeqbidv 3314 |
. . . . 5
⊢ (𝑘 = 𝐾 → (∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}) ↔ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}))) |
21 | 20 | abbidv 2807 |
. . . 4
⊢ (𝑘 = 𝐾 → {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})} = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})}) |
22 | | df-lines 37252 |
. . . 4
⊢ Lines =
(𝑘 ∈ V ↦ {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})}) |
23 | 4 | fvexi 6731 |
. . . . 5
⊢ 𝐴 ∈ V |
24 | | df-sn 4542 |
. . . . . . 7
⊢ {{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}} = {𝑠 ∣ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}} |
25 | | snex 5324 |
. . . . . . 7
⊢ {{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}} ∈ V |
26 | 24, 25 | eqeltrri 2835 |
. . . . . 6
⊢ {𝑠 ∣ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}} ∈ V |
27 | | simpr 488 |
. . . . . . 7
⊢ ((𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}) → 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}) |
28 | 27 | ss2abi 3980 |
. . . . . 6
⊢ {𝑠 ∣ (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})} ⊆ {𝑠 ∣ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}} |
29 | 26, 28 | ssexi 5215 |
. . . . 5
⊢ {𝑠 ∣ (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})} ∈ V |
30 | 23, 23, 29 | ab2rexex2 7753 |
. . . 4
⊢ {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})} ∈ V |
31 | 21, 22, 30 | fvmpt 6818 |
. . 3
⊢ (𝐾 ∈ V →
(Lines‘𝐾) = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})}) |
32 | 2, 31 | syl5eq 2790 |
. 2
⊢ (𝐾 ∈ V → 𝑁 = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})}) |
33 | 1, 32 | syl 17 |
1
⊢ (𝐾 ∈ 𝐵 → 𝑁 = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})}) |