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 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )

Proof

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