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 |
1 2 3 4 5
|
cmtfvalN |
⊢ ( 𝐾 ∈ 𝐴 → 𝐶 = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ) |
7 |
|
df-3an |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) ) |
8 |
7
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } |
9 |
6 8
|
eqtrdi |
⊢ ( 𝐾 ∈ 𝐴 → 𝐶 = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ) |
10 |
9
|
breqd |
⊢ ( 𝐾 ∈ 𝐴 → ( 𝑋 𝐶 𝑌 ↔ 𝑋 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } 𝑌 ) ) |
11 |
10
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑋 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } 𝑌 ) ) |
12 |
|
df-br |
⊢ ( 𝑋 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } 𝑌 ↔ 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ) |
13 |
|
id |
⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 ) |
14 |
|
oveq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∧ 𝑦 ) = ( 𝑋 ∧ 𝑦 ) ) |
15 |
|
oveq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) = ( 𝑋 ∧ ( ⊥ ‘ 𝑦 ) ) ) |
16 |
14 15
|
oveq12d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) = ( ( 𝑋 ∧ 𝑦 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) |
17 |
13 16
|
eqeq12d |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ↔ 𝑋 = ( ( 𝑋 ∧ 𝑦 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) ) |
18 |
|
oveq2 |
⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∧ 𝑦 ) = ( 𝑋 ∧ 𝑌 ) ) |
19 |
|
fveq2 |
⊢ ( 𝑦 = 𝑌 → ( ⊥ ‘ 𝑦 ) = ( ⊥ ‘ 𝑌 ) ) |
20 |
19
|
oveq2d |
⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∧ ( ⊥ ‘ 𝑦 ) ) = ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) |
21 |
18 20
|
oveq12d |
⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ∧ 𝑦 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑦 ) ) ) = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) |
22 |
21
|
eqeq2d |
⊢ ( 𝑦 = 𝑌 → ( 𝑋 = ( ( 𝑋 ∧ 𝑦 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑦 ) ) ) ↔ 𝑋 = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) ) |
23 |
17 22
|
opelopab2 |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } ↔ 𝑋 = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) ) |
24 |
12 23
|
syl5bb |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } 𝑌 ↔ 𝑋 = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) ) |
25 |
24
|
3adant1 |
⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } 𝑌 ↔ 𝑋 = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) ) |
26 |
11 25
|
bitrd |
⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑋 = ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ ( ⊥ ‘ 𝑌 ) ) ) ) ) |