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	⊢ ( 𝜑 → 𝑈 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) )

Metamath Proof Explorer

Theorem lubfval

Proof