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 e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om )
wuncval2.u 
|- U = U. ran F
Assertion wuncval2 
|- ( A e. V -> ( wUniCl ` A ) = U )

Proof

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