Step |
Hyp |
Ref |
Expression |
1 |
|
meetdef.u |
⊢ 𝐺 = ( glb ‘ 𝐾 ) |
2 |
|
meetdef.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
3 |
|
meetdef.k |
⊢ ( 𝜑 → 𝐾 ∈ 𝑉 ) |
4 |
|
meetdef.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑊 ) |
5 |
|
meetdef.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝑍 ) |
6 |
1 2
|
meetdm |
⊢ ( 𝐾 ∈ 𝑉 → dom ∧ = { 〈 𝑥 , 𝑦 〉 ∣ { 𝑥 , 𝑦 } ∈ dom 𝐺 } ) |
7 |
6
|
eleq2d |
⊢ ( 𝐾 ∈ 𝑉 → ( 〈 𝑋 , 𝑌 〉 ∈ dom ∧ ↔ 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ { 𝑥 , 𝑦 } ∈ dom 𝐺 } ) ) |
8 |
3 7
|
syl |
⊢ ( 𝜑 → ( 〈 𝑋 , 𝑌 〉 ∈ dom ∧ ↔ 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ { 𝑥 , 𝑦 } ∈ dom 𝐺 } ) ) |
9 |
|
preq1 |
⊢ ( 𝑥 = 𝑋 → { 𝑥 , 𝑦 } = { 𝑋 , 𝑦 } ) |
10 |
9
|
eleq1d |
⊢ ( 𝑥 = 𝑋 → ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ↔ { 𝑋 , 𝑦 } ∈ dom 𝐺 ) ) |
11 |
|
preq2 |
⊢ ( 𝑦 = 𝑌 → { 𝑋 , 𝑦 } = { 𝑋 , 𝑌 } ) |
12 |
11
|
eleq1d |
⊢ ( 𝑦 = 𝑌 → ( { 𝑋 , 𝑦 } ∈ dom 𝐺 ↔ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) ) |
13 |
10 12
|
opelopabg |
⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑍 ) → ( 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ { 𝑥 , 𝑦 } ∈ dom 𝐺 } ↔ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) ) |
14 |
4 5 13
|
syl2anc |
⊢ ( 𝜑 → ( 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ { 𝑥 , 𝑦 } ∈ dom 𝐺 } ↔ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) ) |
15 |
8 14
|
bitrd |
⊢ ( 𝜑 → ( 〈 𝑋 , 𝑌 〉 ∈ dom ∧ ↔ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) ) |