Step |
Hyp |
Ref |
Expression |
1 |
|
dicval.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
dicval.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
3 |
|
dicval.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
4 |
|
dicval.p |
⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
dicval.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
|
dicval.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
7 |
|
dicval.i |
⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) |
8 |
|
dicval2.g |
⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) |
9 |
1 2 3 4 5 6 7 8
|
dicval2 |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = { 〈 𝑓 , 𝑠 〉 ∣ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) } ) |
10 |
9
|
eleq2d |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ↔ 𝑌 ∈ { 〈 𝑓 , 𝑠 〉 ∣ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) } ) ) |
11 |
|
excom |
⊢ ( ∃ 𝑓 ∃ 𝑠 ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ∃ 𝑠 ∃ 𝑓 ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) |
12 |
|
an12 |
⊢ ( ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ 𝑠 ∈ 𝐸 ) ) ) |
13 |
12
|
exbii |
⊢ ( ∃ 𝑓 ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ∃ 𝑓 ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ 𝑠 ∈ 𝐸 ) ) ) |
14 |
|
fvex |
⊢ ( 𝑠 ‘ 𝐺 ) ∈ V |
15 |
|
opeq1 |
⊢ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) → 〈 𝑓 , 𝑠 〉 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ) |
16 |
15
|
eqeq2d |
⊢ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) → ( 𝑌 = 〈 𝑓 , 𝑠 〉 ↔ 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ) ) |
17 |
16
|
anbi1d |
⊢ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) → ( ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ 𝑠 ∈ 𝐸 ) ↔ ( 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ∧ 𝑠 ∈ 𝐸 ) ) ) |
18 |
14 17
|
ceqsexv |
⊢ ( ∃ 𝑓 ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ 𝑠 ∈ 𝐸 ) ) ↔ ( 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ∧ 𝑠 ∈ 𝐸 ) ) |
19 |
|
ancom |
⊢ ( ( 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ∧ 𝑠 ∈ 𝐸 ) ↔ ( 𝑠 ∈ 𝐸 ∧ 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ) ) |
20 |
13 18 19
|
3bitri |
⊢ ( ∃ 𝑓 ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ( 𝑠 ∈ 𝐸 ∧ 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ) ) |
21 |
20
|
exbii |
⊢ ( ∃ 𝑠 ∃ 𝑓 ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝐸 ∧ 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ) ) |
22 |
11 21
|
bitri |
⊢ ( ∃ 𝑓 ∃ 𝑠 ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝐸 ∧ 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ) ) |
23 |
|
elopab |
⊢ ( 𝑌 ∈ { 〈 𝑓 , 𝑠 〉 ∣ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) } ↔ ∃ 𝑓 ∃ 𝑠 ( 𝑌 = 〈 𝑓 , 𝑠 〉 ∧ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) ) ) |
24 |
|
df-rex |
⊢ ( ∃ 𝑠 ∈ 𝐸 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝐸 ∧ 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ) ) |
25 |
22 23 24
|
3bitr4i |
⊢ ( 𝑌 ∈ { 〈 𝑓 , 𝑠 〉 ∣ ( 𝑓 = ( 𝑠 ‘ 𝐺 ) ∧ 𝑠 ∈ 𝐸 ) } ↔ ∃ 𝑠 ∈ 𝐸 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ) |
26 |
10 25
|
syl6bb |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ↔ ∃ 𝑠 ∈ 𝐸 𝑌 = 〈 ( 𝑠 ‘ 𝐺 ) , 𝑠 〉 ) ) |