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	eqtrid	⊢ ( ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ → ( 𝑋 ∨ 𝑌 ) = ∅ )
34	30 33	biimtrrdi	⊢ ( 𝜑 → ( ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 → ( 𝑋 ∨ 𝑌 ) = ∅ ) )
35	34	imp	⊢ ( ( 𝜑 ∧ ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( 𝑋 ∨ 𝑌 ) = ∅ )
36		ndmfv	⊢ ( ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 → ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ∅ )
37	36	adantl	⊢ ( ( 𝜑 ∧ ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ∅ )
38	35 37	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ { 𝑋 , 𝑌 } ∈ dom 𝑈 ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) )
39	28 38	pm2.61dan	⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) )