Metamath Proof Explorer

Theorem wuncval2

Description: Our earlier expression for a containing weak universe is in fact the weak universe closure. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses wuncval2.f ⊢F=rec⁡z∈V⟼z∪⋃z∪⋃x∈z𝒫x⋃x∪ran⁡y∈z⟼xyA∪1𝑜↾ω
wuncval2.u ⊢U=⋃ran⁡F
Assertion wuncval2 ⊢A∈V→wUniCl⁡A=U

Proof

Step Hyp Ref Expression
1 wuncval2.f ⊢F=rec⁡z∈V⟼z∪⋃z∪⋃x∈z𝒫x⋃x∪ran⁡y∈z⟼xyA∪1𝑜↾ω
2 wuncval2.u ⊢U=⋃ran⁡F
3 1 2 wunex2 ⊢A∈V→U∈WUni∧A⊆U
4 wuncss ⊢U∈WUni∧A⊆U→wUniCl⁡A⊆U
5 3 4 syl ⊢A∈V→wUniCl⁡A⊆U
6 frfnom ⊢rec⁡z∈V⟼z∪⋃z∪⋃x∈z𝒫x⋃x∪ran⁡y∈z⟼xyA∪1𝑜↾ωFnω
7 1 fneq1i ⊢FFnω↔rec⁡z∈V⟼z∪⋃z∪⋃x∈z𝒫x⋃x∪ran⁡y∈z⟼xyA∪1𝑜↾ωFnω
8 6 7 mpbir ⊢FFnω
9 fniunfv ⊢FFnω→⋃m∈ωF⁡m=⋃ran⁡F
10 8 9 ax-mp ⊢⋃m∈ωF⁡m=⋃ran⁡F
11 2 10 eqtr4i ⊢U=⋃m∈ωF⁡m
12 fveq2 ⊢m=∅→F⁡m=F⁡∅
13 12 sseq1d ⊢m=∅→F⁡m⊆wUniCl⁡A↔F⁡∅⊆wUniCl⁡A
14 fveq2 ⊢m=n→F⁡m=F⁡n
15 14 sseq1d ⊢m=n→F⁡m⊆wUniCl⁡A↔F⁡n⊆wUniCl⁡A
16 fveq2 ⊢m=suc⁡n→F⁡m=F⁡suc⁡n
17 16 sseq1d ⊢m=suc⁡n→F⁡m⊆wUniCl⁡A↔F⁡suc⁡n⊆wUniCl⁡A
18 1on ⊢1𝑜∈On
19 unexg ⊢A∈V∧1𝑜∈On→A∪1𝑜∈V
20 18 19 mpan2 ⊢A∈V→A∪1𝑜∈V
21 1 fveq1i ⊢F⁡∅=rec⁡z∈V⟼z∪⋃z∪⋃x∈z𝒫x⋃x∪ran⁡y∈z⟼xyA∪1𝑜↾ω⁡∅
22 fr0g ⊢A∪1𝑜∈V→rec⁡z∈V⟼z∪⋃z∪⋃x∈z𝒫x⋃x∪ran⁡y∈z⟼xyA∪1𝑜↾ω⁡∅=A∪1𝑜
23 21 22 eqtrid ⊢A∪1𝑜∈V→F⁡∅=A∪1𝑜
24 20 23 syl ⊢A∈V→F⁡∅=A∪1𝑜
25 wuncid ⊢A∈V→A⊆wUniCl⁡A
26 df1o2 ⊢1𝑜=∅
27 wunccl ⊢A∈V→wUniCl⁡A∈WUni
28 27 wun0 ⊢A∈V→∅∈wUniCl⁡A
29 28 snssd ⊢A∈V→∅⊆wUniCl⁡A
30 26 29 eqsstrid ⊢A∈V→1𝑜⊆wUniCl⁡A
31 25 30 unssd ⊢A∈V→A∪1𝑜⊆wUniCl⁡A
32 24 31 eqsstrd ⊢A∈V→F⁡∅⊆wUniCl⁡A
33 simplr ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A→n∈ω
34 fvex ⊢F⁡n∈V
35 34 uniex ⊢⋃F⁡n∈V
36 34 35 unex ⊢F⁡n∪⋃F⁡n∈V
37 prex ⊢𝒫u⋃u∈V
38 34 mptex ⊢v∈F⁡n⟼uv∈V
39 38 rnex ⊢ran⁡v∈F⁡n⟼uv∈V
40 37 39 unex ⊢𝒫u⋃u∪ran⁡v∈F⁡n⟼uv∈V
41 34 40 iunex ⊢⋃u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv∈V
42 36 41 unex ⊢F⁡n∪⋃F⁡n∪⋃u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv∈V
43 id ⊢w=z→w=z
44 unieq ⊢w=z→⋃w=⋃z
45 43 44 uneq12d ⊢w=z→w∪⋃w=z∪⋃z
46 pweq ⊢u=x→𝒫u=𝒫x
47 unieq ⊢u=x→⋃u=⋃x
48 46 47 preq12d ⊢u=x→𝒫u⋃u=𝒫x⋃x
49 preq1 ⊢u=x→uv=xv
50 49 mpteq2dv ⊢u=x→v∈w⟼uv=v∈w⟼xv
51 50 rneqd ⊢u=x→ran⁡v∈w⟼uv=ran⁡v∈w⟼xv
52 48 51 uneq12d ⊢u=x→𝒫u⋃u∪ran⁡v∈w⟼uv=𝒫x⋃x∪ran⁡v∈w⟼xv
53 52 cbviunv ⊢⋃u∈w𝒫u⋃u∪ran⁡v∈w⟼uv=⋃x∈w𝒫x⋃x∪ran⁡v∈w⟼xv
54 preq2 ⊢v=y→xv=xy
55 54 cbvmptv ⊢v∈w⟼xv=y∈w⟼xy
56 mpteq1 ⊢w=z→y∈w⟼xy=y∈z⟼xy
57 55 56 eqtrid ⊢w=z→v∈w⟼xv=y∈z⟼xy
58 57 rneqd ⊢w=z→ran⁡v∈w⟼xv=ran⁡y∈z⟼xy
59 58 uneq2d ⊢w=z→𝒫x⋃x∪ran⁡v∈w⟼xv=𝒫x⋃x∪ran⁡y∈z⟼xy
60 43 59 iuneq12d ⊢w=z→⋃x∈w𝒫x⋃x∪ran⁡v∈w⟼xv=⋃x∈z𝒫x⋃x∪ran⁡y∈z⟼xy
61 53 60 eqtrid ⊢w=z→⋃u∈w𝒫u⋃u∪ran⁡v∈w⟼uv=⋃x∈z𝒫x⋃x∪ran⁡y∈z⟼xy
62 45 61 uneq12d ⊢w=z→w∪⋃w∪⋃u∈w𝒫u⋃u∪ran⁡v∈w⟼uv=z∪⋃z∪⋃x∈z𝒫x⋃x∪ran⁡y∈z⟼xy
63 id ⊢w=F⁡n→w=F⁡n
64 unieq ⊢w=F⁡n→⋃w=⋃F⁡n
65 63 64 uneq12d ⊢w=F⁡n→w∪⋃w=F⁡n∪⋃F⁡n
66 mpteq1 ⊢w=F⁡n→v∈w⟼uv=v∈F⁡n⟼uv
67 66 rneqd ⊢w=F⁡n→ran⁡v∈w⟼uv=ran⁡v∈F⁡n⟼uv
68 67 uneq2d ⊢w=F⁡n→𝒫u⋃u∪ran⁡v∈w⟼uv=𝒫u⋃u∪ran⁡v∈F⁡n⟼uv
69 63 68 iuneq12d ⊢w=F⁡n→⋃u∈w𝒫u⋃u∪ran⁡v∈w⟼uv=⋃u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv
70 65 69 uneq12d ⊢w=F⁡n→w∪⋃w∪⋃u∈w𝒫u⋃u∪ran⁡v∈w⟼uv=F⁡n∪⋃F⁡n∪⋃u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv
71 1 62 70 frsucmpt2 ⊢n∈ω∧F⁡n∪⋃F⁡n∪⋃u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv∈V→F⁡suc⁡n=F⁡n∪⋃F⁡n∪⋃u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv
72 33 42 71 sylancl ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A→F⁡suc⁡n=F⁡n∪⋃F⁡n∪⋃u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv
73 simpr ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A→F⁡n⊆wUniCl⁡A
74 27 ad3antrrr ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n→wUniCl⁡A∈WUni
75 73 sselda ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n→u∈wUniCl⁡A
76 74 75 wunelss ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n→u⊆wUniCl⁡A
77 76 ralrimiva ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A→∀u∈F⁡nu⊆wUniCl⁡A
78 unissb ⊢⋃F⁡n⊆wUniCl⁡A↔∀u∈F⁡nu⊆wUniCl⁡A
79 77 78 sylibr ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A→⋃F⁡n⊆wUniCl⁡A
80 73 79 unssd ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A→F⁡n∪⋃F⁡n⊆wUniCl⁡A
81 74 75 wunpw ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n→𝒫u∈wUniCl⁡A
82 74 75 wununi ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n→⋃u∈wUniCl⁡A
83 81 82 prssd ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n→𝒫u⋃u⊆wUniCl⁡A
84 74 adantr ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n∧v∈F⁡n→wUniCl⁡A∈WUni
85 75 adantr ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n∧v∈F⁡n→u∈wUniCl⁡A
86 simplr ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n→F⁡n⊆wUniCl⁡A
87 86 sselda ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n∧v∈F⁡n→v∈wUniCl⁡A
88 84 85 87 wunpr ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n∧v∈F⁡n→uv∈wUniCl⁡A
89 88 fmpttd ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n→v∈F⁡n⟼uv:F⁡n⟶wUniCl⁡A
90 89 frnd ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n→ran⁡v∈F⁡n⟼uv⊆wUniCl⁡A
91 83 90 unssd ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A∧u∈F⁡n→𝒫u⋃u∪ran⁡v∈F⁡n⟼uv⊆wUniCl⁡A
92 91 ralrimiva ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A→∀u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv⊆wUniCl⁡A
93 iunss ⊢⋃u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv⊆wUniCl⁡A↔∀u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv⊆wUniCl⁡A
94 92 93 sylibr ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A→⋃u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv⊆wUniCl⁡A
95 80 94 unssd ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A→F⁡n∪⋃F⁡n∪⋃u∈F⁡n𝒫u⋃u∪ran⁡v∈F⁡n⟼uv⊆wUniCl⁡A
96 72 95 eqsstrd ⊢A∈V∧n∈ω∧F⁡n⊆wUniCl⁡A→F⁡suc⁡n⊆wUniCl⁡A
97 96 ex ⊢A∈V∧n∈ω→F⁡n⊆wUniCl⁡A→F⁡suc⁡n⊆wUniCl⁡A
98 97 expcom ⊢n∈ω→A∈V→F⁡n⊆wUniCl⁡A→F⁡suc⁡n⊆wUniCl⁡A
99 13 15 17 32 98 finds2 ⊢m∈ω→A∈V→F⁡m⊆wUniCl⁡A
100 99 com12 ⊢A∈V→m∈ω→F⁡m⊆wUniCl⁡A
101 100 ralrimiv ⊢A∈V→∀m∈ωF⁡m⊆wUniCl⁡A
102 iunss ⊢⋃m∈ωF⁡m⊆wUniCl⁡A↔∀m∈ωF⁡m⊆wUniCl⁡A
103 101 102 sylibr ⊢A∈V→⋃m∈ωF⁡m⊆wUniCl⁡A
104 11 103 eqsstrid ⊢A∈V→U⊆wUniCl⁡A
105 5 104 eqssd ⊢A∈V→wUniCl⁡A=U