Metamath Proof Explorer

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 ⁡ B → A ∈ ⋃ B ↔ suc ⁡ A ∈ B

Proof

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