Metamath Proof Explorer

Theorem orduninsuc

Description: An ordinal equal to its union is not a successor. (Contributed by NM, 18-Feb-2004)

Ref Expression
Assertion orduninsuc ⊢ Ord ⁡ A → A = ⋃ A ↔ ¬ ∃ x ∈ On A = suc ⁡ x

Proof

Step Hyp Ref Expression
1 ordeleqon ⊢ Ord ⁡ A ↔ A ∈ On ∨ A = On
2 id ⊢ A = if A ∈ On A ∅ → A = if A ∈ On A ∅
3 unieq ⊢ A = if A ∈ On A ∅ → ⋃ A = ⋃ if A ∈ On A ∅
4 2 3 eqeq12d ⊢ A = if A ∈ On A ∅ → A = ⋃ A ↔ if A ∈ On A ∅ = ⋃ if A ∈ On A ∅
5 eqeq1 ⊢ A = if A ∈ On A ∅ → A = suc ⁡ x ↔ if A ∈ On A ∅ = suc ⁡ x
6 5 rexbidv ⊢ A = if A ∈ On A ∅ → ∃ x ∈ On A = suc ⁡ x ↔ ∃ x ∈ On if A ∈ On A ∅ = suc ⁡ x
7 6 notbid ⊢ A = if A ∈ On A ∅ → ¬ ∃ x ∈ On A = suc ⁡ x ↔ ¬ ∃ x ∈ On if A ∈ On A ∅ = suc ⁡ x
8 4 7 bibi12d ⊢ A = if A ∈ On A ∅ → A = ⋃ A ↔ ¬ ∃ x ∈ On A = suc ⁡ x ↔ if A ∈ On A ∅ = ⋃ if A ∈ On A ∅ ↔ ¬ ∃ x ∈ On if A ∈ On A ∅ = suc ⁡ x
9 0elon ⊢ ∅ ∈ On
10 9 elimel ⊢ if A ∈ On A ∅ ∈ On
11 10 onuninsuci ⊢ if A ∈ On A ∅ = ⋃ if A ∈ On A ∅ ↔ ¬ ∃ x ∈ On if A ∈ On A ∅ = suc ⁡ x
12 8 11 dedth ⊢ A ∈ On → A = ⋃ A ↔ ¬ ∃ x ∈ On A = suc ⁡ x
13 unon ⊢ ⋃ On = On
14 13 eqcomi ⊢ On = ⋃ On
15 onprc ⊢ ¬ On ∈ V
16 vex ⊢ x ∈ V
17 16 sucex ⊢ suc ⁡ x ∈ V
18 eleq1 ⊢ On = suc ⁡ x → On ∈ V ↔ suc ⁡ x ∈ V
19 17 18 mpbiri ⊢ On = suc ⁡ x → On ∈ V
20 15 19 mto ⊢ ¬ On = suc ⁡ x
21 20 a1i ⊢ x ∈ On → ¬ On = suc ⁡ x
22 21 nrex ⊢ ¬ ∃ x ∈ On On = suc ⁡ x
23 14 22 2th ⊢ On = ⋃ On ↔ ¬ ∃ x ∈ On On = suc ⁡ x
24 id ⊢ A = On → A = On
25 unieq ⊢ A = On → ⋃ A = ⋃ On
26 24 25 eqeq12d ⊢ A = On → A = ⋃ A ↔ On = ⋃ On
27 eqeq1 ⊢ A = On → A = suc ⁡ x ↔ On = suc ⁡ x
28 27 rexbidv ⊢ A = On → ∃ x ∈ On A = suc ⁡ x ↔ ∃ x ∈ On On = suc ⁡ x
29 28 notbid ⊢ A = On → ¬ ∃ x ∈ On A = suc ⁡ x ↔ ¬ ∃ x ∈ On On = suc ⁡ x
30 26 29 bibi12d ⊢ A = On → A = ⋃ A ↔ ¬ ∃ x ∈ On A = suc ⁡ x ↔ On = ⋃ On ↔ ¬ ∃ x ∈ On On = suc ⁡ x
31 23 30 mpbiri ⊢ A = On → A = ⋃ A ↔ ¬ ∃ x ∈ On A = suc ⁡ x
32 12 31 jaoi ⊢ A ∈ On ∨ A = On → A = ⋃ A ↔ ¬ ∃ x ∈ On A = suc ⁡ x
33 1 32 sylbi ⊢ Ord ⁡ A → A = ⋃ A ↔ ¬ ∃ x ∈ On A = suc ⁡ x