Metamath Proof Explorer


Theorem joinval

Description: Join value. Since both sides evaluate to (/) when they don't exist, for convenience we drop the { X , Y } e. dom U requirement. (Contributed by NM, 9-Sep-2018)

Ref Expression
Hypotheses joindef.u 𝑈 = ( lub ‘ 𝐾 )
joindef.j = ( join ‘ 𝐾 )
joindef.k ( 𝜑𝐾𝑉 )
joindef.x ( 𝜑𝑋𝑊 )
joindef.y ( 𝜑𝑌𝑍 )
Assertion joinval ( 𝜑 → ( 𝑋 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) )

Proof

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 ( 𝜑 → ( 𝑋 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) )