Step |
Hyp |
Ref |
Expression |
1 |
|
dicvalrel.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
dicvalrel.i |
⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
relopabv |
⊢ Rel { 〈 𝑓 , 𝑠 〉 ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑋 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } |
4 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
5 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
6 |
4 5 1 2
|
dicdmN |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 } ) |
7 |
6
|
eleq2d |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ 𝑋 ∈ { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 } ) ) |
8 |
|
breq1 |
⊢ ( 𝑝 = 𝑋 → ( 𝑝 ( le ‘ 𝐾 ) 𝑊 ↔ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) |
9 |
8
|
notbid |
⊢ ( 𝑝 = 𝑋 → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ↔ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) |
10 |
9
|
elrab |
⊢ ( 𝑋 ∈ { 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∣ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 } ↔ ( 𝑋 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) |
11 |
7 10
|
bitrdi |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ ( 𝑋 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) ) |
12 |
11
|
biimpa |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝑋 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) |
13 |
|
eqid |
⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) |
14 |
|
eqid |
⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
15 |
|
eqid |
⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
16 |
4 5 1 13 14 15 2
|
dicval |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = { 〈 𝑓 , 𝑠 〉 ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑋 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) |
17 |
12 16
|
syldan |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑋 ) = { 〈 𝑓 , 𝑠 〉 ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑋 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) |
18 |
17
|
releqd |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel { 〈 𝑓 , 𝑠 〉 ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑋 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) ) |
19 |
3 18
|
mpbiri |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → Rel ( 𝐼 ‘ 𝑋 ) ) |
20 |
19
|
ex |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 → Rel ( 𝐼 ‘ 𝑋 ) ) ) |
21 |
|
rel0 |
⊢ Rel ∅ |
22 |
|
ndmfv |
⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑋 ) = ∅ ) |
23 |
22
|
releqd |
⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel ∅ ) ) |
24 |
21 23
|
mpbiri |
⊢ ( ¬ 𝑋 ∈ dom 𝐼 → Rel ( 𝐼 ‘ 𝑋 ) ) |
25 |
20 24
|
pm2.61d1 |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) ) |