Step |
Hyp |
Ref |
Expression |
1 |
|
joinfval.u |
⊢ 𝑈 = ( lub ‘ 𝐾 ) |
2 |
|
joinfval.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
1 2
|
joinfval2 |
⊢ ( 𝐾 ∈ 𝑉 → ∨ = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } ) |
4 |
3
|
dmeqd |
⊢ ( 𝐾 ∈ 𝑉 → dom ∨ = dom { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } ) |
5 |
|
dmoprab |
⊢ dom { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } |
6 |
|
fvex |
⊢ ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ∈ V |
7 |
6
|
isseti |
⊢ ∃ 𝑧 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) |
8 |
|
19.42v |
⊢ ( ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ ∃ 𝑧 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ) |
9 |
7 8
|
mpbiran2 |
⊢ ( ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ↔ { 𝑥 , 𝑦 } ∈ dom 𝑈 ) |
10 |
9
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 } |
11 |
5 10
|
eqtri |
⊢ dom { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 } |
12 |
4 11
|
eqtrdi |
⊢ ( 𝐾 ∈ 𝑉 → dom ∨ = { 〈 𝑥 , 𝑦 〉 ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 } ) |