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

Metamath Proof Explorer

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 𝑥 ) )