Metamath Proof Explorer

Theorem r1wunlim

Description: The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion r1wunlim ( 𝐴 ∈ 𝑉 → ( ( 𝑅1 ‘ 𝐴 ) ∈ WUni ↔ Lim 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → ( 𝑅1 ‘ 𝐴 ) ∈ WUni )
2 1 wun0 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → ∅ ∈ ( 𝑅1 ‘ 𝐴 ) )
3 elfvdm ⊢ ( ∅ ∈ ( 𝑅1 ‘ 𝐴 ) → 𝐴 ∈ dom 𝑅1 )
4 2 3 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → 𝐴 ∈ dom 𝑅1 )
5 r1fnon ⊢ 𝑅1 Fn On
6 5 fndmi ⊢ dom 𝑅1 = On
7 4 6 eleqtrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → 𝐴 ∈ On )
8 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
9 7 8 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → Ord 𝐴 )
10 n0i ⊢ ( ∅ ∈ ( 𝑅1 ‘ 𝐴 ) → ¬ ( 𝑅1 ‘ 𝐴 ) = ∅ )
11 2 10 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → ¬ ( 𝑅1 ‘ 𝐴 ) = ∅ )
12 fveq2 ⊢ ( 𝐴 = ∅ → ( 𝑅1 ‘ 𝐴 ) = ( 𝑅1 ‘ ∅ ) )
13 r10 ⊢ ( 𝑅1 ‘ ∅ ) = ∅
14 12 13 eqtrdi ⊢ ( 𝐴 = ∅ → ( 𝑅1 ‘ 𝐴 ) = ∅ )
15 11 14 nsyl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → ¬ 𝐴 = ∅ )
16 suceloni ⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
17 7 16 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → suc 𝐴 ∈ On )
18 sucidg ⊢ ( 𝐴 ∈ On → 𝐴 ∈ suc 𝐴 )
19 7 18 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → 𝐴 ∈ suc 𝐴 )
20 r1ord ⊢ ( suc 𝐴 ∈ On → ( 𝐴 ∈ suc 𝐴 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) ) )
21 17 19 20 sylc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) )
22 r1elwf ⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) )
23 wfelirr ⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) → ¬ ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐴 ) )
24 21 22 23 3syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → ¬ ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐴 ) )
25 simprr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → 𝐴 = suc 𝑥 )
26 25 fveq2d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → ( 𝑅1 ‘ 𝐴 ) = ( 𝑅1 ‘ suc 𝑥 ) )
27 r1suc ⊢ ( 𝑥 ∈ On → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
28 27 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
29 26 28 eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → ( 𝑅1 ‘ 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
30 simplr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → ( 𝑅1 ‘ 𝐴 ) ∈ WUni )
31 7 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → 𝐴 ∈ On )
32 sucidg ⊢ ( 𝑥 ∈ On → 𝑥 ∈ suc 𝑥 )
33 32 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → 𝑥 ∈ suc 𝑥 )
34 33 25 eleqtrrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → 𝑥 ∈ 𝐴 )
35 r1ord ⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ∈ ( 𝑅1 ‘ 𝐴 ) ) )
36 31 34 35 sylc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → ( 𝑅1 ‘ 𝑥 ) ∈ ( 𝑅1 ‘ 𝐴 ) )
37 30 36 wunpw ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → 𝒫 ( 𝑅1 ‘ 𝑥 ) ∈ ( 𝑅1 ‘ 𝐴 ) )
38 29 37 eqeltrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) ∧ ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) ) → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐴 ) )
39 38 rexlimdvaa ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐴 ) ) )
40 24 39 mtod ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )
41 ioran ⊢ ( ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ↔ ( ¬ 𝐴 = ∅ ∧ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )
42 15 40 41 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )
43 dflim3 ⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
44 9 42 43 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ WUni ) → Lim 𝐴 )
45 r1limwun ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ∈ WUni )
46 44 45 impbida ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑅1 ‘ 𝐴 ) ∈ WUni ↔ Lim 𝐴 ) )