Metamath Proof Explorer

Theorem r1limwun

Description: Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion r1limwun ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ∈ WUni )

Proof

Step Hyp Ref Expression
1 r1tr ⊢ Tr ( 𝑅1 ‘ 𝐴 )
2 1 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → Tr ( 𝑅1 ‘ 𝐴 ) )
3 limelon ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → 𝐴 ∈ On )
4 r1fnon ⊢ 𝑅1 Fn On
5 fndm ⊢ ( 𝑅1 Fn On → dom 𝑅1 = On )
6 4 5 ax-mp ⊢ dom 𝑅1 = On
7 3 6 eleqtrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → 𝐴 ∈ dom 𝑅1 )
8 onssr1 ⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) )
9 7 8 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) )
10 0ellim ⊢ ( Lim 𝐴 → ∅ ∈ 𝐴 )
11 10 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ∅ ∈ 𝐴 )
12 9 11 sseldd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ∅ ∈ ( 𝑅1 ‘ 𝐴 ) )
13 12 ne0d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ≠ ∅ )
14 rankuni ⊢ ( rank ‘ ∪ 𝑥 ) = ∪ ( rank ‘ 𝑥 )
15 rankon ⊢ ( rank ‘ 𝑥 ) ∈ On
16 eloni ⊢ ( ( rank ‘ 𝑥 ) ∈ On → Ord ( rank ‘ 𝑥 ) )
17 orduniss ⊢ ( Ord ( rank ‘ 𝑥 ) → ∪ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑥 ) )
18 15 16 17 mp2b ⊢ ∪ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑥 )
19 18 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ∪ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑥 ) )
20 rankr1ai ⊢ ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) → ( rank ‘ 𝑥 ) ∈ 𝐴 )
21 20 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( rank ‘ 𝑥 ) ∈ 𝐴 )
22 onuni ⊢ ( ( rank ‘ 𝑥 ) ∈ On → ∪ ( rank ‘ 𝑥 ) ∈ On )
23 15 22 ax-mp ⊢ ∪ ( rank ‘ 𝑥 ) ∈ On
24 3 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → 𝐴 ∈ On )
25 ontr2 ⊢ ( ( ∪ ( rank ‘ 𝑥 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( ∪ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑥 ) ∧ ( rank ‘ 𝑥 ) ∈ 𝐴 ) → ∪ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
26 23 24 25 sylancr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( ( ∪ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑥 ) ∧ ( rank ‘ 𝑥 ) ∈ 𝐴 ) → ∪ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
27 19 21 26 mp2and ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ∪ ( rank ‘ 𝑥 ) ∈ 𝐴 )
28 14 27 eqeltrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( rank ‘ ∪ 𝑥 ) ∈ 𝐴 )
29 r1elwf ⊢ ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
30 29 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
31 uniwf ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
32 30 31 sylib ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ∪ 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
33 7 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → 𝐴 ∈ dom 𝑅1 )
34 rankr1ag ⊢ ( ( ∪ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ dom 𝑅1 ) → ( ∪ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ ∪ 𝑥 ) ∈ 𝐴 ) )
35 32 33 34 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( ∪ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ ∪ 𝑥 ) ∈ 𝐴 ) )
36 28 35 mpbird ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ∪ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) )
37 r1pwcl ⊢ ( Lim 𝐴 → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
38 37 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
39 38 biimpa ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) )
40 29 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
41 r1elwf ⊢ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) → 𝑦 ∈ ∪ ( 𝑅1 “ On ) )
42 41 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → 𝑦 ∈ ∪ ( 𝑅1 “ On ) )
43 rankprb ⊢ ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { 𝑥 , 𝑦 } ) = suc ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) )
44 40 42 43 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( rank ‘ { 𝑥 , 𝑦 } ) = suc ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) )
45 limord ⊢ ( Lim 𝐴 → Ord 𝐴 )
46 45 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → Ord 𝐴 )
47 21 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( rank ‘ 𝑥 ) ∈ 𝐴 )
48 rankr1ai ⊢ ( 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) → ( rank ‘ 𝑦 ) ∈ 𝐴 )
49 48 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( rank ‘ 𝑦 ) ∈ 𝐴 )
50 ordunel ⊢ ( ( Ord 𝐴 ∧ ( rank ‘ 𝑥 ) ∈ 𝐴 ∧ ( rank ‘ 𝑦 ) ∈ 𝐴 ) → ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) ∈ 𝐴 )
51 46 47 49 50 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) ∈ 𝐴 )
52 limsuc ⊢ ( Lim 𝐴 → ( ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) ∈ 𝐴 ↔ suc ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) ∈ 𝐴 ) )
53 52 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) ∈ 𝐴 ↔ suc ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) ∈ 𝐴 ) )
54 51 53 mpbid ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → suc ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) ∈ 𝐴 )
55 44 54 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( rank ‘ { 𝑥 , 𝑦 } ) ∈ 𝐴 )
56 prwf ⊢ ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) → { 𝑥 , 𝑦 } ∈ ∪ ( 𝑅1 “ On ) )
57 40 42 56 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → { 𝑥 , 𝑦 } ∈ ∪ ( 𝑅1 “ On ) )
58 33 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → 𝐴 ∈ dom 𝑅1 )
59 rankr1ag ⊢ ( ( { 𝑥 , 𝑦 } ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ dom 𝑅1 ) → ( { 𝑥 , 𝑦 } ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ { 𝑥 , 𝑦 } ) ∈ 𝐴 ) )
60 57 58 59 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( { 𝑥 , 𝑦 } ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ { 𝑥 , 𝑦 } ) ∈ 𝐴 ) )
61 55 60 mpbird ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) ) → { 𝑥 , 𝑦 } ∈ ( 𝑅1 ‘ 𝐴 ) )
62 61 ralrimiva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ∀ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑅1 ‘ 𝐴 ) )
63 36 39 62 3jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) → ( ∪ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ∧ 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑅1 ‘ 𝐴 ) ) )
64 63 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ∀ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ( ∪ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ∧ 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑅1 ‘ 𝐴 ) ) )
65 fvex ⊢ ( 𝑅1 ‘ 𝐴 ) ∈ V
66 iswun ⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ V → ( ( 𝑅1 ‘ 𝐴 ) ∈ WUni ↔ ( Tr ( 𝑅1 ‘ 𝐴 ) ∧ ( 𝑅1 ‘ 𝐴 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ( ∪ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ∧ 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑅1 ‘ 𝐴 ) ) ) ) )
67 65 66 ax-mp ⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ WUni ↔ ( Tr ( 𝑅1 ‘ 𝐴 ) ∧ ( 𝑅1 ‘ 𝐴 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ( ∪ 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ∧ 𝒫 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑅1 ‘ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑅1 ‘ 𝐴 ) ) ) )
68 2 13 64 67 syl3anbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ∈ WUni )