Theorem sorpssun

Description: A chain of sets is closed under binary union. (Contributed by Mario Carneiro, 16-May-2015)

	Ref	Expression
Assertion	sorpssun	⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ∪ 𝐶 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simprr	⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → 𝐶 ∈ 𝐴 )
2		ssequn1	⊢ ( 𝐵 ⊆ 𝐶 ↔ ( 𝐵 ∪ 𝐶 ) = 𝐶 )
3		eleq1	⊢ ( ( 𝐵 ∪ 𝐶 ) = 𝐶 → ( ( 𝐵 ∪ 𝐶 ) ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
4	2 3	sylbi	⊢ ( 𝐵 ⊆ 𝐶 → ( ( 𝐵 ∪ 𝐶 ) ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
5	1 4	syl5ibrcom	⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ⊆ 𝐶 → ( 𝐵 ∪ 𝐶 ) ∈ 𝐴 ) )
6		simprl	⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → 𝐵 ∈ 𝐴 )
7		ssequn2	⊢ ( 𝐶 ⊆ 𝐵 ↔ ( 𝐵 ∪ 𝐶 ) = 𝐵 )
8		eleq1	⊢ ( ( 𝐵 ∪ 𝐶 ) = 𝐵 → ( ( 𝐵 ∪ 𝐶 ) ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
9	7 8	sylbi	⊢ ( 𝐶 ⊆ 𝐵 → ( ( 𝐵 ∪ 𝐶 ) ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
10	6 9	syl5ibrcom	⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐶 ⊆ 𝐵 → ( 𝐵 ∪ 𝐶 ) ∈ 𝐴 ) )
11		sorpssi	⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) )
12	5 10 11	mpjaod	⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ∪ 𝐶 ) ∈ 𝐴 )