Metamath Proof Explorer


Theorem lubfval

Description: Value of the least upper bound function of a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 6-Sep-2018)

Ref Expression
Hypotheses lubfval.b 𝐵 = ( Base ‘ 𝐾 )
lubfval.l = ( le ‘ 𝐾 )
lubfval.u 𝑈 = ( lub ‘ 𝐾 )
lubfval.p ( 𝜓 ↔ ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) )
lubfval.k ( 𝜑𝐾𝑉 )
Assertion lubfval ( 𝜑𝑈 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥𝐵 𝜓 } ) )

Proof

Step Hyp Ref Expression
1 lubfval.b 𝐵 = ( Base ‘ 𝐾 )
2 lubfval.l = ( le ‘ 𝐾 )
3 lubfval.u 𝑈 = ( lub ‘ 𝐾 )
4 lubfval.p ( 𝜓 ↔ ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) )
5 lubfval.k ( 𝜑𝐾𝑉 )
6 elex ( 𝐾𝑉𝐾 ∈ V )
7 fveq2 ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝐾 ) )
8 7 1 eqtr4di ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = 𝐵 )
9 8 pweqd ( 𝑝 = 𝐾 → 𝒫 ( Base ‘ 𝑝 ) = 𝒫 𝐵 )
10 fveq2 ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ( le ‘ 𝐾 ) )
11 10 2 eqtr4di ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = )
12 11 breqd ( 𝑝 = 𝐾 → ( 𝑦 ( le ‘ 𝑝 ) 𝑥𝑦 𝑥 ) )
13 12 ralbidv ( 𝑝 = 𝐾 → ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ↔ ∀ 𝑦𝑠 𝑦 𝑥 ) )
14 11 breqd ( 𝑝 = 𝐾 → ( 𝑦 ( le ‘ 𝑝 ) 𝑧𝑦 𝑧 ) )
15 14 ralbidv ( 𝑝 = 𝐾 → ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 ↔ ∀ 𝑦𝑠 𝑦 𝑧 ) )
16 11 breqd ( 𝑝 = 𝐾 → ( 𝑥 ( le ‘ 𝑝 ) 𝑧𝑥 𝑧 ) )
17 15 16 imbi12d ( 𝑝 = 𝐾 → ( ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ↔ ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) )
18 8 17 raleqbidv ( 𝑝 = 𝐾 → ( ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ↔ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) )
19 13 18 anbi12d ( 𝑝 = 𝐾 → ( ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ↔ ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) )
20 8 19 riotaeqbidv ( 𝑝 = 𝐾 → ( 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) = ( 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) )
21 9 20 mpteq12dv ( 𝑝 = 𝐾 → ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) ) )
22 19 reubidv ( 𝑝 = 𝐾 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ↔ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) )
23 reueq1 ( ( Base ‘ 𝑝 ) = 𝐵 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ↔ ∃! 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) )
24 8 23 syl ( 𝑝 = 𝐾 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ↔ ∃! 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) )
25 22 24 bitrd ( 𝑝 = 𝐾 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ↔ ∃! 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) )
26 25 abbidv ( 𝑝 = 𝐾 → { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } = { 𝑠 ∣ ∃! 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) } )
27 21 26 reseq12d ( 𝑝 = 𝐾 → ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) } ) )
28 df-lub lub = ( 𝑝 ∈ V ↦ ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } ) )
29 1 fvexi 𝐵 ∈ V
30 29 pwex 𝒫 𝐵 ∈ V
31 30 mptex ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) ) ∈ V
32 31 resex ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) } ) ∈ V
33 27 28 32 fvmpt ( 𝐾 ∈ V → ( lub ‘ 𝐾 ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) } ) )
34 4 a1i ( 𝑥𝐵 → ( 𝜓 ↔ ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) )
35 34 riotabiia ( 𝑥𝐵 𝜓 ) = ( 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) )
36 35 mpteq2i ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 𝜓 ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) )
37 4 reubii ( ∃! 𝑥𝐵 𝜓 ↔ ∃! 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) )
38 37 abbii { 𝑠 ∣ ∃! 𝑥𝐵 𝜓 } = { 𝑠 ∣ ∃! 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) }
39 36 38 reseq12i ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥𝐵 𝜓 } ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥𝐵 ( ∀ 𝑦𝑠 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑠 𝑦 𝑧𝑥 𝑧 ) ) } )
40 33 3 39 3eqtr4g ( 𝐾 ∈ V → 𝑈 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥𝐵 𝜓 } ) )
41 5 6 40 3syl ( 𝜑𝑈 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝑥𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥𝐵 𝜓 } ) )