Theorem ordunisssuc

Description: A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003)

	Ref	Expression
Assertion	ordunisssuc	⊢ ( ( 𝐴 ⊆ On ∧ Ord 𝐵 ) → ( ∪ 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ssel2	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
2		ordsssuc	⊢ ( ( 𝑥 ∈ On ∧ Ord 𝐵 ) → ( 𝑥 ⊆ 𝐵 ↔ 𝑥 ∈ suc 𝐵 ) )
3	1 2	sylan	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ Ord 𝐵 ) → ( 𝑥 ⊆ 𝐵 ↔ 𝑥 ∈ suc 𝐵 ) )
4	3	an32s	⊢ ( ( ( 𝐴 ⊆ On ∧ Ord 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ⊆ 𝐵 ↔ 𝑥 ∈ suc 𝐵 ) )
5	4	ralbidva	⊢ ( ( 𝐴 ⊆ On ∧ Ord 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ suc 𝐵 ) )
6		unissb	⊢ ( ∪ 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 )
7		dfss3	⊢ ( 𝐴 ⊆ suc 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ suc 𝐵 )
8	5 6 7	3bitr4g	⊢ ( ( 𝐴 ⊆ On ∧ Ord 𝐵 ) → ( ∪ 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵 ) )