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 )