Theorem onsupnub

Description: An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	onsupnub	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ On ∧ ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵 ) ) → ∪ 𝐴 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		simprr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ On ∧ ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵 ) ) → ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵 )
2		unissb	⊢ ( ∪ 𝐴 ⊆ 𝐵 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵 )
3	1 2	sylibr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐵 ∈ On ∧ ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵 ) ) → ∪ 𝐴 ⊆ 𝐵 )