Theorem meetfval

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

	Ref	Expression
Hypotheses	meetfval.u	⊢ 𝐺 = ( glb ‘ 𝐾 )
	meetfval.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	meetfval	⊢ ( 𝐾 ∈ 𝑉 → ∧ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } )

Proof

Step	Hyp	Ref	Expression
1		meetfval.u	⊢ 𝐺 = ( glb ‘ 𝐾 )
2		meetfval.m	⊢ ∧ = ( meet ‘ 𝐾 )
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	glbfun	⊢ 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	glbelss	⊢ ( ( 𝐾 ∈ 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	⊢ ( 𝑝 = 𝐾 → ( glb ‘ 𝑝 ) = ( glb ‘ 𝐾 ) )
34	33 1	eqtr4di	⊢ ( 𝑝 = 𝐾 → ( glb ‘ 𝑝 ) = 𝐺 )
35	34	breqd	⊢ ( 𝑝 = 𝐾 → ( { 𝑥 , 𝑦 } ( glb ‘ 𝑝 ) 𝑧 ↔ { 𝑥 , 𝑦 } 𝐺 𝑧 ) )
36	35	oprabbidv	⊢ ( 𝑝 = 𝐾 → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( glb ‘ 𝑝 ) 𝑧 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } )
37		df-meet	⊢ meet = ( 𝑝 ∈ V ↦ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( glb ‘ 𝑝 ) 𝑧 } )
38	36 37	fvmptg	⊢ ( ( 𝐾 ∈ V ∧ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } ∈ V ) → ( meet ‘ 𝐾 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } )
39	32 38	mpdan	⊢ ( 𝐾 ∈ V → ( meet ‘ 𝐾 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } )
40	2 39	eqtrid	⊢ ( 𝐾 ∈ V → ∧ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } )
41	3 40	syl	⊢ ( 𝐾 ∈ 𝑉 → ∧ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } )