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