Metamath Proof Explorer

Theorem orduninsuc

Description: An ordinal class is equal to its union if and only if it is not the successor of an ordinal. Closed-form generalization of onuninsuci . (Contributed by NM, 18-Feb-2004)

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

Proof

Step Hyp Ref Expression
1 ordeleqon ⊢Ord⁡A↔A∈On∨A=On
2 id ⊢A=ifA∈OnA∅→A=ifA∈OnA∅
3 unieq ⊢A=ifA∈OnA∅→⋃A=⋃ifA∈OnA∅
4 2 3 eqeq12d ⊢A=ifA∈OnA∅→A=⋃A↔ifA∈OnA∅=⋃ifA∈OnA∅
5 eqeq1 ⊢A=ifA∈OnA∅→A=suc⁡x↔ifA∈OnA∅=suc⁡x
6 5 rexbidv ⊢A=ifA∈OnA∅→∃x∈OnA=suc⁡x↔∃x∈OnifA∈OnA∅=suc⁡x
7 6 notbid ⊢A=ifA∈OnA∅→¬∃x∈OnA=suc⁡x↔¬∃x∈OnifA∈OnA∅=suc⁡x
8 4 7 bibi12d ⊢A=ifA∈OnA∅→A=⋃A↔¬∃x∈OnA=suc⁡x↔ifA∈OnA∅=⋃ifA∈OnA∅↔¬∃x∈OnifA∈OnA∅=suc⁡x
9 0elon ⊢∅∈On
10 9 elimel ⊢ifA∈OnA∅∈On
11 10 onuninsuci ⊢ifA∈OnA∅=⋃ifA∈OnA∅↔¬∃x∈OnifA∈OnA∅=suc⁡x
12 8 11 dedth ⊢A∈On→A=⋃A↔¬∃x∈OnA=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∈OnOn=suc⁡x
23 14 22 2th ⊢On=⋃On↔¬∃x∈OnOn=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∈OnA=suc⁡x↔∃x∈OnOn=suc⁡x
29 28 notbid ⊢A=On→¬∃x∈OnA=suc⁡x↔¬∃x∈OnOn=suc⁡x
30 26 29 bibi12d ⊢A=On→A=⋃A↔¬∃x∈OnA=suc⁡x↔On=⋃On↔¬∃x∈OnOn=suc⁡x
31 23 30 mpbiri ⊢A=On→A=⋃A↔¬∃x∈OnA=suc⁡x
32 12 31 jaoi ⊢A∈On∨A=On→A=⋃A↔¬∃x∈OnA=suc⁡x
33 1 32 sylbi ⊢Ord⁡A→A=⋃A↔¬∃x∈OnA=suc⁡x