Theorem joinfval

Description: Value of join function for a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018) TODO: prove joinfval2 first to reduce net proof size (existence part)?

	Ref	Expression
Hypotheses	joinfval.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	joinfval.j	⊢ ∨ = ( join ‘ 𝐾 )
Assertion	joinfval	⊢ ( 𝐾 ∈ 𝑉 → ∨ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } )

Proof

Step	Hyp	Ref	Expression
1		joinfval.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
2		joinfval.j	⊢ ∨ = ( join ‘ 𝐾 )
3		elex	⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V )
4		fvex	⊢ ( Base ‘ 𝐾 ) ∈ V
5		moeq	⊢ ∃* 𝑧 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } )
6	5	a1i	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ∃* 𝑧 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) )
7		eqid	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) }
8	4 4 6 7	oprabex	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } ∈ V
9	8	a1i	⊢ ( 𝐾 ∈ V → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } ∈ V )
10	1	lubfun	⊢ Fun 𝑈
11		funbrfv2b	⊢ ( Fun 𝑈 → ( { 𝑥 , 𝑦 } 𝑈 𝑧 ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) ) )
12	10 11	ax-mp	⊢ ( { 𝑥 , 𝑦 } 𝑈 𝑧 ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) )
13		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
15		simpl	⊢ ( ( 𝐾 ∈ V ∧ { 𝑥 , 𝑦 } ∈ dom 𝑈 ) → 𝐾 ∈ V )
16		simpr	⊢ ( ( 𝐾 ∈ V ∧ { 𝑥 , 𝑦 } ∈ dom 𝑈 ) → { 𝑥 , 𝑦 } ∈ dom 𝑈 )
17	13 14 1 15 16	lubelss	⊢ ( ( 𝐾 ∈ V ∧ { 𝑥 , 𝑦 } ∈ dom 𝑈 ) → { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝐾 ) )
18	17	ex	⊢ ( 𝐾 ∈ V → ( { 𝑥 , 𝑦 } ∈ dom 𝑈 → { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝐾 ) ) )
19		vex	⊢ 𝑥 ∈ V
20		vex	⊢ 𝑦 ∈ V
21	19 20	prss	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ↔ { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝐾 ) )
22	18 21	syl6ibr	⊢ ( 𝐾 ∈ V → ( { 𝑥 , 𝑦 } ∈ dom 𝑈 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) )
23		eqcom	⊢ ( ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ↔ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) )
24	23	biimpi	⊢ ( ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = 𝑧 → 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) )
25	22 24	anim12d1	⊢ ( 𝐾 ∈ V → ( ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ) )
26	12 25	syl5bi	⊢ ( 𝐾 ∈ V → ( { 𝑥 , 𝑦 } 𝑈 𝑧 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ) )
27	26	alrimiv	⊢ ( 𝐾 ∈ V → ∀ 𝑧 ( { 𝑥 , 𝑦 } 𝑈 𝑧 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ) )
28	27	alrimiv	⊢ ( 𝐾 ∈ V → ∀ 𝑦 ∀ 𝑧 ( { 𝑥 , 𝑦 } 𝑈 𝑧 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ) )
29	28	alrimiv	⊢ ( 𝐾 ∈ V → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( { 𝑥 , 𝑦 } 𝑈 𝑧 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ) )
30		ssoprab2	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( { 𝑥 , 𝑦 } 𝑈 𝑧 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } )
31	29 30	syl	⊢ ( 𝐾 ∈ V → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } )
32	9 31	ssexd	⊢ ( 𝐾 ∈ V → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } ∈ V )
33		fveq2	⊢ ( 𝑝 = 𝐾 → ( lub ‘ 𝑝 ) = ( lub ‘ 𝐾 ) )
34	33 1	eqtr4di	⊢ ( 𝑝 = 𝐾 → ( lub ‘ 𝑝 ) = 𝑈 )
35	34	breqd	⊢ ( 𝑝 = 𝐾 → ( { 𝑥 , 𝑦 } ( lub ‘ 𝑝 ) 𝑧 ↔ { 𝑥 , 𝑦 } 𝑈 𝑧 ) )
36	35	oprabbidv	⊢ ( 𝑝 = 𝐾 → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( lub ‘ 𝑝 ) 𝑧 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } )
37		df-join	⊢ join = ( 𝑝 ∈ V ↦ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( lub ‘ 𝑝 ) 𝑧 } )
38	36 37	fvmptg	⊢ ( ( 𝐾 ∈ V ∧ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } ∈ V ) → ( join ‘ 𝐾 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } )
39	32 38	mpdan	⊢ ( 𝐾 ∈ V → ( join ‘ 𝐾 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } )
40	2 39	syl5eq	⊢ ( 𝐾 ∈ V → ∨ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } )
41	3 40	syl	⊢ ( 𝐾 ∈ 𝑉 → ∨ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝑈 𝑧 } )