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 ⟼ x y A ∪ 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 ⟼ x y A ∪ 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 ⟼ x y A ∪ 1 𝑜 ↾ ω Fn ω
7 1 fneq1i ⊢ F Fn ω ↔ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω Fn ω
8 6 7 mpbir ⊢ F Fn ω
9 fniunfv ⊢ F Fn ω → ⋃ 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 ⟼ x y A ∪ 1 𝑜 ↾ ω ⁡ ∅
22 fr0g ⊢ A ∪ 1 𝑜 ∈ V → rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω ⁡ ∅ = A ∪ 1 𝑜
23 21 22 syl5eq ⊢ 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 ⟼ u v ∈ V
39 38 rnex ⊢ ran ⁡ v ∈ F ⁡ n ⟼ u v ∈ V
40 37 39 unex ⊢ 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v ∈ V
41 34 40 iunex ⊢ ⋃ u ∈ F ⁡ n 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v ∈ V
42 36 41 unex ⊢ F ⁡ n ∪ ⋃ F ⁡ n ∪ ⋃ u ∈ F ⁡ n 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v ∈ 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 → u v = x v
50 49 mpteq2dv ⊢ u = x → v ∈ w ⟼ u v = v ∈ w ⟼ x v
51 50 rneqd ⊢ u = x → ran ⁡ v ∈ w ⟼ u v = ran ⁡ v ∈ w ⟼ x v
52 48 51 uneq12d ⊢ u = x → 𝒫 u ⋃ u ∪ ran ⁡ v ∈ w ⟼ u v = 𝒫 x ⋃ x ∪ ran ⁡ v ∈ w ⟼ x v
53 52 cbviunv ⊢ ⋃ u ∈ w 𝒫 u ⋃ u ∪ ran ⁡ v ∈ w ⟼ u v = ⋃ x ∈ w 𝒫 x ⋃ x ∪ ran ⁡ v ∈ w ⟼ x v
54 preq2 ⊢ v = y → x v = x y
55 54 cbvmptv ⊢ v ∈ w ⟼ x v = y ∈ w ⟼ x y
56 mpteq1 ⊢ w = z → y ∈ w ⟼ x y = y ∈ z ⟼ x y
57 55 56 syl5eq ⊢ w = z → v ∈ w ⟼ x v = y ∈ z ⟼ x y
58 57 rneqd ⊢ w = z → ran ⁡ v ∈ w ⟼ x v = ran ⁡ y ∈ z ⟼ x y
59 58 uneq2d ⊢ w = z → 𝒫 x ⋃ x ∪ ran ⁡ v ∈ w ⟼ x v = 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y
60 43 59 iuneq12d ⊢ w = z → ⋃ x ∈ w 𝒫 x ⋃ x ∪ ran ⁡ v ∈ w ⟼ x v = ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y
61 53 60 syl5eq ⊢ w = z → ⋃ u ∈ w 𝒫 u ⋃ u ∪ ran ⁡ v ∈ w ⟼ u v = ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y
62 45 61 uneq12d ⊢ w = z → w ∪ ⋃ w ∪ ⋃ u ∈ w 𝒫 u ⋃ u ∪ ran ⁡ v ∈ w ⟼ u v = z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y
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 ⟼ u v = v ∈ F ⁡ n ⟼ u v
67 66 rneqd ⊢ w = F ⁡ n → ran ⁡ v ∈ w ⟼ u v = ran ⁡ v ∈ F ⁡ n ⟼ u v
68 67 uneq2d ⊢ w = F ⁡ n → 𝒫 u ⋃ u ∪ ran ⁡ v ∈ w ⟼ u v = 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v
69 63 68 iuneq12d ⊢ w = F ⁡ n → ⋃ u ∈ w 𝒫 u ⋃ u ∪ ran ⁡ v ∈ w ⟼ u v = ⋃ u ∈ F ⁡ n 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v
70 65 69 uneq12d ⊢ w = F ⁡ n → w ∪ ⋃ w ∪ ⋃ u ∈ w 𝒫 u ⋃ u ∪ ran ⁡ v ∈ w ⟼ u v = F ⁡ n ∪ ⋃ F ⁡ n ∪ ⋃ u ∈ F ⁡ n 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v
71 1 62 70 frsucmpt2 ⊢ n ∈ ω ∧ F ⁡ n ∪ ⋃ F ⁡ n ∪ ⋃ u ∈ F ⁡ n 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v ∈ V → F ⁡ suc ⁡ n = F ⁡ n ∪ ⋃ F ⁡ n ∪ ⋃ u ∈ F ⁡ n 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v
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 ⟼ u v
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 ⁡ n u ⊆ wUniCl ⁡ A
78 unissb ⊢ ⋃ F ⁡ n ⊆ wUniCl ⁡ A ↔ ∀ u ∈ F ⁡ n u ⊆ 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 → u v ∈ wUniCl ⁡ A
89 88 fmpttd ⊢ A ∈ V ∧ n ∈ ω ∧ F ⁡ n ⊆ wUniCl ⁡ A ∧ u ∈ F ⁡ n → v ∈ F ⁡ n ⟼ u v : F ⁡ n ⟶ wUniCl ⁡ A
90 89 frnd ⊢ A ∈ V ∧ n ∈ ω ∧ F ⁡ n ⊆ wUniCl ⁡ A ∧ u ∈ F ⁡ n → ran ⁡ v ∈ F ⁡ n ⟼ u v ⊆ wUniCl ⁡ A
91 83 90 unssd ⊢ A ∈ V ∧ n ∈ ω ∧ F ⁡ n ⊆ wUniCl ⁡ A ∧ u ∈ F ⁡ n → 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v ⊆ wUniCl ⁡ A
92 91 ralrimiva ⊢ A ∈ V ∧ n ∈ ω ∧ F ⁡ n ⊆ wUniCl ⁡ A → ∀ u ∈ F ⁡ n 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v ⊆ wUniCl ⁡ A
93 iunss ⊢ ⋃ u ∈ F ⁡ n 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v ⊆ wUniCl ⁡ A ↔ ∀ u ∈ F ⁡ n 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v ⊆ wUniCl ⁡ A
94 92 93 sylibr ⊢ A ∈ V ∧ n ∈ ω ∧ F ⁡ n ⊆ wUniCl ⁡ A → ⋃ u ∈ F ⁡ n 𝒫 u ⋃ u ∪ ran ⁡ v ∈ F ⁡ n ⟼ u v ⊆ 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 ⟼ u v ⊆ 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