Theorem onuninsuci

Description: An ordinal is equal to its union if and only if it is not the successor of an ordinal. A closed-form generalization of this result is orduninsuc . (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		unisnv	⊢ ∪ { 𝑥 } = 𝑥
10	9	uneq2i	⊢ ( ∪ 𝑥 ∪ ∪ { 𝑥 } ) = ( ∪ 𝑥 ∪ 𝑥 )
11	8 10	eqtri	⊢ ∪ ( 𝑥 ∪ { 𝑥 } ) = ( ∪ 𝑥 ∪ 𝑥 )
12	7 11	eqtrdi	⊢ ( 𝐴 = suc 𝑥 → ∪ 𝐴 = ( ∪ 𝑥 ∪ 𝑥 ) )
13		tron	⊢ Tr On
14		eleq1	⊢ ( 𝐴 = suc 𝑥 → ( 𝐴 ∈ On ↔ suc 𝑥 ∈ On ) )
15	1 14	mpbii	⊢ ( 𝐴 = suc 𝑥 → suc 𝑥 ∈ On )
16		trsuc	⊢ ( ( Tr On ∧ suc 𝑥 ∈ On ) → 𝑥 ∈ On )
17	13 15 16	sylancr	⊢ ( 𝐴 = suc 𝑥 → 𝑥 ∈ On )
18		ontr	⊢ ( 𝑥 ∈ On → Tr 𝑥 )
19		df-tr	⊢ ( Tr 𝑥 ↔ ∪ 𝑥 ⊆ 𝑥 )
20	18 19	sylib	⊢ ( 𝑥 ∈ On → ∪ 𝑥 ⊆ 𝑥 )
21	17 20	syl	⊢ ( 𝐴 = suc 𝑥 → ∪ 𝑥 ⊆ 𝑥 )
22		ssequn1	⊢ ( ∪ 𝑥 ⊆ 𝑥 ↔ ( ∪ 𝑥 ∪ 𝑥 ) = 𝑥 )
23	21 22	sylib	⊢ ( 𝐴 = suc 𝑥 → ( ∪ 𝑥 ∪ 𝑥 ) = 𝑥 )
24	12 23	eqtrd	⊢ ( 𝐴 = suc 𝑥 → ∪ 𝐴 = 𝑥 )
25	3 24	sylan9eqr	⊢ ( ( 𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴 ) → 𝐴 = 𝑥 )
26		vex	⊢ 𝑥 ∈ V
27	26	sucid	⊢ 𝑥 ∈ suc 𝑥
28		eleq2	⊢ ( 𝐴 = suc 𝑥 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ suc 𝑥 ) )
29	27 28	mpbiri	⊢ ( 𝐴 = suc 𝑥 → 𝑥 ∈ 𝐴 )
30	29	adantr	⊢ ( ( 𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴 ) → 𝑥 ∈ 𝐴 )
31	25 30	eqeltrd	⊢ ( ( 𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴 ) → 𝐴 ∈ 𝐴 )
32	2 31	mto	⊢ ¬ ( 𝐴 = suc 𝑥 ∧ 𝐴 = ∪ 𝐴 )
33	32	imnani	⊢ ( 𝐴 = suc 𝑥 → ¬ 𝐴 = ∪ 𝐴 )
34	33	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ¬ 𝐴 = ∪ 𝐴 )
35		onuni	⊢ ( 𝐴 ∈ On → ∪ 𝐴 ∈ On )
36	1 35	ax-mp	⊢ ∪ 𝐴 ∈ On
37		onuniorsuc	⊢ ( 𝐴 ∈ On → ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 ) )
38	1 37	ax-mp	⊢ ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 )
39	38	ori	⊢ ( ¬ 𝐴 = ∪ 𝐴 → 𝐴 = suc ∪ 𝐴 )
40		suceq	⊢ ( 𝑥 = ∪ 𝐴 → suc 𝑥 = suc ∪ 𝐴 )
41	40	rspceeqv	⊢ ( ( ∪ 𝐴 ∈ On ∧ 𝐴 = suc ∪ 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )
42	36 39 41	sylancr	⊢ ( ¬ 𝐴 = ∪ 𝐴 → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )
43	34 42	impbii	⊢ ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ↔ ¬ 𝐴 = ∪ 𝐴 )
44	43	con2bii	⊢ ( 𝐴 = ∪ 𝐴 ↔ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )