Step |
Hyp |
Ref |
Expression |
1 |
|
joindef.u |
⊢ 𝑈 = ( lub ‘ 𝐾 ) |
2 |
|
joindef.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
joindef.k |
⊢ ( 𝜑 → 𝐾 ∈ 𝑉 ) |
4 |
|
joindef.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑊 ) |
5 |
|
joindef.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝑍 ) |
6 |
1 2
|
joinfval2 |
⊢ ( 𝐾 ∈ 𝑉 → ∨ = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } ) |
7 |
3 6
|
syl |
⊢ ( 𝜑 → ∨ = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } ) |
8 |
7
|
oveqd |
⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( 𝑋 { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) ) |
9 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑋 { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) ) |
10 |
|
simpr |
⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → { 𝑋 , 𝑌 } ∈ dom 𝑈 ) |
11 |
|
eqidd |
⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) |
12 |
|
fvexd |
⊢ ( 𝜑 → ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ∈ V ) |
13 |
|
preq12 |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { 𝑥 , 𝑦 } = { 𝑋 , 𝑌 } ) |
14 |
13
|
eleq1d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ↔ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) ) |
15 |
14
|
3adant3 |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) → ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ↔ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) ) |
16 |
|
simp3 |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) → 𝑧 = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) |
17 |
13
|
fveq2d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) |
18 |
17
|
3adant3 |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) |
19 |
16 18
|
eqeq12d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ↔ ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) ) |
20 |
15 19
|
anbi12d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) → ( ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ↔ ( { 𝑋 , 𝑌 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) ) ) |
21 |
|
moeq |
⊢ ∃* 𝑧 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) |
22 |
21
|
moani |
⊢ ∃* 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) |
23 |
|
eqid |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } |
24 |
20 22 23
|
ovigg |
⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑍 ∧ ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ∈ V ) → ( ( { 𝑋 , 𝑌 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑋 { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) ) |
25 |
4 5 12 24
|
syl3anc |
⊢ ( 𝜑 → ( ( { 𝑋 , 𝑌 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑋 { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) ) |
26 |
25
|
adantr |
⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( ( { 𝑋 , 𝑌 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑋 { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) ) |
27 |
10 11 26
|
mp2and |
⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( 𝑋 { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) |
28 |
9 27
|
eqtrd |
⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) |
29 |
1 2 3 4 5
|
joindef |
⊢ ( 𝜑 → ( 〈 𝑋 , 𝑌 〉 ∈ dom ∨ ↔ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) ) |
30 |
29
|
notbid |
⊢ ( 𝜑 → ( ¬ 〈 𝑋 , 𝑌 〉 ∈ dom ∨ ↔ ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) ) |
31 |
|
df-ov |
⊢ ( 𝑋 ∨ 𝑌 ) = ( ∨ ‘ 〈 𝑋 , 𝑌 〉 ) |
32 |
|
ndmfv |
⊢ ( ¬ 〈 𝑋 , 𝑌 〉 ∈ dom ∨ → ( ∨ ‘ 〈 𝑋 , 𝑌 〉 ) = ∅ ) |
33 |
31 32
|
syl5eq |
⊢ ( ¬ 〈 𝑋 , 𝑌 〉 ∈ dom ∨ → ( 𝑋 ∨ 𝑌 ) = ∅ ) |
34 |
30 33
|
syl6bir |
⊢ ( 𝜑 → ( ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 → ( 𝑋 ∨ 𝑌 ) = ∅ ) ) |
35 |
34
|
imp |
⊢ ( ( 𝜑 ∧ ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( 𝑋 ∨ 𝑌 ) = ∅ ) |
36 |
|
ndmfv |
⊢ ( ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 → ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ∅ ) |
37 |
36
|
adantl |
⊢ ( ( 𝜑 ∧ ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ∅ ) |
38 |
35 37
|
eqtr4d |
⊢ ( ( 𝜑 ∧ ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) |
39 |
28 38
|
pm2.61dan |
⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) ) |