This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ 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 𝑥 )