Metamath Proof Explorer


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 A On
Assertion onuninsuci A = A ¬ x On A = suc x

Proof

Step Hyp Ref Expression
1 onssi.1 A On
2 1 onirri ¬ A A
3 id A = A A = A
4 df-suc suc x = x x
5 4 eqeq2i A = suc x A = x x
6 unieq A = x x A = x x
7 5 6 sylbi A = suc x A = x x
8 uniun x x = x x
9 unisnv x = x
10 9 uneq2i x x = x x
11 8 10 eqtri x x = x x
12 7 11 eqtrdi A = suc x A = x x
13 tron Tr On
14 eleq1 A = suc x A On suc x On
15 1 14 mpbii A = suc x suc x On
16 trsuc Tr On suc x On x On
17 13 15 16 sylancr A = suc x x On
18 ontr x On Tr x
19 df-tr Tr x x x
20 18 19 sylib x On x x
21 17 20 syl A = suc x x x
22 ssequn1 x x x x = x
23 21 22 sylib A = suc x x x = x
24 12 23 eqtrd A = suc x A = x
25 3 24 sylan9eqr A = suc x A = A A = x
26 vex x V
27 26 sucid x suc x
28 eleq2 A = suc x x A x suc x
29 27 28 mpbiri A = suc x x A
30 29 adantr A = suc x A = A x A
31 25 30 eqeltrd A = suc x A = A A A
32 2 31 mto ¬ A = suc x A = A
33 32 imnani A = suc x ¬ A = A
34 33 rexlimivw x On A = suc x ¬ A = A
35 onuni A On A On
36 1 35 ax-mp A On
37 onuniorsuc A On A = A A = suc A
38 1 37 ax-mp A = A A = suc A
39 38 ori ¬ A = A A = suc A
40 suceq x = A suc x = suc A
41 40 rspceeqv A On A = suc A x On A = suc x
42 36 39 41 sylancr ¬ A = A x On A = suc x
43 34 42 impbii x On A = suc x ¬ A = A
44 43 con2bii A = A ¬ x On A = suc x