Step |
Hyp |
Ref |
Expression |
1 |
|
cmtfval.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
cmtfval.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
cmtfval.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
4 |
|
cmtfval.o |
⊢ ⊥ = ( oc ‘ 𝐾 ) |
5 |
|
cmtfval.c |
⊢ 𝐶 = ( cm ‘ 𝐾 ) |
6 |
|
elex |
⊢ ( 𝐾 ∈ 𝐴 → 𝐾 ∈ V ) |
7 |
|
fveq2 |
⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝐾 ) ) |
8 |
7 1
|
eqtr4di |
⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = 𝐵 ) |
9 |
8
|
eleq2d |
⊢ ( 𝑝 = 𝐾 → ( 𝑥 ∈ ( Base ‘ 𝑝 ) ↔ 𝑥 ∈ 𝐵 ) ) |
10 |
8
|
eleq2d |
⊢ ( 𝑝 = 𝐾 → ( 𝑦 ∈ ( Base ‘ 𝑝 ) ↔ 𝑦 ∈ 𝐵 ) ) |
11 |
|
fveq2 |
⊢ ( 𝑝 = 𝐾 → ( join ‘ 𝑝 ) = ( join ‘ 𝐾 ) ) |
12 |
11 2
|
eqtr4di |
⊢ ( 𝑝 = 𝐾 → ( join ‘ 𝑝 ) = ∨ ) |
13 |
|
fveq2 |
⊢ ( 𝑝 = 𝐾 → ( meet ‘ 𝑝 ) = ( meet ‘ 𝐾 ) ) |
14 |
13 3
|
eqtr4di |
⊢ ( 𝑝 = 𝐾 → ( meet ‘ 𝑝 ) = ∧ ) |
15 |
14
|
oveqd |
⊢ ( 𝑝 = 𝐾 → ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) = ( 𝑥 ∧ 𝑦 ) ) |
16 |
|
eqidd |
⊢ ( 𝑝 = 𝐾 → 𝑥 = 𝑥 ) |
17 |
|
fveq2 |
⊢ ( 𝑝 = 𝐾 → ( oc ‘ 𝑝 ) = ( oc ‘ 𝐾 ) ) |
18 |
17 4
|
eqtr4di |
⊢ ( 𝑝 = 𝐾 → ( oc ‘ 𝑝 ) = ⊥ ) |
19 |
18
|
fveq1d |
⊢ ( 𝑝 = 𝐾 → ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) = ( ⊥ ‘ 𝑦 ) ) |
20 |
14 16 19
|
oveq123d |
⊢ ( 𝑝 = 𝐾 → ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) = ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) |
21 |
12 15 20
|
oveq123d |
⊢ ( 𝑝 = 𝐾 → ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) |
22 |
21
|
eqeq2d |
⊢ ( 𝑝 = 𝐾 → ( 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ↔ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) ) |
23 |
9 10 22
|
3anbi123d |
⊢ ( 𝑝 = 𝐾 → ( ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) ) ) |
24 |
23
|
opabbidv |
⊢ ( 𝑝 = 𝐾 → { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ) |
25 |
|
df-cmtN |
⊢ cm = ( 𝑝 ∈ V ↦ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) } ) |
26 |
|
df-3an |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) ) |
27 |
26
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } |
28 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
29 |
28 28
|
xpex |
⊢ ( 𝐵 × 𝐵 ) ∈ V |
30 |
|
opabssxp |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ⊆ ( 𝐵 × 𝐵 ) |
31 |
29 30
|
ssexi |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ∈ V |
32 |
27 31
|
eqeltri |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ∈ V |
33 |
24 25 32
|
fvmpt |
⊢ ( 𝐾 ∈ V → ( cm ‘ 𝐾 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ) |
34 |
5 33
|
syl5eq |
⊢ ( 𝐾 ∈ V → 𝐶 = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ) |
35 |
6 34
|
syl |
⊢ ( 𝐾 ∈ 𝐴 → 𝐶 = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ) |