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

Metamath Proof Explorer

Theorem ordunisuc2

Description: An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005)

Ref Expression
Assertion ordunisuc2 ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 orduninsuc ⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )
2 ralnex ⊢ ( ∀ 𝑥 ∈ On ¬ 𝐴 = suc 𝑥 ↔ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )
3 onsuc ⊢ ( 𝑥 ∈ On → suc 𝑥 ∈ On )
4 eloni ⊢ ( suc 𝑥 ∈ On → Ord suc 𝑥 )
5 3 4 syl ⊢ ( 𝑥 ∈ On → Ord suc 𝑥 )
6 ordtri3 ⊢ ( ( Ord 𝐴 ∧ Ord suc 𝑥 ) → ( 𝐴 = suc 𝑥 ↔ ¬ ( 𝐴 ∈ suc 𝑥 ∨ suc 𝑥 ∈ 𝐴 ) ) )
7 5 6 sylan2 ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( 𝐴 = suc 𝑥 ↔ ¬ ( 𝐴 ∈ suc 𝑥 ∨ suc 𝑥 ∈ 𝐴 ) ) )
8 7 con2bid ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( ( 𝐴 ∈ suc 𝑥 ∨ suc 𝑥 ∈ 𝐴 ) ↔ ¬ 𝐴 = suc 𝑥 ) )
9 onnbtwn ⊢ ( 𝑥 ∈ On → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ suc 𝑥 ) )
10 imnan ⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝐴 ∈ suc 𝑥 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ suc 𝑥 ) )
11 9 10 sylibr ⊢ ( 𝑥 ∈ On → ( 𝑥 ∈ 𝐴 → ¬ 𝐴 ∈ suc 𝑥 ) )
12 11 con2d ⊢ ( 𝑥 ∈ On → ( 𝐴 ∈ suc 𝑥 → ¬ 𝑥 ∈ 𝐴 ) )
13 pm2.21 ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) )
14 12 13 syl6 ⊢ ( 𝑥 ∈ On → ( 𝐴 ∈ suc 𝑥 → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
15 14 adantl ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( 𝐴 ∈ suc 𝑥 → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
16 ax-1 ⊢ ( suc 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) )
17 16 a1i ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( suc 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
18 15 17 jaod ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( ( 𝐴 ∈ suc 𝑥 ∨ suc 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
19 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
20 ordtri2or ⊢ ( ( Ord 𝑥 ∧ Ord 𝐴 ) → ( 𝑥 ∈ 𝐴 ∨ 𝐴 ⊆ 𝑥 ) )
21 19 20 sylan ⊢ ( ( 𝑥 ∈ On ∧ Ord 𝐴 ) → ( 𝑥 ∈ 𝐴 ∨ 𝐴 ⊆ 𝑥 ) )
22 21 ancoms ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( 𝑥 ∈ 𝐴 ∨ 𝐴 ⊆ 𝑥 ) )
23 22 orcomd ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( 𝐴 ⊆ 𝑥 ∨ 𝑥 ∈ 𝐴 ) )
24 23 adantr ⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) ∧ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ( 𝐴 ⊆ 𝑥 ∨ 𝑥 ∈ 𝐴 ) )
25 ordsssuc2 ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ∈ suc 𝑥 ) )
26 25 biimpd ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( 𝐴 ⊆ 𝑥 → 𝐴 ∈ suc 𝑥 ) )
27 26 adantr ⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) ∧ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ( 𝐴 ⊆ 𝑥 → 𝐴 ∈ suc 𝑥 ) )
28 simpr ⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) ∧ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) )
29 27 28 orim12d ⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) ∧ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ( ( 𝐴 ⊆ 𝑥 ∨ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∈ suc 𝑥 ∨ suc 𝑥 ∈ 𝐴 ) ) )
30 24 29 mpd ⊢ ( ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) ∧ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ( 𝐴 ∈ suc 𝑥 ∨ suc 𝑥 ∈ 𝐴 ) )
31 30 ex ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ( 𝐴 ∈ suc 𝑥 ∨ suc 𝑥 ∈ 𝐴 ) ) )
32 18 31 impbid ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( ( 𝐴 ∈ suc 𝑥 ∨ suc 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
33 8 32 bitr3d ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ On ) → ( ¬ 𝐴 = suc 𝑥 ↔ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
34 33 pm5.74da ⊢ ( Ord 𝐴 → ( ( 𝑥 ∈ On → ¬ 𝐴 = suc 𝑥 ) ↔ ( 𝑥 ∈ On → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ) )
35 impexp ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑥 ∈ 𝐴 ) → suc 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ On → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
36 simpr ⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
37 ordelon ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
38 37 ex ⊢ ( Ord 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ On ) )
39 38 ancrd ⊢ ( Ord 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ On ∧ 𝑥 ∈ 𝐴 ) ) )
40 36 39 impbid2 ⊢ ( Ord 𝐴 → ( ( 𝑥 ∈ On ∧ 𝑥 ∈ 𝐴 ) ↔ 𝑥 ∈ 𝐴 ) )
41 40 imbi1d ⊢ ( Ord 𝐴 → ( ( ( 𝑥 ∈ On ∧ 𝑥 ∈ 𝐴 ) → suc 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
42 35 41 bitr3id ⊢ ( Ord 𝐴 → ( ( 𝑥 ∈ On → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
43 34 42 bitrd ⊢ ( Ord 𝐴 → ( ( 𝑥 ∈ On → ¬ 𝐴 = suc 𝑥 ) ↔ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
44 43 ralbidv2 ⊢ ( Ord 𝐴 → ( ∀ 𝑥 ∈ On ¬ 𝐴 = suc 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) )
45 2 44 bitr3id ⊢ ( Ord 𝐴 → ( ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) )
46 1 45 bitrd ⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) )