Metamath Proof Explorer

Theorem wunex2

Description: Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses wunex2.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 )
wunex2.u 
|- U = U. ran F
Assertion wunex2 
|- ( A e. V -> ( U e. WUni /\ A C_ U ) )

Proof

Step Hyp Ref Expression
1 wunex2.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 wunex2.u 
 |-  U = U. ran F
3 2 eleq2i 
 |-  ( a e. U <-> a e. U. ran F )
4 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
5 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 )
6 4 5 mpbir 
 |-  F Fn _om
7 fnunirn 
 |-  ( F Fn _om -> ( a e. U. ran F <-> E. m e. _om a e. ( F ` m ) ) )
8 6 7 ax-mp 
 |-  ( a e. U. ran F <-> E. m e. _om a e. ( F ` m ) )
9 3 8 bitri 
 |-  ( a e. U <-> E. m e. _om a e. ( F ` m ) )
10 elssuni 
 |-  ( a e. ( F ` m ) -> a C_ U. ( F ` m ) )
11 10 ad2antll 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> a C_ U. ( F ` m ) )
12 ssun2 
 |-  U. ( F ` m ) C_ ( ( F ` m ) u. U. ( F ` m ) )
13 ssun1 
 |-  ( ( F ` m ) u. U. ( F ` m ) ) C_ ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) )
14 12 13 sstri 
 |-  U. ( F ` m ) C_ ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) )
15 11 14 sstrdi 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> a C_ ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) ) )
16 simprl 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> m e. _om )
17 fvex 
 |-  ( F ` m ) e. _V
18 17 uniex 
 |-  U. ( F ` m ) e. _V
19 17 18 unex 
 |-  ( ( F ` m ) u. U. ( F ` m ) ) e. _V
20 prex 
 |-  { ~P u , U. u } e. _V
21 17 mptex 
 |-  ( v e. ( F ` m ) |-> { u , v } ) e. _V
22 21 rnex 
 |-  ran ( v e. ( F ` m ) |-> { u , v } ) e. _V
23 20 22 unex 
 |-  ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) e. _V
24 17 23 iunex 
 |-  U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) e. _V
25 19 24 unex 
 |-  ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) ) e. _V
26 id 
 |-  ( w = z -> w = z )
27 unieq 
 |-  ( w = z -> U. w = U. z )
28 26 27 uneq12d 
 |-  ( w = z -> ( w u. U. w ) = ( z u. U. z ) )
29 pweq 
 |-  ( u = x -> ~P u = ~P x )
30 unieq 
 |-  ( u = x -> U. u = U. x )
31 29 30 preq12d 
 |-  ( u = x -> { ~P u , U. u } = { ~P x , U. x } )
32 preq2 
 |-  ( v = y -> { u , v } = { u , y } )
33 32 cbvmptv 
 |-  ( v e. w |-> { u , v } ) = ( y e. w |-> { u , y } )
34 preq1 
 |-  ( u = x -> { u , y } = { x , y } )
35 34 mpteq2dv 
 |-  ( u = x -> ( y e. w |-> { u , y } ) = ( y e. w |-> { x , y } ) )
36 33 35 syl5eq 
 |-  ( u = x -> ( v e. w |-> { u , v } ) = ( y e. w |-> { x , y } ) )
37 36 rneqd 
 |-  ( u = x -> ran ( v e. w |-> { u , v } ) = ran ( y e. w |-> { x , y } ) )
38 31 37 uneq12d 
 |-  ( u = x -> ( { ~P u , U. u } u. ran ( v e. w |-> { u , v } ) ) = ( { ~P x , U. x } u. ran ( y e. w |-> { x , y } ) ) )
39 38 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 ( y e. w |-> { x , y } ) )
40 mpteq1 
 |-  ( w = z -> ( y e. w |-> { x , y } ) = ( y e. z |-> { x , y } ) )
41 40 rneqd 
 |-  ( w = z -> ran ( y e. w |-> { x , y } ) = ran ( y e. z |-> { x , y } ) )
42 41 uneq2d 
 |-  ( w = z -> ( { ~P x , U. x } u. ran ( y e. w |-> { x , y } ) ) = ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) )
43 26 42 iuneq12d 
 |-  ( w = z -> U_ x e. w ( { ~P x , U. x } u. ran ( y e. w |-> { x , y } ) ) = U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) )
44 39 43 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 } ) ) )
45 28 44 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 } ) ) ) )
46 id 
 |-  ( w = ( F ` m ) -> w = ( F ` m ) )
47 unieq 
 |-  ( w = ( F ` m ) -> U. w = U. ( F ` m ) )
48 46 47 uneq12d 
 |-  ( w = ( F ` m ) -> ( w u. U. w ) = ( ( F ` m ) u. U. ( F ` m ) ) )
49 mpteq1 
 |-  ( w = ( F ` m ) -> ( v e. w |-> { u , v } ) = ( v e. ( F ` m ) |-> { u , v } ) )
50 49 rneqd 
 |-  ( w = ( F ` m ) -> ran ( v e. w |-> { u , v } ) = ran ( v e. ( F ` m ) |-> { u , v } ) )
51 50 uneq2d 
 |-  ( w = ( F ` m ) -> ( { ~P u , U. u } u. ran ( v e. w |-> { u , v } ) ) = ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) )
52 46 51 iuneq12d 
 |-  ( w = ( F ` m ) -> U_ u e. w ( { ~P u , U. u } u. ran ( v e. w |-> { u , v } ) ) = U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) )
53 48 52 uneq12d 
 |-  ( w = ( F ` m ) -> ( ( w u. U. w ) u. U_ u e. w ( { ~P u , U. u } u. ran ( v e. w |-> { u , v } ) ) ) = ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) ) )
54 1 45 53 frsucmpt2w 
 |-  ( ( m e. _om /\ ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) ) e. _V ) -> ( F ` suc m ) = ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) ) )
55 16 25 54 sylancl 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> ( F ` suc m ) = ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) ) )
56 15 55 sseqtrrd 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> a C_ ( F ` suc m ) )
57 fvssunirn 
 |-  ( F ` suc m ) C_ U. ran F
58 57 2 sseqtrri 
 |-  ( F ` suc m ) C_ U
59 56 58 sstrdi 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> a C_ U )
60 59 rexlimdvaa 
 |-  ( A e. V -> ( E. m e. _om a e. ( F ` m ) -> a C_ U ) )
61 9 60 syl5bi 
 |-  ( A e. V -> ( a e. U -> a C_ U ) )
62 61 ralrimiv 
 |-  ( A e. V -> A. a e. U a C_ U )
63 dftr3 
 |-  ( Tr U <-> A. a e. U a C_ U )
64 62 63 sylibr 
 |-  ( A e. V -> Tr U )
65 1on 
 |-  1o e. On
66 unexg 
 |-  ( ( A e. V /\ 1o e. On ) -> ( A u. 1o ) e. _V )
67 65 66 mpan2 
 |-  ( A e. V -> ( A u. 1o ) e. _V )
68 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 ) ` (/) )
69 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 ) )
70 68 69 syl5eq 
 |-  ( ( A u. 1o ) e. _V -> ( F ` (/) ) = ( A u. 1o ) )
71 67 70 syl 
 |-  ( A e. V -> ( F ` (/) ) = ( A u. 1o ) )
72 fvssunirn 
 |-  ( F ` (/) ) C_ U. ran F
73 72 2 sseqtrri 
 |-  ( F ` (/) ) C_ U
74 71 73 eqsstrrdi 
 |-  ( A e. V -> ( A u. 1o ) C_ U )
75 74 unssbd 
 |-  ( A e. V -> 1o C_ U )
76 1n0 
 |-  1o =/= (/)
77 ssn0 
 |-  ( ( 1o C_ U /\ 1o =/= (/) ) -> U =/= (/) )
78 75 76 77 sylancl 
 |-  ( A e. V -> U =/= (/) )
79 pweq 
 |-  ( u = a -> ~P u = ~P a )
80 unieq 
 |-  ( u = a -> U. u = U. a )
81 79 80 preq12d 
 |-  ( u = a -> { ~P u , U. u } = { ~P a , U. a } )
82 preq1 
 |-  ( u = a -> { u , v } = { a , v } )
83 82 mpteq2dv 
 |-  ( u = a -> ( v e. ( F ` m ) |-> { u , v } ) = ( v e. ( F ` m ) |-> { a , v } ) )
84 83 rneqd 
 |-  ( u = a -> ran ( v e. ( F ` m ) |-> { u , v } ) = ran ( v e. ( F ` m ) |-> { a , v } ) )
85 81 84 uneq12d 
 |-  ( u = a -> ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) = ( { ~P a , U. a } u. ran ( v e. ( F ` m ) |-> { a , v } ) ) )
86 85 ssiun2s 
 |-  ( a e. ( F ` m ) -> ( { ~P a , U. a } u. ran ( v e. ( F ` m ) |-> { a , v } ) ) C_ U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) )
87 86 ad2antll 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> ( { ~P a , U. a } u. ran ( v e. ( F ` m ) |-> { a , v } ) ) C_ U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) )
88 ssun2 
 |-  U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) C_ ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) )
89 88 55 sseqtrrid 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) C_ ( F ` suc m ) )
90 89 58 sstrdi 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) C_ U )
91 87 90 sstrd 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> ( { ~P a , U. a } u. ran ( v e. ( F ` m ) |-> { a , v } ) ) C_ U )
92 91 unssad 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> { ~P a , U. a } C_ U )
93 vpwex 
 |-  ~P a e. _V
94 vuniex 
 |-  U. a e. _V
95 93 94 prss 
 |-  ( ( ~P a e. U /\ U. a e. U ) <-> { ~P a , U. a } C_ U )
96 92 95 sylibr 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> ( ~P a e. U /\ U. a e. U ) )
97 96 simprd 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> U. a e. U )
98 96 simpld 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> ~P a e. U )
99 2 eleq2i 
 |-  ( b e. U <-> b e. U. ran F )
100 fnunirn 
 |-  ( F Fn _om -> ( b e. U. ran F <-> E. n e. _om b e. ( F ` n ) ) )
101 6 100 ax-mp 
 |-  ( b e. U. ran F <-> E. n e. _om b e. ( F ` n ) )
102 99 101 bitri 
 |-  ( b e. U <-> E. n e. _om b e. ( F ` n ) )
103 ordom 
 |-  Ord _om
104 simplrl 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> m e. _om )
105 simprl 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> n e. _om )
106 ordunel 
 |-  ( ( Ord _om /\ m e. _om /\ n e. _om ) -> ( m u. n ) e. _om )
107 103 104 105 106 mp3an2i 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> ( m u. n ) e. _om )
108 ssun1 
 |-  m C_ ( m u. n )
109 fveq2 
 |-  ( k = m -> ( F ` k ) = ( F ` m ) )
110 109 sseq2d 
 |-  ( k = m -> ( ( F ` m ) C_ ( F ` k ) <-> ( F ` m ) C_ ( F ` m ) ) )
111 fveq2 
 |-  ( k = i -> ( F ` k ) = ( F ` i ) )
112 111 sseq2d 
 |-  ( k = i -> ( ( F ` m ) C_ ( F ` k ) <-> ( F ` m ) C_ ( F ` i ) ) )
113 fveq2 
 |-  ( k = suc i -> ( F ` k ) = ( F ` suc i ) )
114 113 sseq2d 
 |-  ( k = suc i -> ( ( F ` m ) C_ ( F ` k ) <-> ( F ` m ) C_ ( F ` suc i ) ) )
115 fveq2 
 |-  ( k = ( m u. n ) -> ( F ` k ) = ( F ` ( m u. n ) ) )
116 115 sseq2d 
 |-  ( k = ( m u. n ) -> ( ( F ` m ) C_ ( F ` k ) <-> ( F ` m ) C_ ( F ` ( m u. n ) ) ) )
117 ssidd 
 |-  ( m e. _om -> ( F ` m ) C_ ( F ` m ) )
118 fveq2 
 |-  ( m = i -> ( F ` m ) = ( F ` i ) )
119 suceq 
 |-  ( m = i -> suc m = suc i )
120 119 fveq2d 
 |-  ( m = i -> ( F ` suc m ) = ( F ` suc i ) )
121 118 120 sseq12d 
 |-  ( m = i -> ( ( F ` m ) C_ ( F ` suc m ) <-> ( F ` i ) C_ ( F ` suc i ) ) )
122 ssun1 
 |-  ( F ` m ) C_ ( ( F ` m ) u. U. ( F ` m ) )
123 122 13 sstri 
 |-  ( F ` m ) C_ ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) )
124 25 54 mpan2 
 |-  ( m e. _om -> ( F ` suc m ) = ( ( ( F ` m ) u. U. ( F ` m ) ) u. U_ u e. ( F ` m ) ( { ~P u , U. u } u. ran ( v e. ( F ` m ) |-> { u , v } ) ) ) )
125 123 124 sseqtrrid 
 |-  ( m e. _om -> ( F ` m ) C_ ( F ` suc m ) )
126 121 125 vtoclga 
 |-  ( i e. _om -> ( F ` i ) C_ ( F ` suc i ) )
127 126 ad2antrr 
 |-  ( ( ( i e. _om /\ m e. _om ) /\ m C_ i ) -> ( F ` i ) C_ ( F ` suc i ) )
128 sstr2 
 |-  ( ( F ` m ) C_ ( F ` i ) -> ( ( F ` i ) C_ ( F ` suc i ) -> ( F ` m ) C_ ( F ` suc i ) ) )
129 127 128 syl5com 
 |-  ( ( ( i e. _om /\ m e. _om ) /\ m C_ i ) -> ( ( F ` m ) C_ ( F ` i ) -> ( F ` m ) C_ ( F ` suc i ) ) )
130 110 112 114 116 117 129 findsg 
 |-  ( ( ( ( m u. n ) e. _om /\ m e. _om ) /\ m C_ ( m u. n ) ) -> ( F ` m ) C_ ( F ` ( m u. n ) ) )
131 108 130 mpan2 
 |-  ( ( ( m u. n ) e. _om /\ m e. _om ) -> ( F ` m ) C_ ( F ` ( m u. n ) ) )
132 107 104 131 syl2anc 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> ( F ` m ) C_ ( F ` ( m u. n ) ) )
133 simplrr 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> a e. ( F ` m ) )
134 132 133 sseldd 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> a e. ( F ` ( m u. n ) ) )
135 82 mpteq2dv 
 |-  ( u = a -> ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) = ( v e. ( F ` ( m u. n ) ) |-> { a , v } ) )
136 135 rneqd 
 |-  ( u = a -> ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) = ran ( v e. ( F ` ( m u. n ) ) |-> { a , v } ) )
137 81 136 uneq12d 
 |-  ( u = a -> ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) = ( { ~P a , U. a } u. ran ( v e. ( F ` ( m u. n ) ) |-> { a , v } ) ) )
138 137 ssiun2s 
 |-  ( a e. ( F ` ( m u. n ) ) -> ( { ~P a , U. a } u. ran ( v e. ( F ` ( m u. n ) ) |-> { a , v } ) ) C_ U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) )
139 134 138 syl 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> ( { ~P a , U. a } u. ran ( v e. ( F ` ( m u. n ) ) |-> { a , v } ) ) C_ U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) )
140 ssun2 
 |-  U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) C_ ( ( ( F ` ( m u. n ) ) u. U. ( F ` ( m u. n ) ) ) u. U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) )
141 fvex 
 |-  ( F ` ( m u. n ) ) e. _V
142 141 uniex 
 |-  U. ( F ` ( m u. n ) ) e. _V
143 141 142 unex 
 |-  ( ( F ` ( m u. n ) ) u. U. ( F ` ( m u. n ) ) ) e. _V
144 141 mptex 
 |-  ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) e. _V
145 144 rnex 
 |-  ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) e. _V
146 20 145 unex 
 |-  ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) e. _V
147 141 146 iunex 
 |-  U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) e. _V
148 143 147 unex 
 |-  ( ( ( F ` ( m u. n ) ) u. U. ( F ` ( m u. n ) ) ) u. U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) ) e. _V
149 id 
 |-  ( w = ( F ` ( m u. n ) ) -> w = ( F ` ( m u. n ) ) )
150 unieq 
 |-  ( w = ( F ` ( m u. n ) ) -> U. w = U. ( F ` ( m u. n ) ) )
151 149 150 uneq12d 
 |-  ( w = ( F ` ( m u. n ) ) -> ( w u. U. w ) = ( ( F ` ( m u. n ) ) u. U. ( F ` ( m u. n ) ) ) )
152 mpteq1 
 |-  ( w = ( F ` ( m u. n ) ) -> ( v e. w |-> { u , v } ) = ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) )
153 152 rneqd 
 |-  ( w = ( F ` ( m u. n ) ) -> ran ( v e. w |-> { u , v } ) = ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) )
154 153 uneq2d 
 |-  ( w = ( F ` ( m u. n ) ) -> ( { ~P u , U. u } u. ran ( v e. w |-> { u , v } ) ) = ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) )
155 149 154 iuneq12d 
 |-  ( w = ( F ` ( m u. n ) ) -> U_ u e. w ( { ~P u , U. u } u. ran ( v e. w |-> { u , v } ) ) = U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) )
156 151 155 uneq12d 
 |-  ( w = ( F ` ( m u. n ) ) -> ( ( w u. U. w ) u. U_ u e. w ( { ~P u , U. u } u. ran ( v e. w |-> { u , v } ) ) ) = ( ( ( F ` ( m u. n ) ) u. U. ( F ` ( m u. n ) ) ) u. U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) ) )
157 1 45 156 frsucmpt2w 
 |-  ( ( ( m u. n ) e. _om /\ ( ( ( F ` ( m u. n ) ) u. U. ( F ` ( m u. n ) ) ) u. U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) ) e. _V ) -> ( F ` suc ( m u. n ) ) = ( ( ( F ` ( m u. n ) ) u. U. ( F ` ( m u. n ) ) ) u. U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) ) )
158 107 148 157 sylancl 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> ( F ` suc ( m u. n ) ) = ( ( ( F ` ( m u. n ) ) u. U. ( F ` ( m u. n ) ) ) u. U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) ) )
159 140 158 sseqtrrid 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) C_ ( F ` suc ( m u. n ) ) )
160 fvssunirn 
 |-  ( F ` suc ( m u. n ) ) C_ U. ran F
161 160 2 sseqtrri 
 |-  ( F ` suc ( m u. n ) ) C_ U
162 159 161 sstrdi 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> U_ u e. ( F ` ( m u. n ) ) ( { ~P u , U. u } u. ran ( v e. ( F ` ( m u. n ) ) |-> { u , v } ) ) C_ U )
163 139 162 sstrd 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> ( { ~P a , U. a } u. ran ( v e. ( F ` ( m u. n ) ) |-> { a , v } ) ) C_ U )
164 163 unssbd 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> ran ( v e. ( F ` ( m u. n ) ) |-> { a , v } ) C_ U )
165 ssun2 
 |-  n C_ ( m u. n )
166 id 
 |-  ( i = ( m u. n ) -> i = ( m u. n ) )
167 165 166 sseqtrrid 
 |-  ( i = ( m u. n ) -> n C_ i )
168 167 biantrud 
 |-  ( i = ( m u. n ) -> ( n e. _om <-> ( n e. _om /\ n C_ i ) ) )
169 168 bicomd 
 |-  ( i = ( m u. n ) -> ( ( n e. _om /\ n C_ i ) <-> n e. _om ) )
170 fveq2 
 |-  ( i = ( m u. n ) -> ( F ` i ) = ( F ` ( m u. n ) ) )
171 170 sseq2d 
 |-  ( i = ( m u. n ) -> ( ( F ` n ) C_ ( F ` i ) <-> ( F ` n ) C_ ( F ` ( m u. n ) ) ) )
172 169 171 imbi12d 
 |-  ( i = ( m u. n ) -> ( ( ( n e. _om /\ n C_ i ) -> ( F ` n ) C_ ( F ` i ) ) <-> ( n e. _om -> ( F ` n ) C_ ( F ` ( m u. n ) ) ) ) )
173 eleq1w 
 |-  ( m = n -> ( m e. _om <-> n e. _om ) )
174 173 anbi2d 
 |-  ( m = n -> ( ( i e. _om /\ m e. _om ) <-> ( i e. _om /\ n e. _om ) ) )
175 sseq1 
 |-  ( m = n -> ( m C_ i <-> n C_ i ) )
176 174 175 anbi12d 
 |-  ( m = n -> ( ( ( i e. _om /\ m e. _om ) /\ m C_ i ) <-> ( ( i e. _om /\ n e. _om ) /\ n C_ i ) ) )
177 fveq2 
 |-  ( m = n -> ( F ` m ) = ( F ` n ) )
178 177 sseq1d 
 |-  ( m = n -> ( ( F ` m ) C_ ( F ` i ) <-> ( F ` n ) C_ ( F ` i ) ) )
179 176 178 imbi12d 
 |-  ( m = n -> ( ( ( ( i e. _om /\ m e. _om ) /\ m C_ i ) -> ( F ` m ) C_ ( F ` i ) ) <-> ( ( ( i e. _om /\ n e. _om ) /\ n C_ i ) -> ( F ` n ) C_ ( F ` i ) ) ) )
180 110 112 114 112 117 129 findsg 
 |-  ( ( ( i e. _om /\ m e. _om ) /\ m C_ i ) -> ( F ` m ) C_ ( F ` i ) )
181 179 180 chvarvv 
 |-  ( ( ( i e. _om /\ n e. _om ) /\ n C_ i ) -> ( F ` n ) C_ ( F ` i ) )
182 181 expl 
 |-  ( i e. _om -> ( ( n e. _om /\ n C_ i ) -> ( F ` n ) C_ ( F ` i ) ) )
183 172 182 vtoclga 
 |-  ( ( m u. n ) e. _om -> ( n e. _om -> ( F ` n ) C_ ( F ` ( m u. n ) ) ) )
184 107 105 183 sylc 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> ( F ` n ) C_ ( F ` ( m u. n ) ) )
185 simprr 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> b e. ( F ` n ) )
186 184 185 sseldd 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> b e. ( F ` ( m u. n ) ) )
187 prex 
 |-  { a , b } e. _V
188 eqid 
 |-  ( v e. ( F ` ( m u. n ) ) |-> { a , v } ) = ( v e. ( F ` ( m u. n ) ) |-> { a , v } )
189 preq2 
 |-  ( v = b -> { a , v } = { a , b } )
190 188 189 elrnmpt1s 
 |-  ( ( b e. ( F ` ( m u. n ) ) /\ { a , b } e. _V ) -> { a , b } e. ran ( v e. ( F ` ( m u. n ) ) |-> { a , v } ) )
191 186 187 190 sylancl 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> { a , b } e. ran ( v e. ( F ` ( m u. n ) ) |-> { a , v } ) )
192 164 191 sseldd 
 |-  ( ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) /\ ( n e. _om /\ b e. ( F ` n ) ) ) -> { a , b } e. U )
193 192 rexlimdvaa 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> ( E. n e. _om b e. ( F ` n ) -> { a , b } e. U ) )
194 102 193 syl5bi 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> ( b e. U -> { a , b } e. U ) )
195 194 ralrimiv 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> A. b e. U { a , b } e. U )
196 97 98 195 3jca 
 |-  ( ( A e. V /\ ( m e. _om /\ a e. ( F ` m ) ) ) -> ( U. a e. U /\ ~P a e. U /\ A. b e. U { a , b } e. U ) )
197 196 rexlimdvaa 
 |-  ( A e. V -> ( E. m e. _om a e. ( F ` m ) -> ( U. a e. U /\ ~P a e. U /\ A. b e. U { a , b } e. U ) ) )
198 9 197 syl5bi 
 |-  ( A e. V -> ( a e. U -> ( U. a e. U /\ ~P a e. U /\ A. b e. U { a , b } e. U ) ) )
199 198 ralrimiv 
 |-  ( A e. V -> A. a e. U ( U. a e. U /\ ~P a e. U /\ A. b e. U { a , b } e. U ) )
200 rdgfun 
 |-  Fun 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 ) )
201 omex 
 |-  _om e. _V
202 resfunexg 
 |-  ( ( Fun 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 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 ) e. _V )
203 200 201 202 mp2an 
 |-  ( 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 ) e. _V
204 1 203 eqeltri 
 |-  F e. _V
205 204 rnex 
 |-  ran F e. _V
206 205 uniex 
 |-  U. ran F e. _V
207 2 206 eqeltri 
 |-  U e. _V
208 iswun 
 |-  ( U e. _V -> ( U e. WUni <-> ( Tr U /\ U =/= (/) /\ A. a e. U ( U. a e. U /\ ~P a e. U /\ A. b e. U { a , b } e. U ) ) ) )
209 207 208 ax-mp 
 |-  ( U e. WUni <-> ( Tr U /\ U =/= (/) /\ A. a e. U ( U. a e. U /\ ~P a e. U /\ A. b e. U { a , b } e. U ) ) )
210 64 78 199 209 syl3anbrc 
 |-  ( A e. V -> U e. WUni )
211 74 unssad 
 |-  ( A e. V -> A C_ U )
212 210 211 jca 
 |-  ( A e. V -> ( U e. WUni /\ A C_ U ) )