Theorem onuninsuci

Description: A limit ordinal is not a successor ordinal. (Contributed by NM, 18-Feb-2004)

	Ref	Expression
Hypothesis	onssi.1	⊢ 𝐴 ∈ On
Assertion	onuninsuci	⊢ ( 𝐴 = ∪ 𝐴 ↔ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		onssi.1	⊢ 𝐴 ∈ On
2	1	onirri	⊢ ¬ 𝐴 ∈ 𝐴
3		id	⊢ ( 𝐴 = ∪ 𝐴 → 𝐴 = ∪ 𝐴 )
4		df-suc	⊢ suc 𝑥 = ( 𝑥 ∪ { 𝑥 } )
5	4	eqeq2i	⊢ ( 𝐴 = suc 𝑥 ↔ 𝐴 = ( 𝑥 ∪ { 𝑥 } ) )
6		unieq	⊢ ( 𝐴 = ( 𝑥 ∪ { 𝑥 } ) → ∪ 𝐴 = ∪ ( 𝑥 ∪ { 𝑥 } ) )
7	5 6	sylbi	⊢ ( 𝐴 = suc 𝑥 → ∪ 𝐴 = ∪ ( 𝑥 ∪ { 𝑥 } ) )
8		uniun	⊢ ∪ ( 𝑥 ∪ { 𝑥 } ) = ( ∪ 𝑥 ∪ ∪ { 𝑥 } )
9		vex	⊢ 𝑥 ∈ V
10	9	unisn	⊢ ∪ { 𝑥 } = 𝑥
11	10	uneq2i	⊢ ( ∪ 𝑥 ∪ ∪ { 𝑥 } ) = ( ∪ 𝑥 ∪ 𝑥 )
12	8 11	eqtri	⊢ ∪ ( 𝑥 ∪ { 𝑥 } ) = ( ∪ 𝑥 ∪ 𝑥 )
13	7 12	eqtrdi	⊢ ( 𝐴 = suc 𝑥 → ∪ 𝐴 = ( ∪ 𝑥 ∪ 𝑥 ) )
14		tron	⊢ Tr On
15		eleq1	⊢ ( 𝐴 = suc 𝑥 → ( 𝐴 ∈ On ↔ suc 𝑥 ∈ On ) )
16	1 15	mpbii	⊢ ( 𝐴 = suc 𝑥 → suc 𝑥 ∈ On )
17		trsuc	⊢ ( ( Tr On ∧ suc 𝑥 ∈ On ) → 𝑥 ∈ On )
18	14 16 17	sylancr	⊢ ( 𝐴 = suc 𝑥 → 𝑥 ∈ On )
19		eloni	⊢ ( 𝑥 ∈ On → Ord 𝑥 )
20		ordtr	⊢ ( Ord 𝑥 → Tr 𝑥 )
21	19 20	syl	⊢ ( 𝑥 ∈ On → Tr 𝑥 )
22		df-tr	⊢ ( Tr 𝑥 ↔ ∪ 𝑥 ⊆ 𝑥 )
23	21 22	sylib	⊢ ( 𝑥 ∈ On → ∪ 𝑥 ⊆ 𝑥 )
24	18 23	syl	⊢ ( 𝐴 = suc 𝑥 → ∪ 𝑥 ⊆ 𝑥 )
25		ssequn1	⊢ ( ∪ 𝑥 ⊆ 𝑥 ↔ ( ∪ 𝑥 ∪ 𝑥 ) = 𝑥 )
26	24 25	sylib	⊢ ( 𝐴 = suc 𝑥 → ( ∪ 𝑥 ∪ 𝑥 ) = 𝑥 )
27	13 26	eqtrd	⊢ ( 𝐴 = suc 𝑥 → ∪ 𝐴 = 𝑥 )
28	3 27	sylan9eqr	⊢ ( ( 𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴 ) → 𝐴 = 𝑥 )
29	9	sucid	⊢ 𝑥 ∈ suc 𝑥
30		eleq2	⊢ ( 𝐴 = suc 𝑥 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ suc 𝑥 ) )
31	29 30	mpbiri	⊢ ( 𝐴 = suc 𝑥 → 𝑥 ∈ 𝐴 )
32	31	adantr	⊢ ( ( 𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴 ) → 𝑥 ∈ 𝐴 )
33	28 32	eqeltrd	⊢ ( ( 𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴 ) → 𝐴 ∈ 𝐴 )
34	2 33	mto	⊢ ¬ ( 𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴 )
35	34	imnani	⊢ ( 𝐴 = suc 𝑥 → ¬ 𝐴 = ∪ 𝐴 )
36	35	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ 𝐴 = ∪ 𝐴 )
37		onuni	⊢ ( 𝐴 ∈ On → ∪ 𝐴 ∈ On )
38	1 37	ax-mp	⊢ ∪ 𝐴 ∈ On
39	1	onuniorsuci	⊢ ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 )
40	39	ori	⊢ ( ¬ 𝐴 = ∪ 𝐴 → 𝐴 = suc ∪ 𝐴 )
41		suceq	⊢ ( 𝑥 = ∪ 𝐴 → suc 𝑥 = suc ∪ 𝐴 )
42	41	rspceeqv	⊢ ( ( ∪ 𝐴 ∈ On ∧ 𝐴 = suc ∪ 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )
43	38 40 42	sylancr	⊢ ( ¬ 𝐴 = ∪ 𝐴 → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )
44	36 43	impbii	⊢ ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ↔ ¬ 𝐴 = ∪ 𝐴 )
45	44	con2bii	⊢ ( 𝐴 = ∪ 𝐴 ↔ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )