Theorem safesnsupfiub

Description: If B is a finite subset of ordered class A , we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024)

	Ref	Expression
Hypotheses	safesnsupfiub.small	⊢ ( 𝜑 → ( 𝑂 = ∅ ∨ 𝑂 = 1o ) )
	safesnsupfiub.finite	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	safesnsupfiub.subset	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
	safesnsupfiub.ordered	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
	safesnsupfiub.ub	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑥 𝑅 𝑦 )
Assertion	safesnsupfiub	⊢ ( 𝜑 → ∀ 𝑥 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ∀ 𝑦 ∈ 𝐶 𝑥 𝑅 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		safesnsupfiub.small	⊢ ( 𝜑 → ( 𝑂 = ∅ ∨ 𝑂 = 1o ) )
2		safesnsupfiub.finite	⊢ ( 𝜑 → 𝐵 ∈ Fin )
3		safesnsupfiub.subset	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
4		safesnsupfiub.ordered	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
5		safesnsupfiub.ub	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑥 𝑅 𝑦 )
6	1 2 3 4	safesnsupfiss	⊢ ( 𝜑 → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ⊆ 𝐵 )
7	6	sseld	⊢ ( 𝜑 → ( 𝑥 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) → 𝑥 ∈ 𝐵 ) )
8	7	imim1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 → ∀ 𝑦 ∈ 𝐶 𝑥 𝑅 𝑦 ) → ( 𝑥 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) → ∀ 𝑦 ∈ 𝐶 𝑥 𝑅 𝑦 ) ) )
9	8	ralimdv2	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑥 𝑅 𝑦 → ∀ 𝑥 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ∀ 𝑦 ∈ 𝐶 𝑥 𝑅 𝑦 ) )
10	5 9	mpd	⊢ ( 𝜑 → ∀ 𝑥 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ∀ 𝑦 ∈ 𝐶 𝑥 𝑅 𝑦 )