Theorem ordsucuniel

Description: Given an element A of the union of an ordinal B , suc A is an element of B itself. (Contributed by Scott Fenton, 28-Mar-2012) (Proof shortened by Mario Carneiro, 29-May-2015)

	Ref	Expression
Assertion	ordsucuniel	⊢ ( Ord 𝐵 → ( 𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		orduni	⊢ ( Ord 𝐵 → Ord ∪ 𝐵 )
2		ordelord	⊢ ( ( Ord ∪ 𝐵 ∧ 𝐴 ∈ ∪ 𝐵 ) → Ord 𝐴 )
3	2	ex	⊢ ( Ord ∪ 𝐵 → ( 𝐴 ∈ ∪ 𝐵 → Ord 𝐴 ) )
4	1 3	syl	⊢ ( Ord 𝐵 → ( 𝐴 ∈ ∪ 𝐵 → Ord 𝐴 ) )
5		ordelord	⊢ ( ( Ord 𝐵 ∧ suc 𝐴 ∈ 𝐵 ) → Ord suc 𝐴 )
6		ordsuc	⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )
7	5 6	sylibr	⊢ ( ( Ord 𝐵 ∧ suc 𝐴 ∈ 𝐵 ) → Ord 𝐴 )
8	7	ex	⊢ ( Ord 𝐵 → ( suc 𝐴 ∈ 𝐵 → Ord 𝐴 ) )
9		ordsson	⊢ ( Ord 𝐵 → 𝐵 ⊆ On )
10		ordunisssuc	⊢ ( ( 𝐵 ⊆ On ∧ Ord 𝐴 ) → ( ∪ 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ suc 𝐴 ) )
11	9 10	sylan	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( ∪ 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ suc 𝐴 ) )
12		ordtri1	⊢ ( ( Ord ∪ 𝐵 ∧ Ord 𝐴 ) → ( ∪ 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ∪ 𝐵 ) )
13	1 12	sylan	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( ∪ 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ∪ 𝐵 ) )
14		ordtri1	⊢ ( ( Ord 𝐵 ∧ Ord suc 𝐴 ) → ( 𝐵 ⊆ suc 𝐴 ↔ ¬ suc 𝐴 ∈ 𝐵 ) )
15	6 14	sylan2b	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ⊆ suc 𝐴 ↔ ¬ suc 𝐴 ∈ 𝐵 ) )
16	11 13 15	3bitr3d	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( ¬ 𝐴 ∈ ∪ 𝐵 ↔ ¬ suc 𝐴 ∈ 𝐵 ) )
17	16	con4bid	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵 ) )
18	17	ex	⊢ ( Ord 𝐵 → ( Ord 𝐴 → ( 𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵 ) ) )
19	4 8 18	pm5.21ndd	⊢ ( Ord 𝐵 → ( 𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵 ) )