Step |
Hyp |
Ref |
Expression |
1 |
|
ltrnset.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
ltrnset.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
ltrnset.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
4 |
|
ltrnset.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
5 |
|
ltrnset.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
6 |
|
ltrnset.d |
⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) |
7 |
|
ltrnset.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
8 |
1 2 3 4 5 6 7
|
ltrnset |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → 𝑇 = { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } ) |
9 |
8
|
eleq2d |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ 𝐹 ∈ { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } ) ) |
10 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ) |
11 |
10
|
oveq2d |
⊢ ( 𝑓 = 𝐹 → ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) = ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ) |
12 |
11
|
oveq1d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) ) |
13 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑞 ) ) |
14 |
13
|
oveq2d |
⊢ ( 𝑓 = 𝐹 → ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) = ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ) |
15 |
14
|
oveq1d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) |
16 |
12 15
|
eqeq12d |
⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ↔ ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) |
17 |
16
|
imbi2d |
⊢ ( 𝑓 = 𝐹 → ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) |
18 |
17
|
2ralbidv |
⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) |
19 |
18
|
elrab |
⊢ ( 𝐹 ∈ { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) |
20 |
9 19
|
bitrdi |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) ) |