Metamath Proof Explorer


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 syl5eq ( 𝐾 ∈ V → = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } )
41 3 40 syl ( 𝐾𝑉 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } )