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